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];
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)) {
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 ()) {
}
}
+ // 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
--- /dev/null
+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");
+ }
+}