summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--codegen/valaccodebasemodule.vala18
-rw-r--r--tests/Makefile.am1
-rw-r--r--tests/methods/postconditions.vala51
3 files changed, 63 insertions, 7 deletions
diff --git a/codegen/valaccodebasemodule.vala b/codegen/valaccodebasemodule.vala
index 20f250704..0bf62de07 100644
--- a/codegen/valaccodebasemodule.vala
+++ b/codegen/valaccodebasemodule.vala
@@ -2339,6 +2339,14 @@ public abstract class Vala.CCodeBaseModule : CodeGenerator {
pop_line ();
}
+ if (b.parent_symbol is Method) {
+ unowned Method m = (Method) b.parent_symbol;
+ // check postconditions
+ foreach (var postcondition in m.get_postconditions ()) {
+ create_postcondition_statement (postcondition);
+ }
+ }
+
// free in reverse order
for (int i = local_vars.size - 1; i >= 0; i--) {
var local = local_vars[i];
@@ -2363,10 +2371,6 @@ public abstract class Vala.CCodeBaseModule : CodeGenerator {
return_out_parameter (param);
}
}
- // check postconditions
- foreach (var postcondition in m.get_postconditions ()) {
- create_postcondition_statement (postcondition);
- }
} else if (!unreachable_exit_block && b.parent_symbol is PropertyAccessor) {
var acc = (PropertyAccessor) b.parent_symbol;
if (acc.value_parameter != null && !acc.value_parameter.captured && requires_destroy (acc.value_parameter.variable_type)) {
@@ -3993,9 +3997,6 @@ public abstract class Vala.CCodeBaseModule : CodeGenerator {
ccode.add_assignment (result_lhs, get_cvalue (stmt.return_expression));
}
- // free local variables
- append_local_free (current_symbol);
-
if (current_method != null) {
// check postconditions
foreach (Expression postcondition in current_method.get_postconditions ()) {
@@ -4003,6 +4004,9 @@ public abstract class Vala.CCodeBaseModule : CodeGenerator {
}
}
+ // free local variables
+ append_local_free (current_symbol);
+
if (current_method != null && !current_method.coroutine) {
// assign values to output parameters if they are not NULL
// otherwise, free the value if necessary
diff --git a/tests/Makefile.am b/tests/Makefile.am
index dcda2cbe0..9139b02d5 100644
--- a/tests/Makefile.am
+++ b/tests/Makefile.am
@@ -120,6 +120,7 @@ TESTS = \
methods/iterator.vala \
methods/parameter-ref-array-resize.vala \
methods/prepostconditions.vala \
+ methods/postconditions.vala \
methods/same-name.vala \
methods/symbolresolution.vala \
methods/bug540483.vala \
diff --git a/tests/methods/postconditions.vala b/tests/methods/postconditions.vala
new file mode 100644
index 000000000..5cd9c5929
--- /dev/null
+++ b/tests/methods/postconditions.vala
@@ -0,0 +1,51 @@
+void foo (owned string[] a) ensures (a[1] == "bar") {
+}
+
+void foz (ref string[] a) ensures (a[1] == "bar") {
+ a = { "foo", "bar" };
+}
+
+void fom (out string[] a) ensures (a[1] == "bar") {
+ a = { "foo", "bar" };
+}
+
+string[] bar (owned string[] a) ensures (result[0] == "manam" && a[1] == "foo") {
+ return { "manam" };
+}
+
+string[] baz (ref string[] a) ensures (result[0] == "manam" && a[1] == "foo") {
+ a = { "bar", "foo" };
+ return { "manam" };
+}
+
+string[] bam (out string[] a) ensures (result[0] == "manam" && a[1] == "foo") {
+ a = { "bar", "foo" };
+ return { "manam" };
+}
+
+void main () {
+ {
+ foo ({ "foo", "bar" });
+ }
+ {
+ string[] a = {};
+ foz (ref a);
+ assert (a[0] == "foo");
+ }
+ {
+ string[] a;
+ fom (out a);
+ assert (a[0] == "foo");
+ }
+ {
+ assert (bar ({ "bar", "foo" })[0] == "manam");
+ }
+ {
+ string[] a = {};
+ assert (baz (ref a)[0] == "manam");
+ }
+ {
+ string[] a;
+ assert (bam (out a)[0] == "manam");
+ }
+}