Set up the same test infrastructure as in Boogie.

1 files changed, 179 insertions, 0 deletions

diff --git a/Test/dafny0/Definedness.dfy.expect b/Test/dafny0/Definedness.dfy.expect
new file mode 100644
index 00000000..41073c0e
--- /dev/null
+++ b/Test/dafny0/Definedness.dfy.expect
@@ -0,0 +1,179 @@
+Definedness.dfy(11,7): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+Definedness.dfy(18,16): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+Definedness.dfy(27,16): Error: target object may be null

+Execution trace:

+    (0,0): anon0

+Definedness.dfy(28,21): Error: target object may be null

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Then

+Definedness.dfy(29,17): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+Definedness.dfy(36,16): Error: target object may be null

+Execution trace:

+    (0,0): anon0

+Definedness.dfy(45,16): Error: target object may be null

+Execution trace:

+    (0,0): anon0

+Definedness.dfy(53,18): Error: target object may be null

+Execution trace:

+    (0,0): anon0

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

+Definedness.dfy(53,22): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+Definedness.dfy(60,18): Error: target object may be null

+Execution trace:

+    (0,0): anon0

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

+Definedness.dfy(60,22): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

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

+Definedness.dfy(67,22): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+Definedness.dfy(88,7): Error: target object may be null

+Execution trace:

+    (0,0): anon0

+Definedness.dfy(89,5): Error: possible violation of function precondition

+Definedness.dfy(79,16): Related location

+Execution trace:

+    (0,0): anon0

+Definedness.dfy(89,10): Error: assignment may update an object not in the enclosing context's modifies clause

+Execution trace:

+    (0,0): anon0

+Definedness.dfy(89,10): Error: target object may be null

+Execution trace:

+    (0,0): anon0

+Definedness.dfy(90,10): Error: possible violation of function precondition

+Definedness.dfy(79,16): Related location

+Execution trace:

+    (0,0): anon0

+Definedness.dfy(95,14): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+Definedness.dfy(95,23): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+Definedness.dfy(96,15): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+Definedness.dfy(101,12): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+Definedness.dfy(108,15): Error: possible division by zero

+Execution trace:

+    Definedness.dfy(108,5): anon7_LoopHead

+    (0,0): anon7_LoopBody

+    Definedness.dfy(108,5): anon8_Else

+Definedness.dfy(117,23): Error: possible violation of function precondition

+Definedness.dfy(79,16): Related location

+Execution trace:

+    (0,0): anon0

+    Definedness.dfy(116,5): anon12_LoopHead

+    (0,0): anon12_LoopBody

+    (0,0): anon13_Then

+Definedness.dfy(123,17): Error: possible violation of function precondition

+Definedness.dfy(79,16): Related location

+Execution trace:

+    (0,0): anon0

+    Definedness.dfy(116,5): anon12_LoopHead

+    (0,0): anon12_LoopBody

+    Definedness.dfy(116,5): anon13_Else

+    (0,0): anon14_Then

+    Definedness.dfy(122,5): anon15_LoopHead

+    (0,0): anon15_LoopBody

+    (0,0): anon16_Then

+Definedness.dfy(133,17): Error: possible violation of function precondition

+Definedness.dfy(79,16): Related location

+Execution trace:

+    (0,0): anon0

+    Definedness.dfy(132,5): anon6_LoopHead

+    (0,0): anon6_LoopBody

+    (0,0): anon7_Then

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

+Execution trace:

+    (0,0): anon0

+Definedness.dfy(134,17): Error: possible violation of function precondition

+Definedness.dfy(79,16): Related location

+Execution trace:

+    (0,0): anon0

+    Definedness.dfy(132,5): anon6_LoopHead

+    (0,0): anon6_LoopBody

+    (0,0): anon7_Then

+Definedness.dfy(143,15): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+    Definedness.dfy(143,5): anon8_LoopHead

+    (0,0): anon8_LoopBody

+    Definedness.dfy(143,5): anon9_Else

+Definedness.dfy(162,15): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+    Definedness.dfy(156,5): anon16_LoopHead

+    (0,0): anon16_LoopBody

+    Definedness.dfy(156,5): anon17_Else

+    (0,0): anon18_Then

+    (0,0): anon5

+    (0,0): anon19_Then

+    Definedness.dfy(162,5): anon20_LoopHead

+    (0,0): anon20_LoopBody

+    Definedness.dfy(162,5): anon21_Else

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

+Execution trace:

+    (0,0): anon0

+Definedness.dfy(181,17): Error: possible violation of function precondition

+Definedness.dfy(79,16): Related location

+Execution trace:

+    (0,0): anon0

+    Definedness.dfy(173,5): anon18_LoopHead

+    (0,0): anon18_LoopBody

+    Definedness.dfy(173,5): anon19_Else

+    (0,0): anon20_Then

+    Definedness.dfy(180,5): anon21_LoopHead

+    (0,0): anon21_LoopBody

+    (0,0): anon22_Then

+    (0,0): anon23_Then

+    (0,0): anon11

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

+Execution trace:

+    (0,0): anon0

+    Definedness.dfy(194,5): anon6_LoopHead

+    (0,0): anon6_LoopBody

+    (0,0): anon7_Then

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

+Execution trace:

+    (0,0): anon0

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

+Execution trace:

+    (0,0): anon0

+    Definedness.dfy(194,5): anon6_LoopHead

+    (0,0): anon6_LoopBody

+    (0,0): anon7_Then

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

+Definedness.dfy(217,46): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Else

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

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+    (0,0): anon2

+    (0,0): anon6_Then

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

+Definedness.dfy(240,24): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+    (0,0): anon7_Then

+    (0,0): anon2

+    (0,0): anon8_Else

+

+Dafny program verifier finished with 21 verified, 37 errors