summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-07-16 14:30:43 -0700
committerGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-07-16 14:30:43 -0700
commit34bf8d39390f135c073ef8822fe2896d82b06477 (patch)
treea5e5a57bca108ad4529b27112e1e51ac68cd28f0 /Test
parent9f8cb23ad0662cea28f681872236277c2af2432e (diff)
Minor fixes in .expect files
Diffstat (limited to 'Test')
-rw-r--r--Test/dafny0/SmallTests.dfy.expect46
-rw-r--r--Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy.expect2
2 files changed, 24 insertions, 24 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
diff --git a/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy.expect b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy.expect
index 42fd56a5..c87e2af2 100644
--- a/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy.expect
+++ b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy.expect
@@ -1,2 +1,2 @@
-Dafny program verifier finished with 8 verified, 0 errors
+Dafny program verifier finished with 10 verified, 0 errors