diff options
Diffstat (limited to 'Test/lazyinline/Answer')
| -rw-r--r-- | Test/lazyinline/Answer | 90 |
1 files changed, 57 insertions, 33 deletions
diff --git a/Test/lazyinline/Answer b/Test/lazyinline/Answer index 1feac694..eb3baae3 100644 --- a/Test/lazyinline/Answer +++ b/Test/lazyinline/Answer @@ -2,31 +2,31 @@ bar1.bpl(25,1): Error BP5003: A postcondition might not hold on this return path.
bar1.bpl(21,1): Related location: This is the postcondition that might not hold.
Execution trace:
- bar1.bpl(24,3): anon0
- Inlined call to procedure foo begins
- bar1.bpl(13,5): anon0
- Inlined call to procedure bar begins
- bar1.bpl(7,5): anon0
- Inlined call to procedure bar ends
- Inlined call to procedure bar begins
- bar1.bpl(7,5): anon0
- Inlined call to procedure bar ends
- Inlined call to procedure foo ends
+ bar1.bpl(24,3): anon0
+ Inlined call to procedure foo begins
+ bar1.bpl(13,5): anon0
+ Inlined call to procedure bar begins
+ bar1.bpl(7,5): anon0
+ Inlined call to procedure bar ends
+ Inlined call to procedure bar begins
+ bar1.bpl(7,5): anon0
+ Inlined call to procedure bar ends
+ Inlined call to procedure foo ends
Boogie program verifier finished with 0 verified, 1 error
-----
----- Running regression test bar2.bpl
bar2.bpl(21,3): Error BP5001: This assertion might not hold.
Execution trace:
- bar2.bpl(19,3): anon0
- Inlined call to procedure foo begins
- bar2.bpl(5,3): anon0
- bar2.bpl(6,7): anon3_Then
- Inlined call to procedure foo ends
- Inlined call to procedure foo begins
- bar2.bpl(5,3): anon0
- bar2.bpl(9,7): anon3_Else
- Inlined call to procedure foo ends
+ bar2.bpl(19,3): anon0
+ Inlined call to procedure foo begins
+ bar2.bpl(5,3): anon0
+ bar2.bpl(6,7): anon3_Then
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo begins
+ bar2.bpl(5,3): anon0
+ bar2.bpl(9,7): anon3_Else
+ Inlined call to procedure foo ends
Boogie program verifier finished with 0 verified, 1 error
-----
@@ -34,23 +34,23 @@ Boogie program verifier finished with 0 verified, 1 error bar3.bpl(41,1): Error BP5003: A postcondition might not hold on this return path.
bar3.bpl(34,1): Related location: This is the postcondition that might not hold.
Execution trace:
- bar3.bpl(38,3): anon0
- Inlined call to procedure foo begins
- bar3.bpl(18,3): anon0
- bar3.bpl(19,7): anon3_Then
- Inlined call to procedure bar begins
- bar3.bpl(7,3): anon0
- bar3.bpl(8,7): anon3_Then
- Inlined call to procedure bar ends
- Inlined call to procedure bar begins
- bar3.bpl(7,3): anon0
- bar3.bpl(8,7): anon3_Then
- Inlined call to procedure bar ends
- Inlined call to procedure foo ends
+ bar3.bpl(38,3): anon0
+ Inlined call to procedure foo begins
+ bar3.bpl(18,3): anon0
+ bar3.bpl(19,7): anon3_Then
Inlined call to procedure bar begins
bar3.bpl(7,3): anon0
- bar3.bpl(10,7): anon3_Else
+ bar3.bpl(8,7): anon3_Then
Inlined call to procedure bar ends
+ Inlined call to procedure bar begins
+ bar3.bpl(7,3): anon0
+ bar3.bpl(8,7): anon3_Then
+ Inlined call to procedure bar ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure bar begins
+ bar3.bpl(7,3): anon0
+ bar3.bpl(10,7): anon3_Else
+ Inlined call to procedure bar ends
Boogie program verifier finished with 0 verified, 1 error
-----
@@ -58,10 +58,34 @@ Boogie program verifier finished with 0 verified, 1 error Boogie program verifier finished with 1 verified, 0 errors
-----
+----- Running regression test bar5.bpl
+(0,0): Error BP5001: This assertion might not hold.
+Execution trace:
+ bar5.bpl(24,3): anon0
+ Inlined call to procedure foo begins
+ bar5.bpl(13,5): anon0
+ Inlined call to procedure foo ends
+
+Boogie program verifier finished with 0 verified, 1 error
+-----
----- Running regression test bar6.bpl
Boogie program verifier finished with 1 verified, 0 errors
-----
+----- Running regression test bar7.bpl
+
+Boogie program verifier finished with 1 verified, 0 errors
+-----
+----- Running regression test bar8.bpl
+(0,0): Error BP5001: This assertion might not hold.
+Execution trace:
+ bar8.bpl(13,5): anon0
+ Inlined call to procedure foo begins
+ bar8.bpl(6,3): anon0
+ Inlined call to procedure foo ends
+
+Boogie program verifier finished with 0 verified, 1 error
+-----
----- Running regression test foo.bpl
Boogie program verifier finished with 2 verified, 0 errors
|