Added regression test for loop modifies clauses.

2 files changed, 86 insertions, 1 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 2abd64b2..da82fd59 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1000,3 +1000,88 @@ RefinementErrors.dfy(42,9): Error: Refined class has a member with the same name
 RefinementErrors.dfy(12,10): Error: Refinement methods can only be declared in refinement classes: M

 RefinementErrors.dfy(34,10): Error: Different number of output variables

 6 resolution/type errors detected in RefinementErrors.dfy

+

+-------------------- LoopModifies.dfy --------------------

+LoopModifies.dfy(6,5): Error: assignment may update an array element not in the enclosing context's modifies clause

+Execution trace:

+    (0,0): anon0

+LoopModifies.dfy(17,8): Error: assignment may update an array element not in the enclosing context's modifies clause

+Execution trace:

+    (0,0): anon0

+    LoopModifies.dfy(14,4): anon9_LoopHead

+    (0,0): anon9_LoopBody

+    LoopModifies.dfy(14,4): anon10_Else

+    (0,0): anon5

+    LoopModifies.dfy(14,4): anon12_Else

+    (0,0): anon7

+LoopModifies.dfy(46,8): Error: assignment may update an array element not in the enclosing context's modifies clause

+Execution trace:

+    (0,0): anon0

+    LoopModifies.dfy(42,4): anon9_LoopHead

+    (0,0): anon9_LoopBody

+    LoopModifies.dfy(42,4): anon10_Else

+    (0,0): anon5

+    LoopModifies.dfy(42,4): anon12_Else

+    (0,0): anon7

+LoopModifies.dfy(61,8): Error: assignment may update an array element not in the enclosing context's modifies clause

+Execution trace:

+    (0,0): anon0

+    LoopModifies.dfy(57,4): anon9_LoopHead

+    (0,0): anon9_LoopBody

+    LoopModifies.dfy(57,4): anon10_Else

+    (0,0): anon5

+    LoopModifies.dfy(57,4): anon12_Else

+    (0,0): anon7

+LoopModifies.dfy(74,4): Error: loop modifies clause may violate context's modifies clause

+Execution trace:

+    (0,0): anon0

+LoopModifies.dfy(98,5): Error: assignment may update an array element not in the enclosing context's modifies clause

+Execution trace:

+    (0,0): anon0

+    LoopModifies.dfy(90,4): anon9_LoopHead

+    (0,0): anon9_LoopBody

+    LoopModifies.dfy(90,4): anon10_Else

+    (0,0): anon5

+    LoopModifies.dfy(90,4): anon12_Else

+    (0,0): anon7

+LoopModifies.dfy(146,5): Error: assignment may update an array element not in the enclosing context's modifies clause

+Execution trace:

+    (0,0): anon0

+    LoopModifies.dfy(134,4): anon17_LoopHead

+    (0,0): anon17_LoopBody

+    LoopModifies.dfy(134,4): anon18_Else

+    (0,0): anon5

+    LoopModifies.dfy(134,4): anon20_Else

+    (0,0): anon7

+    LoopModifies.dfy(139,7): anon21_LoopHead

+    (0,0): anon21_LoopBody

+    LoopModifies.dfy(139,7): anon22_Else

+    (0,0): anon12

+    LoopModifies.dfy(139,7): anon24_Else

+    (0,0): anon14

+LoopModifies.dfy(197,10): Error: assignment may update an array element not in the enclosing context's modifies clause

+Execution trace:

+    (0,0): anon0

+    LoopModifies.dfy(193,4): anon9_LoopHead

+    (0,0): anon9_LoopBody

+    LoopModifies.dfy(193,4): anon10_Else

+    (0,0): anon5

+    LoopModifies.dfy(193,4): anon12_Else

+    (0,0): anon7

+LoopModifies.dfy(260,10): Error: assignment may update an array element not in the enclosing context's modifies clause

+Execution trace:

+    (0,0): anon0

+    LoopModifies.dfy(248,4): anon17_LoopHead

+    (0,0): anon17_LoopBody

+    LoopModifies.dfy(248,4): anon18_Else

+    (0,0): anon5

+    LoopModifies.dfy(248,4): anon20_Else

+    (0,0): anon7

+    LoopModifies.dfy(256,7): anon21_LoopHead

+    (0,0): anon21_LoopBody

+    LoopModifies.dfy(256,7): anon22_Else

+    (0,0): anon12

+    LoopModifies.dfy(256,7): anon24_Else

+    (0,0): anon14

+

+Dafny program verifier finished with 21 verified, 9 errors

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index aed9ee8a..3c64f623 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -18,7 +18,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             Comprehensions.dfy Basics.dfy ControlStructures.dfy

             Termination.dfy DTypes.dfy

             TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy

-            Refinement.dfy RefinementErrors.dfy) do (

+            Refinement.dfy RefinementErrors.dfy LoopModifies.dfy) do (

   echo.

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

   %DAFNY_EXE% /compile:0 %* %%f