summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar Dan Liew <daniel.liew@imperial.ac.uk>2014-05-10 15:35:07 +0100
committerGravatar Dan Liew <daniel.liew@imperial.ac.uk>2014-05-10 15:35:07 +0100
commit88a5ed2e9a79118fa45f195360aa10597a182fec (patch)
treefd3fd1ef1a6956616e3a42dc55adf0aaa394ee5c /Test
parent631da48e5bffbdd66ac6f076a8beb120385addfa (diff)
Unbreak the tests in test2 for batch file testing infrastructure
Diffstat (limited to 'Test')
-rw-r--r--Test/test2/Answer40
1 files changed, 20 insertions, 20 deletions
diff --git a/Test/test2/Answer b/Test/test2/Answer
index 5d446e64..9403e6a9 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -81,14 +81,14 @@ OldIllegal.bpl(16,23): Error: old expressions allowed only in two-state contexts
2 name resolution errors detected in OldIllegal.bpl
-------------------- Arrays.bpl --------------------
-Arrays.bpl(48,5): Error BP5003: A postcondition might not hold on this return path.
-Arrays.bpl(40,3): Related location: This is the postcondition that might not hold.
+Arrays.bpl(50,5): Error BP5003: A postcondition might not hold on this return path.
+Arrays.bpl(42,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Arrays.bpl(44,3): start
-Arrays.bpl(129,5): Error BP5003: A postcondition might not hold on this return path.
-Arrays.bpl(121,3): Related location: This is the postcondition that might not hold.
+ Arrays.bpl(46,3): start
+Arrays.bpl(131,5): Error BP5003: A postcondition might not hold on this return path.
+Arrays.bpl(123,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Arrays.bpl(125,3): start
+ Arrays.bpl(127,3): start
Boogie program verifier finished with 8 verified, 2 errors
@@ -362,12 +362,12 @@ Execution trace:
Boogie program verifier finished with 2 verified, 2 errors
-------------------- Lambda.bpl --------------------
-Lambda.bpl(39,3): Error BP5001: This assertion might not hold.
+Lambda.bpl(41,3): Error BP5001: This assertion might not hold.
Execution trace:
- Lambda.bpl(38,5): anon0
-Lambda.bpl(40,3): Error BP5001: This assertion might not hold.
+ Lambda.bpl(40,5): anon0
+Lambda.bpl(42,3): Error BP5001: This assertion might not hold.
Execution trace:
- Lambda.bpl(38,5): anon0
+ Lambda.bpl(40,5): anon0
Boogie program verifier finished with 6 verified, 2 errors
@@ -447,24 +447,24 @@ Execution trace:
Boogie program verifier finished with 1 verified, 3 errors
-------------------- Arrays.bpl /typeEncoding:m --------------------
-Arrays.bpl(48,5): Error BP5003: A postcondition might not hold on this return path.
-Arrays.bpl(40,3): Related location: This is the postcondition that might not hold.
+Arrays.bpl(50,5): Error BP5003: A postcondition might not hold on this return path.
+Arrays.bpl(42,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Arrays.bpl(44,3): start
-Arrays.bpl(129,5): Error BP5003: A postcondition might not hold on this return path.
-Arrays.bpl(121,3): Related location: This is the postcondition that might not hold.
+ Arrays.bpl(46,3): start
+Arrays.bpl(131,5): Error BP5003: A postcondition might not hold on this return path.
+Arrays.bpl(123,3): Related location: This is the postcondition that might not hold.
Execution trace:
- Arrays.bpl(125,3): start
+ Arrays.bpl(127,3): start
Boogie program verifier finished with 8 verified, 2 errors
-------------------- Lambda.bpl /typeEncoding:m --------------------
-Lambda.bpl(39,3): Error BP5001: This assertion might not hold.
+Lambda.bpl(41,3): Error BP5001: This assertion might not hold.
Execution trace:
- Lambda.bpl(38,5): anon0
-Lambda.bpl(40,3): Error BP5001: This assertion might not hold.
+ Lambda.bpl(40,5): anon0
+Lambda.bpl(42,3): Error BP5001: This assertion might not hold.
Execution trace:
- Lambda.bpl(38,5): anon0
+ Lambda.bpl(40,5): anon0
Boogie program verifier finished with 6 verified, 2 errors