summaryrefslogtreecommitdiff
path: root/Test/dafny0/SmallTests.dfy.expect
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny0/SmallTests.dfy.expect')
-rw-r--r--Test/dafny0/SmallTests.dfy.expect109
1 files changed, 55 insertions, 54 deletions
diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect
index 5f766cd6..746e978a 100644
--- a/Test/dafny0/SmallTests.dfy.expect
+++ b/Test/dafny0/SmallTests.dfy.expect
@@ -1,43 +1,42 @@
-SmallTests.dfy(33,11): Error: index out of range
+SmallTests.dfy(507,4): Warning: /!\ No trigger covering all quantified variables found.
+SmallTests.dfy(34,10): Error: index out of range
Execution trace:
(0,0): anon0
-SmallTests.dfy(64,36): Error: possible division by zero
+SmallTests.dfy(65,35): Error: possible division by zero
Execution trace:
(0,0): anon0
- (0,0): anon12_Then
-SmallTests.dfy(65,51): Error: possible division by zero
+ (0,0): anon13_Then
+SmallTests.dfy(66,50): 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
+ (0,0): anon14_Else
+SmallTests.dfy(67,21): 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
+ (0,0): anon14_Then
+ (0,0): anon15_Then
+SmallTests.dfy(86,23): Error: target object may be null
Execution trace:
(0,0): anon0
- SmallTests.dfy(84,5): anon8_LoopHead
+ SmallTests.dfy(85,5): anon8_LoopHead
(0,0): anon8_LoopBody
(0,0): anon9_Then
-SmallTests.dfy(119,6): Error: call may violate context's modifies clause
+SmallTests.dfy(120,5): Error: call may violate context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon4_Else
(0,0): anon3
-SmallTests.dfy(132,10): Error: call may violate context's modifies clause
+SmallTests.dfy(133,9): Error: call may violate context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-SmallTests.dfy(134,10): Error: call may violate context's modifies clause
+SmallTests.dfy(135,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
+SmallTests.dfy(175,8): Error: assignment may update an object field not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon22_Else
@@ -46,23 +45,23 @@ Execution trace:
(0,0): anon28_Then
(0,0): anon29_Then
(0,0): anon19
-SmallTests.dfy(198,14): Error: assertion violation
+SmallTests.dfy(199,13): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon9_Then
-SmallTests.dfy(205,14): Error: assertion violation
+SmallTests.dfy(206,13): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon9_Else
(0,0): anon3
(0,0): anon10_Then
-SmallTests.dfy(207,14): Error: assertion violation
+SmallTests.dfy(208,13): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon9_Else
(0,0): anon3
(0,0): anon10_Else
-SmallTests.dfy(212,14): Error: assertion violation
+SmallTests.dfy(213,13): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon9_Else
@@ -70,7 +69,7 @@ Execution trace:
(0,0): anon10_Then
(0,0): anon6
(0,0): anon11_Then
-SmallTests.dfy(214,14): Error: assertion violation
+SmallTests.dfy(215,13): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon9_Else
@@ -78,37 +77,38 @@ Execution trace:
(0,0): anon10_Then
(0,0): anon6
(0,0): anon11_Else
-SmallTests.dfy(260,24): Error BP5002: A precondition for this call might not hold.
-SmallTests.dfy(238,30): Related location: This is the precondition that might not hold.
+SmallTests.dfy(261,23): Error BP5002: A precondition for this call might not hold.
+SmallTests.dfy(239,29): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
- SmallTests.dfy(255,19): anon3_Else
+ SmallTests.dfy(256,19): anon3_Else
(0,0): anon2
-SmallTests.dfy(365,12): Error: assertion violation
+SmallTests.dfy(367,11): Error: assertion violation
Execution trace:
(0,0): anon0
-SmallTests.dfy(375,12): Error: assertion violation
+SmallTests.dfy(377,11): Error: assertion violation
Execution trace:
(0,0): anon0
-SmallTests.dfy(385,6): Error: cannot prove termination; try supplying a decreases clause
+SmallTests.dfy(387,5): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
- (0,0): anon3_Else
-SmallTests.dfy(690,14): Error: assertion violation
+ (0,0): anon4_Else
+SmallTests.dfy(692,13): Error: assertion violation
Execution trace:
(0,0): anon0
- SmallTests.dfy(687,5): anon7_LoopHead
+ SmallTests.dfy(689,5): anon7_LoopHead
(0,0): anon7_LoopBody
- SmallTests.dfy(687,5): anon8_Else
+ SmallTests.dfy(689,5): anon8_Else
(0,0): anon9_Then
-SmallTests.dfy(711,14): Error: assertion violation
+SmallTests.dfy(713,13): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon7_Then
(0,0): anon8_Then
(0,0): anon3
-SmallTests.dfy(295,3): Error BP5003: A postcondition might not hold on this return path.
-SmallTests.dfy(289,11): Related location: This is the postcondition that might not hold.
+SmallTests.dfy(296,2): Error BP5003: A postcondition might not hold on this return path.
+SmallTests.dfy(290,10): Related location: This is the postcondition that might not hold.
+SmallTests.dfy(290,40): Related location
Execution trace:
(0,0): anon0
(0,0): anon18_Else
@@ -116,29 +116,29 @@ Execution trace:
(0,0): anon24_Then
(0,0): anon15
(0,0): anon25_Else
-SmallTests.dfy(336,12): Error: assertion violation
+SmallTests.dfy(338,11): Error: assertion violation
Execution trace:
(0,0): anon0
- (0,0): anon8_Then
- (0,0): anon7
-SmallTests.dfy(343,10): Error: assertion violation
+ (0,0): anon7_Then
+ (0,0): anon6
+SmallTests.dfy(345,9): Error: assertion violation
Execution trace:
(0,0): anon0
-SmallTests.dfy(353,4): Error: cannot prove termination; try supplying a decreases clause
+SmallTests.dfy(355,3): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
- (0,0): anon3_Else
-SmallTests.dfy(397,10): Error BP5003: A postcondition might not hold on this return path.
-SmallTests.dfy(400,41): Related location: This is the postcondition that might not hold.
+ (0,0): anon4_Else
+SmallTests.dfy(399,9): Error BP5003: A postcondition might not hold on this return path.
+SmallTests.dfy(402,40): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
- (0,0): anon6_Else
-SmallTests.dfy(561,12): Error: assertion violation
+ (0,0): anon7_Else
+SmallTests.dfy(563,11): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
(0,0): anon2
-SmallTests.dfy(575,20): Error: left-hand sides 0 and 1 may refer to the same location
+SmallTests.dfy(577,19): Error: left-hand sides 0 and 1 may refer to the same location
Execution trace:
(0,0): anon0
(0,0): anon27_Then
@@ -150,11 +150,11 @@ Execution trace:
(0,0): anon31_Then
(0,0): anon32_Then
(0,0): anon12
-SmallTests.dfy(577,15): Error: left-hand sides 1 and 2 may refer to the same location
+SmallTests.dfy(579,14): Error: left-hand sides 1 and 2 may refer to the same location
Execution trace:
(0,0): anon0
(0,0): anon27_Then
- SmallTests.dfy(570,18): anon28_Else
+ SmallTests.dfy(572,18): anon28_Else
(0,0): anon4
(0,0): anon29_Else
(0,0): anon30_Then
@@ -165,16 +165,16 @@ Execution trace:
(0,0): anon37_Then
(0,0): anon22
(0,0): anon38_Then
-SmallTests.dfy(584,25): Error: target object may be null
+SmallTests.dfy(586,24): Error: target object may be null
Execution trace:
(0,0): anon0
-SmallTests.dfy(597,10): Error: assertion violation
+SmallTests.dfy(599,9): Error: assertion violation
Execution trace:
(0,0): anon0
-SmallTests.dfy(621,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
+SmallTests.dfy(623,4): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
Execution trace:
(0,0): anon0
-SmallTests.dfy(644,23): Error: assertion violation
+SmallTests.dfy(646,22): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon8_Then
@@ -182,20 +182,21 @@ Execution trace:
(0,0): anon4
(0,0): anon10_Then
(0,0): anon7
-SmallTests.dfy(658,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
+SmallTests.dfy(660,9): 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(660,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
+SmallTests.dfy(662,9): 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(673,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
+SmallTests.dfy(675,8): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
Execution trace:
(0,0): anon0
Dafny program verifier finished with 104 verified, 35 errors
+SmallTests.dfy.tmp.dprint.dfy(369,4): Warning: /!\ No trigger covering all quantified variables found.
Dafny program verifier finished with 0 verified, 0 errors
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-29 05:58:43 +0000