Set up the same test infrastructure as in Boogie.

1 files changed, 185 insertions, 0 deletions

diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect
new file mode 100644
index 00000000..496e3e5d
--- /dev/null
+++ b/Test/dafny0/SmallTests.dfy.expect
@@ -0,0 +1,185 @@
+SmallTests.dfy(33,11): Error: index out of range

+Execution trace:

+    (0,0): anon0

+SmallTests.dfy(64,36): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+    (0,0): anon12_Then

+SmallTests.dfy(65,51): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+    (0,0): anon12_Else

+    (0,0): anon3

+    (0,0): anon13_Else

+SmallTests.dfy(66,22): Error: target object may be null

+Execution trace:

+    (0,0): anon0

+    (0,0): anon12_Then

+    (0,0): anon3

+    (0,0): anon13_Then

+    (0,0): anon6

+SmallTests.dfy(85,24): Error: target object may be null

+Execution trace:

+    (0,0): anon0

+    SmallTests.dfy(84,5): anon8_LoopHead

+    (0,0): anon8_LoopBody

+    (0,0): anon9_Then

+SmallTests.dfy(119,5): Error: call may violate context's modifies clause

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Else

+    (0,0): anon3

+SmallTests.dfy(132,9): Error: call may violate context's modifies clause

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Then

+SmallTests.dfy(134,9): Error: call may violate context's modifies clause

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

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

+Execution trace:

+    (0,0): anon0

+    (0,0): anon22_Else

+    (0,0): anon24_Else

+    (0,0): anon26_Else

+    (0,0): anon28_Then

+    (0,0): anon29_Then

+    (0,0): anon19

+SmallTests.dfy(198,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Then

+SmallTests.dfy(205,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Else

+    (0,0): anon3

+    (0,0): anon7_Then

+SmallTests.dfy(207,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Else

+    (0,0): anon3

+    (0,0): anon7_Else

+SmallTests.dfy(253,24): Error BP5002: A precondition for this call might not hold.

+SmallTests.dfy(231,30): Related location: This is the precondition that might not hold.

+Execution trace:

+    (0,0): anon0

+    SmallTests.dfy(248,19): anon3_Else

+    (0,0): anon2

+SmallTests.dfy(358,12): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+SmallTests.dfy(368,12): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+SmallTests.dfy(378,6): Error: cannot prove termination; try supplying a decreases clause

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+SmallTests.dfy(682,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    SmallTests.dfy(679,5): anon7_LoopHead

+    (0,0): anon7_LoopBody

+    SmallTests.dfy(679,5): anon8_Else

+    (0,0): anon9_Then

+SmallTests.dfy(703,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon7_Then

+    (0,0): anon8_Then

+    (0,0): anon3

+SmallTests.dfy(288,3): Error BP5003: A postcondition might not hold on this return path.

+SmallTests.dfy(282,11): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+    (0,0): anon18_Else

+    (0,0): anon23_Then

+    (0,0): anon24_Then

+    (0,0): anon15

+    (0,0): anon25_Else

+SmallTests.dfy(329,12): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon8_Then

+    (0,0): anon7

+SmallTests.dfy(336,10): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+SmallTests.dfy(346,4): Error: cannot prove termination; try supplying a decreases clause

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+SmallTests.dfy(390,10): Error BP5003: A postcondition might not hold on this return path.

+SmallTests.dfy(393,41): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Else

+SmallTests.dfy(553,12): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Then

+    (0,0): anon2

+SmallTests.dfy(567,20): Error: left-hand sides 0 and 1 may refer to the same location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon27_Then

+    (0,0): anon28_Then

+    (0,0): anon4

+    (0,0): anon29_Then

+    (0,0): anon30_Then

+    (0,0): anon9

+    (0,0): anon31_Then

+    (0,0): anon32_Then

+    (0,0): anon12

+SmallTests.dfy(569,15): Error: left-hand sides 1 and 2 may refer to the same location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon27_Then

+    SmallTests.dfy(562,18): anon28_Else

+    (0,0): anon4

+    (0,0): anon29_Else

+    (0,0): anon30_Then

+    (0,0): anon9

+    (0,0): anon31_Else

+    (0,0): anon35_Then

+    (0,0): anon36_Then

+    (0,0): anon37_Then

+    (0,0): anon22

+    (0,0): anon38_Then

+SmallTests.dfy(576,25): Error: target object may be null

+Execution trace:

+    (0,0): anon0

+SmallTests.dfy(589,10): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+SmallTests.dfy(613,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+Execution trace:

+    (0,0): anon0

+SmallTests.dfy(636,10): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon8_Then

+    (0,0): anon9_Then

+    (0,0): anon4

+    (0,0): anon10_Then

+    (0,0): anon7

+SmallTests.dfy(650,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+    (0,0): anon6_Then

+    (0,0): anon3

+SmallTests.dfy(652,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Else

+SmallTests.dfy(665,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 87 verified, 33 errors

+

+Dafny program verifier finished with 0 verified, 0 errors