Dafny: Fixed bug in call statements where mutability of out parameters was not checked.

Added regression test.

1 files changed, 21 insertions, 0 deletions

diff --git a/Test/dafny0/CallStmtTests.dfy b/Test/dafny0/CallStmtTests.dfy
new file mode 100644
index 00000000..735efe81
--- /dev/null
+++ b/Test/dafny0/CallStmtTests.dfy
@@ -0,0 +1,21 @@
+

+method testing1(t: int)

+{

+   t := m(); // error: should be checked at the Dafny level, not fall to Boogie.

+}

+

+method m() returns (r: int)

+{

+   return 3;

+}

+

+method testing2()

+{

+   var v;

+   v := m2(); // error: v needs to be ghost because r is.

+}

+

+method m2() returns (ghost r: int)

+{

+   r := 23;

+}