diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-07-16 14:30:43 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-07-16 14:30:43 -0700 |
| commit | 34bf8d39390f135c073ef8822fe2896d82b06477 (patch) | |
| tree | a5e5a57bca108ad4529b27112e1e51ac68cd28f0 /Test/dafny0/SmallTests.dfy.expect | |
| parent | 9f8cb23ad0662cea28f681872236277c2af2432e (diff) | |
Minor fixes in .expect files
Diffstat (limited to 'Test/dafny0/SmallTests.dfy.expect')
| -rw-r--r-- | Test/dafny0/SmallTests.dfy.expect | 46 |
1 files changed, 23 insertions, 23 deletions
diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect index 3df8118a..b0605d8e 100644 --- a/Test/dafny0/SmallTests.dfy.expect +++ b/Test/dafny0/SmallTests.dfy.expect @@ -82,24 +82,24 @@ Execution trace: (0,0): anon0
SmallTests.dfy(256,19): anon3_Else
(0,0): anon2
-SmallTests.dfy(366,12): Error: assertion violation
+SmallTests.dfy(367,12): Error: assertion violation
Execution trace:
(0,0): anon0
-SmallTests.dfy(376,12): Error: assertion violation
+SmallTests.dfy(377,12): Error: assertion violation
Execution trace:
(0,0): anon0
-SmallTests.dfy(386,6): Error: cannot prove termination; try supplying a decreases clause
+SmallTests.dfy(387,6): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-SmallTests.dfy(691,14): Error: assertion violation
+SmallTests.dfy(692,14): Error: assertion violation
Execution trace:
(0,0): anon0
- SmallTests.dfy(688,5): anon7_LoopHead
+ SmallTests.dfy(689,5): anon7_LoopHead
(0,0): anon7_LoopBody
- SmallTests.dfy(688,5): anon8_Else
+ SmallTests.dfy(689,5): anon8_Else
(0,0): anon9_Then
-SmallTests.dfy(712,14): Error: assertion violation
+SmallTests.dfy(713,14): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon7_Then
@@ -114,29 +114,29 @@ Execution trace: (0,0): anon24_Then
(0,0): anon15
(0,0): anon25_Else
-SmallTests.dfy(337,12): Error: assertion violation
+SmallTests.dfy(338,12): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon8_Then
(0,0): anon7
-SmallTests.dfy(344,10): Error: assertion violation
+SmallTests.dfy(345,10): Error: assertion violation
Execution trace:
(0,0): anon0
-SmallTests.dfy(354,4): Error: cannot prove termination; try supplying a decreases clause
+SmallTests.dfy(355,4): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-SmallTests.dfy(398,10): Error BP5003: A postcondition might not hold on this return path.
-SmallTests.dfy(401,41): Related location: This is the postcondition that might not hold.
+SmallTests.dfy(399,10): Error BP5003: A postcondition might not hold on this return path.
+SmallTests.dfy(402,41): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon7_Else
-SmallTests.dfy(562,12): Error: assertion violation
+SmallTests.dfy(563,12): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
(0,0): anon2
-SmallTests.dfy(576,20): Error: left-hand sides 0 and 1 may refer to the same location
+SmallTests.dfy(577,20): Error: left-hand sides 0 and 1 may refer to the same location
Execution trace:
(0,0): anon0
(0,0): anon27_Then
@@ -148,11 +148,11 @@ Execution trace: (0,0): anon31_Then
(0,0): anon32_Then
(0,0): anon12
-SmallTests.dfy(578,15): Error: left-hand sides 1 and 2 may refer to the same location
+SmallTests.dfy(579,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(571,18): anon28_Else
+ SmallTests.dfy(572,18): anon28_Else
(0,0): anon4
(0,0): anon29_Else
(0,0): anon30_Then
@@ -163,16 +163,16 @@ Execution trace: (0,0): anon37_Then
(0,0): anon22
(0,0): anon38_Then
-SmallTests.dfy(585,25): Error: target object may be null
+SmallTests.dfy(586,25): Error: target object may be null
Execution trace:
(0,0): anon0
-SmallTests.dfy(598,10): Error: assertion violation
+SmallTests.dfy(599,10): Error: assertion violation
Execution trace:
(0,0): anon0
-SmallTests.dfy(622,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
+SmallTests.dfy(623,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
Execution trace:
(0,0): anon0
-SmallTests.dfy(645,23): Error: assertion violation
+SmallTests.dfy(646,23): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon8_Then
@@ -180,17 +180,17 @@ Execution trace: (0,0): anon4
(0,0): anon10_Then
(0,0): anon7
-SmallTests.dfy(659,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
+SmallTests.dfy(660,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(661,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
+SmallTests.dfy(662,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(674,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
+SmallTests.dfy(675,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
Execution trace:
(0,0): anon0
|