Bugfix in the translation of calc statements (oops), added more resolution and verification tests

5 files changed, 73 insertions, 14 deletions

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 2af8d4b4..2e486533 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -3986,11 +3986,13 @@ namespace Microsoft.Dafny {
       } else if (stmt is CalcStmt) {

         /* Translate into:

         if (*) {

+            // line well-formedness checks;

+        } else if (*) {

             hint0;

             assert t0 op t1;

             assume false;

-        } else if ...

-        } else {

+        } else if (*) { ...

+        } else if (*) {

             hint<n-1>;

             assert t<n-1> op tn;

             assume false;

@@ -4002,7 +4004,6 @@ namespace Microsoft.Dafny {
         AddComment(builder, stmt, "calc statement");

         if (s.Lines.Count > 0) {          

           Bpl.IfCmd ifCmd = null;

-          Bpl.StmtList els = null;

           Bpl.StmtListBuilder b;

           // check steps:

           for (int i = s.Steps.Count; 0 <= --i; ) {

@@ -4010,13 +4011,7 @@ namespace Microsoft.Dafny {
             TrStmt(s.Hints[i], b, locals, etran);

             b.Add(Assert(s.Lines[i + 1].tok, etran.TrExpr(s.Steps[i]), "the calculation step between the previous line and this line might not hold"));

             b.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False));

-            if (i == s.Steps.Count - 1) {

-              // first iteration (last step)

-              els = b.Collect(s.Tok);

-            } else {

-              ifCmd = new Bpl.IfCmd(s.Tok, null, b.Collect(s.Tok), ifCmd, els);

-              els = null;

-            }

+            ifCmd = new Bpl.IfCmd(s.Tok, null, b.Collect(s.Tok), ifCmd, null);

           }

           // check well-formedness of lines:

           b = new Bpl.StmtListBuilder();

@@ -4024,7 +4019,7 @@ namespace Microsoft.Dafny {
             TrStmt_CheckWellformed(e, b, locals, etran, false);

           }

           b.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False));

-          ifCmd = new Bpl.IfCmd(s.Tok, null, b.Collect(s.Tok), ifCmd, els);

+          ifCmd = new Bpl.IfCmd(s.Tok, null, b.Collect(s.Tok), ifCmd, null);

           builder.Add(ifCmd);

           // assume result:

           if (s.Steps.Count > 0) {

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 970f6d0f..158bd5fc 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -550,7 +550,8 @@ ResolutionErrors.dfy(372,8): Error: first argument to ==> must be of type bool (
 ResolutionErrors.dfy(372,8): Error: second argument to ==> must be of type bool (instead got int)

 ResolutionErrors.dfy(377,8): Error: first argument to ==> must be of type bool (instead got int)

 ResolutionErrors.dfy(377,8): Error: second argument to ==> must be of type bool (instead got int)

-56 resolution/type errors detected in ResolutionErrors.dfy

+ResolutionErrors.dfy(382,4): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

+57 resolution/type errors detected in ResolutionErrors.dfy

 

 -------------------- ParseErrors.dfy --------------------

 ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator

@@ -1629,6 +1630,26 @@ TailCalls.dfy(42,12): Error: 'decreases *' is allowed only on tail-recursive met
 TailCalls.dfy(64,12): Error: 'decreases *' is allowed only on tail-recursive methods

 5 resolution/type errors detected in TailCalls.dfy

 

+-------------------- Calculations.dfy --------------------

+Calculations.dfy(3,4): Error: index out of range

+Execution trace:

+    (0,0): anon0

+    (0,0): anon11_Then

+Calculations.dfy(8,13): Error: index out of range

+Execution trace:

+    (0,0): anon0

+    (0,0): anon13_Then

+Calculations.dfy(8,17): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon13_Then

+Calculations.dfy(36,11): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    Calculations.dfy(31,2): anon5_Else

+

+Dafny program verifier finished with 4 verified, 4 errors

+

 -------------------- Superposition.dfy --------------------

 

 Verifying CheckWellformed$$_0_M0.C.M ...

diff --git a/Test/dafny0/Calculations.dfy b/Test/dafny0/Calculations.dfy
new file mode 100644
index 00000000..9e44f62e
--- /dev/null
+++ b/Test/dafny0/Calculations.dfy
@@ -0,0 +1,37 @@
+method CalcTest0(s: seq<int>) {
+	calc {
+		s[0]; // error: ill-formed line
+	}
+	
+	calc {
+		2;
+		{ assert s[0] == 1; } // error: ill-formed hint
+		1 + 1;
+	}
+	
+	if (|s| > 0) {
+		calc {
+			s[0]; // OK: well-formed in this context
+			{ assert s[0] == s[0]; }
+			<= s[0];
+		}
+	}
+}
+
+method CalcTest1(x: int, y: int) {
+	calc {
+		x + y;
+		{ assume x == 0; }
+		y;
+	}
+	assert x == 0; // OK: follows from x + y == y;
+}
+
+method CalcTest2(x: int, y: int) {
+	calc {
+		x + y;
+		{ assume x == 0; }
+		y + x;
+	}
+	assert x == 0; // error: even though assumed above, is not exported by the calculation
+}
\ No newline at end of file
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index a7a84ebb..c615c5ec 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -376,5 +376,10 @@ method TestCalc(m: int, n: int, a: bool, b: bool)
 		n + m;

 		n + m + 1;

 		==> n + m + 2; // error: ==> operator requires boolean lines

-	}		

+	}

+	calc {

+		n + m;

+		{ print n + m; } // error: non-ghost statements are not allowed in hints

+		m + n;

+	}			

 }

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 2055e283..23dc20e0 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -23,7 +23,8 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy

             CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy

             Predicates.dfy Skeletons.dfy Maps.dfy LiberalEquality.dfy

-            RefinementModificationChecking.dfy TailCalls.dfy) do (

+            RefinementModificationChecking.dfy TailCalls.dfy

+            Calculations.dfy) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f