summaryrefslogtreecommitdiff
path: root/Test/dafny0/Definedness.dfy.expect
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny0/Definedness.dfy.expect')
-rw-r--r--Test/dafny0/Definedness.dfy.expect110
1 files changed, 53 insertions, 57 deletions
diff --git a/Test/dafny0/Definedness.dfy.expect b/Test/dafny0/Definedness.dfy.expect
index 41073c0e..b5b015ad 100644
--- a/Test/dafny0/Definedness.dfy.expect
+++ b/Test/dafny0/Definedness.dfy.expect
@@ -1,87 +1,87 @@
-Definedness.dfy(11,7): Error: possible division by zero
+Definedness.dfy(11,6): Error: possible division by zero
Execution trace:
(0,0): anon0
- (0,0): anon3_Else
-Definedness.dfy(18,16): Error: possible division by zero
+ (0,0): anon4_Else
+Definedness.dfy(18,15): Error: possible division by zero
Execution trace:
(0,0): anon0
-Definedness.dfy(27,16): Error: target object may be null
+Definedness.dfy(27,15): Error: target object may be null
Execution trace:
(0,0): anon0
-Definedness.dfy(28,21): Error: target object may be null
+Definedness.dfy(28,20): Error: target object may be null
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-Definedness.dfy(29,17): Error: possible division by zero
+Definedness.dfy(29,16): Error: possible division by zero
Execution trace:
(0,0): anon0
-Definedness.dfy(36,16): Error: target object may be null
+Definedness.dfy(36,15): Error: target object may be null
Execution trace:
(0,0): anon0
-Definedness.dfy(45,16): Error: target object may be null
+Definedness.dfy(45,15): Error: target object may be null
Execution trace:
(0,0): anon0
-Definedness.dfy(53,18): Error: target object may be null
+Definedness.dfy(53,17): 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.
+Definedness.dfy(54,2): Error BP5003: A postcondition might not hold on this return path.
+Definedness.dfy(53,21): 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
+Definedness.dfy(60,17): 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.
+Definedness.dfy(61,2): Error BP5003: A postcondition might not hold on this return path.
+Definedness.dfy(60,21): 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.
+Definedness.dfy(68,2): Error BP5003: A postcondition might not hold on this return path.
+Definedness.dfy(67,21): 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
+Definedness.dfy(88,6): 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
+Definedness.dfy(89,4): Error: possible violation of function precondition
+Definedness.dfy(79,15): 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
+Definedness.dfy(89,9): 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
+Definedness.dfy(89,9): 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
+Definedness.dfy(90,9): Error: possible violation of function precondition
+Definedness.dfy(79,15): Related location
Execution trace:
(0,0): anon0
-Definedness.dfy(95,14): Error: possible division by zero
+Definedness.dfy(95,13): Error: possible division by zero
Execution trace:
(0,0): anon0
-Definedness.dfy(95,23): Error: possible division by zero
+Definedness.dfy(95,22): Error: possible division by zero
Execution trace:
(0,0): anon0
-Definedness.dfy(96,15): Error: possible division by zero
+Definedness.dfy(96,14): Error: possible division by zero
Execution trace:
(0,0): anon0
-Definedness.dfy(101,12): Error: possible division by zero
+Definedness.dfy(101,11): Error: possible division by zero
Execution trace:
(0,0): anon0
-Definedness.dfy(108,15): Error: possible division by zero
+Definedness.dfy(108,14): 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
+Definedness.dfy(117,22): Error: possible violation of function precondition
+Definedness.dfy(79,15): 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
+Definedness.dfy(123,16): Error: possible violation of function precondition
+Definedness.dfy(79,15): Related location
Execution trace:
(0,0): anon0
Definedness.dfy(116,5): anon12_LoopHead
@@ -91,30 +91,30 @@ Execution trace:
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
+Definedness.dfy(133,16): Error: possible violation of function precondition
+Definedness.dfy(79,15): 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.
+Definedness.dfy(133,21): 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
+Definedness.dfy(134,16): Error: possible violation of function precondition
+Definedness.dfy(79,15): 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
+Definedness.dfy(143,14): 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
+Definedness.dfy(162,14): Error: possible division by zero
Execution trace:
(0,0): anon0
Definedness.dfy(156,5): anon16_LoopHead
@@ -126,11 +126,11 @@ Execution trace:
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.
+Definedness.dfy(175,27): 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
+Definedness.dfy(181,16): Error: possible violation of function precondition
+Definedness.dfy(79,15): Related location
Execution trace:
(0,0): anon0
Definedness.dfy(173,5): anon18_LoopHead
@@ -142,38 +142,34 @@ Execution trace:
(0,0): anon22_Then
(0,0): anon23_Then
(0,0): anon11
-Definedness.dfy(196,19): Error: possible division by zero
+Definedness.dfy(196,18): 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.
+Definedness.dfy(196,22): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
(0,0): anon0
-Definedness.dfy(196,28): Error: possible division by zero
+Definedness.dfy(196,27): 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.
+Definedness.dfy(215,9): Error BP5003: A postcondition might not hold on this return path.
+Definedness.dfy(217,45): 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
+ (0,0): anon4_Else
+Definedness.dfy(224,21): 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.
+ (0,0): anon4_Then
+Definedness.dfy(237,9): Error BP5003: A postcondition might not hold on this return path.
+Definedness.dfy(240,23): 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
+ (0,0): anon4_Else
Dafny program verifier finished with 21 verified, 37 errors
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-28 21:53:40 +0000