diff options
| author |  Jason Koenig <unknown> | 2011-06-29 19:10:44 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2011-06-29 19:10:44 -0700 |
| commit | ffbc6c1e2a8b372e6df472acf486481d95657042 (patch) | |
| tree | 45426fbafc9e97c329e7fc7403b37ec3028bdbdd /Test/dafny0/Answer | |
| parent | eeeb1e217b3045191a498f4567f1e28979b4f075 (diff) | |
Added additional test case to modifies on loops tests.
Diffstat (limited to 'Test/dafny0/Answer')
| -rw-r--r-- | Test/dafny0/Answer | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 51d3efcd..384037ae 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1040,7 +1040,7 @@ Execution trace: 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
+LoopModifies.dfy(98,8): 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
@@ -1049,7 +1049,7 @@ Execution trace: (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
+LoopModifies.dfy(146,11): 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
@@ -1073,23 +1073,23 @@ Execution trace: (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
+LoopModifies.dfy(285,13): 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
+ LoopModifies.dfy(273,4): anon17_LoopHead
(0,0): anon17_LoopBody
- LoopModifies.dfy(248,4): anon18_Else
+ LoopModifies.dfy(273,4): anon18_Else
(0,0): anon5
- LoopModifies.dfy(248,4): anon20_Else
+ LoopModifies.dfy(273,4): anon20_Else
(0,0): anon7
- LoopModifies.dfy(256,7): anon21_LoopHead
+ LoopModifies.dfy(281,7): anon21_LoopHead
(0,0): anon21_LoopBody
- LoopModifies.dfy(256,7): anon22_Else
+ LoopModifies.dfy(281,7): anon22_Else
(0,0): anon12
- LoopModifies.dfy(256,7): anon24_Else
+ LoopModifies.dfy(281,7): anon24_Else
(0,0): anon14
-Dafny program verifier finished with 21 verified, 9 errors
+Dafny program verifier finished with 23 verified, 9 errors
-------------------- ReturnErrors.dfy --------------------
ReturnErrors.dfy(30,10): Error: cannot have method call in return statement.
|