diff options
| author |  qadeer <qadeer@microsoft.com> | 2012-04-28 11:16:59 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2012-04-28 11:16:59 -0700 |
| commit | cbdf99d0162f27eeeae8b4aae1af9a4721fa74c6 (patch) | |
| tree | 91a2c1c01d72575e700abd64ec6f0fc6322ed082 /Test/lazyinline/Answer | |
| parent | 271e771e41773a9420fcdaf82579b5e1733f450e (diff) | |
removed the lazy inline test directory
Diffstat (limited to 'Test/lazyinline/Answer')
| -rw-r--r-- | Test/lazyinline/Answer | 92 |
1 files changed, 0 insertions, 92 deletions
diff --git a/Test/lazyinline/Answer b/Test/lazyinline/Answer deleted file mode 100644 index eb3baae3..00000000 --- a/Test/lazyinline/Answer +++ /dev/null @@ -1,92 +0,0 @@ ------ Running regression test bar1.bpl
-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
-
-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
-
-Boogie program verifier finished with 0 verified, 1 error
------
------ Running regression test bar3.bpl
-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
- 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
------
------ Running regression test bar4.bpl
-
-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
------
|