From 98b0ebe1adba86bbf8452bcb036f01c884b69b90 Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Wed, 6 Jul 2011 14:10:11 -0700
Subject: Dafny: Fixed bug in call statements where mutability of out
 parameters was not checked. Added regression test.

---
 Test/dafny0/Answer            |  5 +++++
 Test/dafny0/CallStmtTests.dfy | 21 +++++++++++++++++++++
 Test/dafny0/runtest.bat       |  3 ++-
 3 files changed, 28 insertions(+), 1 deletion(-)
 create mode 100644 Test/dafny0/CallStmtTests.dfy

(limited to 'Test')

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index e5621773..a29c64fa 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1103,3 +1103,8 @@ Dafny program verifier finished with 16 verified, 0 errors
 -------------------- ChainingDisjointTests.dfy --------------------
 
 Dafny program verifier finished with 6 verified, 0 errors
+
+-------------------- CallStmtTests.dfy --------------------
+CallStmtTests.dfy(4,3): Error: LHS of assignment must denote a mutable variable
+CallStmtTests.dfy(15,8): Error: actual out-parameter 0 is required to be a ghost variable
+2 resolution/type errors detected in CallStmtTests.dfy
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;
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 143a0dc5..7aa1b38e 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -19,7 +19,8 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             Termination.dfy DTypes.dfy
             TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy
             Refinement.dfy RefinementErrors.dfy LoopModifies.dfy
-            ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy) do (
+            ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy
+            CallStmtTests.dfy) do (
   echo.
   echo -------------------- %%f --------------------
   %DAFNY_EXE% /compile:0 %* %%f
-- 
cgit v1.2.3