diff options
| author |  wuestholz <unknown> | 2014-05-29 21:41:00 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-05-29 21:41:00 +0200 |
| commit | 607ef28aadb281ab61a2be493a637126e967a388 (patch) | |
| tree | aae16c049c860e443920f9c6ee31af4e35f8a800 /Test/dafny0/LoopModifies.dfy.expect | |
| parent | dc0a9130355352d0f47e07232d8119fc7219ccbc (diff) | |
Set up the same test infrastructure as in Boogie.
Diffstat (limited to 'Test/dafny0/LoopModifies.dfy.expect')
| -rw-r--r-- | Test/dafny0/LoopModifies.dfy.expect | 65 |
1 files changed, 65 insertions, 0 deletions
diff --git a/Test/dafny0/LoopModifies.dfy.expect b/Test/dafny0/LoopModifies.dfy.expect new file mode 100644 index 00000000..682975fb --- /dev/null +++ b/Test/dafny0/LoopModifies.dfy.expect @@ -0,0 +1,65 @@ +LoopModifies.dfy(8,5): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+ (0,0): anon0
+LoopModifies.dfy(19,8): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+ (0,0): anon0
+ LoopModifies.dfy(16,4): anon8_LoopHead
+ (0,0): anon8_LoopBody
+ LoopModifies.dfy(16,4): anon9_Else
+ LoopModifies.dfy(16,4): anon11_Else
+LoopModifies.dfy(48,8): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+ (0,0): anon0
+ LoopModifies.dfy(44,4): anon8_LoopHead
+ (0,0): anon8_LoopBody
+ LoopModifies.dfy(44,4): anon9_Else
+ LoopModifies.dfy(44,4): anon11_Else
+LoopModifies.dfy(63,8): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+ (0,0): anon0
+ LoopModifies.dfy(59,4): anon9_LoopHead
+ (0,0): anon9_LoopBody
+ LoopModifies.dfy(59,4): anon10_Else
+ LoopModifies.dfy(59,4): anon12_Else
+LoopModifies.dfy(76,4): Error: loop modifies clause may violate context's modifies clause
+Execution trace:
+ (0,0): anon0
+LoopModifies.dfy(100,8): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+ (0,0): anon0
+ LoopModifies.dfy(92,4): anon8_LoopHead
+ (0,0): anon8_LoopBody
+ LoopModifies.dfy(92,4): anon9_Else
+ LoopModifies.dfy(92,4): anon11_Else
+LoopModifies.dfy(148,11): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+ (0,0): anon0
+ LoopModifies.dfy(136,4): anon17_LoopHead
+ (0,0): anon17_LoopBody
+ LoopModifies.dfy(136,4): anon18_Else
+ LoopModifies.dfy(136,4): anon20_Else
+ LoopModifies.dfy(141,7): anon21_LoopHead
+ (0,0): anon21_LoopBody
+ LoopModifies.dfy(141,7): anon22_Else
+ LoopModifies.dfy(141,7): anon24_Else
+LoopModifies.dfy(199,10): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+ (0,0): anon0
+ LoopModifies.dfy(195,4): anon8_LoopHead
+ (0,0): anon8_LoopBody
+ LoopModifies.dfy(195,4): anon9_Else
+ LoopModifies.dfy(195,4): anon11_Else
+LoopModifies.dfy(287,13): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+ (0,0): anon0
+ LoopModifies.dfy(275,4): anon16_LoopHead
+ (0,0): anon16_LoopBody
+ LoopModifies.dfy(275,4): anon17_Else
+ LoopModifies.dfy(275,4): anon19_Else
+ LoopModifies.dfy(283,7): anon20_LoopHead
+ (0,0): anon20_LoopBody
+ LoopModifies.dfy(283,7): anon21_Else
+ LoopModifies.dfy(283,7): anon23_Else
+
+Dafny program verifier finished with 23 verified, 9 errors
|