Dafny: removed Dafny's "foreach" statements (replaced by the new "parallel" statement)

1 files changed, 33 insertions, 31 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 697bdd9e..04d60716 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -173,11 +173,18 @@ SmallTests.dfy(131,9): Error: call may violate context's modifies clause
 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

-SmallTests.dfy(171,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause

+SmallTests.dfy(171,9): Error: assignment may update an object field not in the enclosing context's modifies clause

 Execution trace:

     (0,0): anon0

-    (0,0): anon4_Else

-    (0,0): anon3

+    (0,0): anon22_Else

+    (0,0): anon5

+    (0,0): anon24_Else

+    (0,0): anon11

+    (0,0): anon26_Else

+    (0,0): anon16

+    (0,0): anon28_Then

+    (0,0): anon29_Then

+    (0,0): anon19

 SmallTests.dfy(199,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

@@ -374,46 +381,37 @@ Execution trace:
     (0,0): anon23_Then

     (0,0): anon24_Then

     (0,0): anon11

-Definedness.dfy(199,24): Error: possible violation of function precondition

+Definedness.dfy(193,19): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-Definedness.dfy(201,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause

-Execution trace:

-    (0,0): anon0

-Definedness.dfy(203,33): Error: range expression must be well defined

-Execution trace:

-    (0,0): anon0

-Definedness.dfy(218,19): Error: possible division by zero

-Execution trace:

-    (0,0): anon0

-    Definedness.dfy(216,5): anon7_LoopHead

+    Definedness.dfy(191,5): anon7_LoopHead

     (0,0): anon7_LoopBody

     (0,0): anon8_Then

-Definedness.dfy(218,23): Error BP5004: This loop invariant might not hold on entry.

+Definedness.dfy(193,23): Error BP5004: This loop invariant might not hold on entry.

 Execution trace:

     (0,0): anon0

-Definedness.dfy(218,28): Error: possible division by zero

+Definedness.dfy(193,28): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-    Definedness.dfy(216,5): anon7_LoopHead

+    Definedness.dfy(191,5): anon7_LoopHead

     (0,0): anon7_LoopBody

     (0,0): anon8_Then

-Definedness.dfy(239,46): Error: possible violation of function postcondition

+Definedness.dfy(214,46): Error: possible violation of function postcondition

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Else

-Definedness.dfy(246,22): Error: target object may be null

+Definedness.dfy(221,22): Error: target object may be null

 Execution trace:

     (0,0): anon5_Then

     (0,0): anon2

     (0,0): anon6_Then

-Definedness.dfy(262,24): Error: possible violation of function postcondition

+Definedness.dfy(237,24): Error: possible violation of function postcondition

 Execution trace:

     (0,0): anon7_Then

     (0,0): anon2

     (0,0): anon8_Else

 

-Dafny program verifier finished with 23 verified, 39 errors

+Dafny program verifier finished with 22 verified, 36 errors

 

 -------------------- FunctionSpecifications.dfy --------------------

 FunctionSpecifications.dfy(28,13): Error: possible violation of function postcondition

@@ -1128,21 +1126,25 @@ TypeAntecedents.dfy(55,1): Error BP5003: A postcondition might not hold on this
 TypeAntecedents.dfy(54,15): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon15_Then

+    (0,0): anon25_Then

     (0,0): anon6

-    (0,0): anon18_Then

+    (0,0): anon28_Then

     (0,0): anon8

-    (0,0): anon19_Then

-    (0,0): anon10

-    (0,0): anon20_Then

-    (0,0): anon21_Then

-    (0,0): anon14

+    (0,0): anon29_Else

+    (0,0): anon13

+    (0,0): anon31_Else

+    (0,0): anon18

+    (0,0): anon33_Then

+    (0,0): anon20

+    (0,0): anon34_Then

+    (0,0): anon35_Then

+    (0,0): anon24

 TypeAntecedents.dfy(63,16): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    (0,0): anon15_Else

-    (0,0): anon16_Then

-    (0,0): anon17_Else

+    (0,0): anon25_Else

+    (0,0): anon26_Then

+    (0,0): anon27_Else

 

 Dafny program verifier finished with 12 verified, 3 errors