diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-28 16:32:14 +0100 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-05-28 16:32:14 +0100 |
| commit | 08e1dc93d185e221b65bd59ccc167526937ee4d4 (patch) | |
| tree | 5af0f9ea8cc49a34adc45e63f5b1ba4326fc2a13 /Test/stratifiedinline | |
| parent | 68bb2d0882069c9468e7e36c78a0eef710b7c677 (diff) | |
Removed old test infrastructure files except for
./AbsHoudini/
./doomed/
./z3api/
./test17/
because their conversion to lit incomplete.
Diffstat (limited to 'Test/stratifiedinline')
| -rw-r--r-- | Test/stratifiedinline/Answer | 519 | ||||
| -rw-r--r-- | Test/stratifiedinline/runtest.bat | 46 |
2 files changed, 0 insertions, 565 deletions
diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer deleted file mode 100644 index 2a3d7605..00000000 --- a/Test/stratifiedinline/Answer +++ /dev/null @@ -1,519 +0,0 @@ ------ Running regression test bar1.bpl
-(0,0): Error BP5001: This assertion might not hold.
-Execution trace:
- bar1.bpl(24,3): anon0
- Inlined call to procedure foo begins
- bar1.bpl(15,5): anon0
- Inlined call to procedure bar begins
- bar1.bpl(9,5): anon0
- Inlined call to procedure bar ends
- Inlined call to procedure bar begins
- bar1.bpl(9,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
-(0,0): Error BP5001: This assertion might not hold.
-Execution trace:
- bar2.bpl(20,3): anon0
- Inlined call to procedure foo begins
- bar2.bpl(6,3): anon0
- bar2.bpl(7,7): anon3_Then
- Inlined call to procedure foo ends
- Inlined call to procedure foo begins
- bar2.bpl(6,3): anon0
- bar2.bpl(10,7): anon3_Else
- Inlined call to procedure foo ends
-
-Boogie program verifier finished with 0 verified, 1 error
------
------ Running regression test bar3.bpl
-(0,0): Error BP5001: This assertion might not hold.
-Execution trace:
- bar3.bpl(37,3): anon0
- Inlined call to procedure foo begins
- bar3.bpl(20,3): anon0
- bar3.bpl(21,7): anon3_Then
- Inlined call to procedure bar begins
- bar3.bpl(9,3): anon0
- bar3.bpl(10,7): anon3_Then
- Inlined call to procedure bar ends
- Inlined call to procedure bar begins
- bar3.bpl(9,3): anon0
- bar3.bpl(10,7): anon3_Then
- Inlined call to procedure bar ends
- Inlined call to procedure foo ends
- Inlined call to procedure bar begins
- bar3.bpl(9,3): anon0
- bar3.bpl(12,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 bar6.bpl
-
-Boogie program verifier finished with 1 verified, 0 errors
------
------ Running regression test bar7.bpl
-(0,0): Error BP5001: This assertion might not hold.
-Execution trace:
- bar7.bpl(37,5): anon0
- bar7.bpl(39,5): anon4_Then
- Inlined call to procedure foo begins
- bar7.bpl(9,3): anon0
- bar7.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar7.bpl(9,3): anon0
- bar7.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar7.bpl(9,3): anon0
- bar7.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar7.bpl(9,3): anon0
- bar7.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar7.bpl(9,3): anon0
- bar7.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar7.bpl(9,3): anon0
- bar7.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar7.bpl(9,3): anon0
- bar7.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar7.bpl(9,3): anon0
- bar7.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar7.bpl(9,3): anon0
- bar7.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar7.bpl(9,3): anon0
- bar7.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar7.bpl(9,3): anon0
- bar7.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar7.bpl(9,3): anon0
- bar7.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar7.bpl(9,3): anon0
- bar7.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar7.bpl(9,3): anon0
- bar7.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar7.bpl(9,3): anon0
- bar7.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar7.bpl(9,3): anon0
- bar7.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar7.bpl(9,3): anon0
- bar7.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar7.bpl(9,3): anon0
- bar7.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar7.bpl(9,3): anon0
- bar7.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar7.bpl(9,3): anon0
- bar7.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar7.bpl(9,3): anon0
- bar7.bpl(9,3): anon2_Else
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- bar7.bpl(44,3): anon3
-
-Boogie program verifier finished with 0 verified, 1 error
------
------ Running regression test bar8.bpl
-(0,0): Error BP5001: This assertion might not hold.
-Execution trace:
- bar8.bpl(36,5): anon0
- bar8.bpl(38,5): anon4_Then
- Inlined call to procedure foo begins
- bar8.bpl(9,3): anon0
- bar8.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar8.bpl(9,3): anon0
- bar8.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar8.bpl(9,3): anon0
- bar8.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar8.bpl(9,3): anon0
- bar8.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar8.bpl(9,3): anon0
- bar8.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar8.bpl(9,3): anon0
- bar8.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar8.bpl(9,3): anon0
- bar8.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar8.bpl(9,3): anon0
- bar8.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar8.bpl(9,3): anon0
- bar8.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar8.bpl(9,3): anon0
- bar8.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar8.bpl(9,3): anon0
- bar8.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar8.bpl(9,3): anon0
- bar8.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar8.bpl(9,3): anon0
- bar8.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar8.bpl(9,3): anon0
- bar8.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar8.bpl(9,3): anon0
- bar8.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar8.bpl(9,3): anon0
- bar8.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar8.bpl(9,3): anon0
- bar8.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar8.bpl(9,3): anon0
- bar8.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar8.bpl(9,3): anon0
- bar8.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar8.bpl(9,3): anon0
- bar8.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar8.bpl(9,3): anon0
- bar8.bpl(9,3): anon2_Else
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- bar8.bpl(43,3): anon3
-
-Boogie program verifier finished with 0 verified, 1 error
------
------ Running regression test bar9.bpl
-(0,0): Error BP5001: This assertion might not hold.
-Execution trace:
- bar9.bpl(37,5): anon0
- bar9.bpl(43,5): anon4_Else
- Inlined call to procedure bar1 begins
- bar9.bpl(18,3): anon0
- bar9.bpl(20,7): anon2_Then
- Inlined call to procedure bar1 begins
- bar9.bpl(18,3): anon0
- bar9.bpl(20,7): anon2_Then
- Inlined call to procedure bar1 begins
- bar9.bpl(18,3): anon0
- bar9.bpl(20,7): anon2_Then
- Inlined call to procedure bar1 begins
- bar9.bpl(18,3): anon0
- bar9.bpl(20,7): anon2_Then
- Inlined call to procedure bar1 begins
- bar9.bpl(18,3): anon0
- bar9.bpl(20,7): anon2_Then
- Inlined call to procedure bar1 begins
- bar9.bpl(18,3): anon0
- bar9.bpl(20,7): anon2_Then
- Inlined call to procedure bar1 begins
- bar9.bpl(18,3): anon0
- bar9.bpl(20,7): anon2_Then
- Inlined call to procedure bar1 begins
- bar9.bpl(18,3): anon0
- bar9.bpl(20,7): anon2_Then
- Inlined call to procedure bar1 begins
- bar9.bpl(18,3): anon0
- bar9.bpl(20,7): anon2_Then
- Inlined call to procedure bar1 begins
- bar9.bpl(18,3): anon0
- bar9.bpl(20,7): anon2_Then
- Inlined call to procedure bar1 begins
- bar9.bpl(18,3): anon0
- bar9.bpl(20,7): anon2_Then
- Inlined call to procedure bar1 begins
- bar9.bpl(18,3): anon0
- bar9.bpl(20,7): anon2_Then
- Inlined call to procedure bar1 begins
- bar9.bpl(18,3): anon0
- bar9.bpl(20,7): anon2_Then
- Inlined call to procedure bar1 begins
- bar9.bpl(18,3): anon0
- bar9.bpl(20,7): anon2_Then
- Inlined call to procedure bar1 begins
- bar9.bpl(18,3): anon0
- bar9.bpl(20,7): anon2_Then
- Inlined call to procedure bar1 begins
- bar9.bpl(18,3): anon0
- bar9.bpl(20,7): anon2_Then
- Inlined call to procedure bar1 begins
- bar9.bpl(18,3): anon0
- bar9.bpl(20,7): anon2_Then
- Inlined call to procedure bar1 begins
- bar9.bpl(18,3): anon0
- bar9.bpl(20,7): anon2_Then
- Inlined call to procedure bar1 begins
- bar9.bpl(18,3): anon0
- bar9.bpl(20,7): anon2_Then
- Inlined call to procedure bar1 begins
- bar9.bpl(18,3): anon0
- bar9.bpl(20,7): anon2_Then
- Inlined call to procedure bar1 begins
- bar9.bpl(18,3): anon0
- bar9.bpl(18,3): anon2_Else
- Inlined call to procedure bar1 ends
- Inlined call to procedure bar1 ends
- Inlined call to procedure bar1 ends
- Inlined call to procedure bar1 ends
- Inlined call to procedure bar1 ends
- Inlined call to procedure bar1 ends
- Inlined call to procedure bar1 ends
- Inlined call to procedure bar1 ends
- Inlined call to procedure bar1 ends
- Inlined call to procedure bar1 ends
- Inlined call to procedure bar1 ends
- Inlined call to procedure bar1 ends
- Inlined call to procedure bar1 ends
- Inlined call to procedure bar1 ends
- Inlined call to procedure bar1 ends
- Inlined call to procedure bar1 ends
- Inlined call to procedure bar1 ends
- Inlined call to procedure bar1 ends
- Inlined call to procedure bar1 ends
- Inlined call to procedure bar1 ends
- Inlined call to procedure bar1 ends
- Inlined call to procedure bar2 begins
- bar9.bpl(28,3): anon0
- bar9.bpl(29,7): anon2_Then
- Inlined call to procedure bar2 begins
- bar9.bpl(28,3): anon0
- bar9.bpl(29,7): anon2_Then
- Inlined call to procedure bar2 begins
- bar9.bpl(28,3): anon0
- bar9.bpl(29,7): anon2_Then
- Inlined call to procedure bar2 begins
- bar9.bpl(28,3): anon0
- bar9.bpl(29,7): anon2_Then
- Inlined call to procedure bar2 begins
- bar9.bpl(28,3): anon0
- bar9.bpl(29,7): anon2_Then
- Inlined call to procedure bar2 begins
- bar9.bpl(28,3): anon0
- bar9.bpl(29,7): anon2_Then
- Inlined call to procedure bar2 begins
- bar9.bpl(28,3): anon0
- bar9.bpl(29,7): anon2_Then
- Inlined call to procedure bar2 begins
- bar9.bpl(28,3): anon0
- bar9.bpl(29,7): anon2_Then
- Inlined call to procedure bar2 begins
- bar9.bpl(28,3): anon0
- bar9.bpl(29,7): anon2_Then
- Inlined call to procedure bar2 begins
- bar9.bpl(28,3): anon0
- bar9.bpl(29,7): anon2_Then
- Inlined call to procedure bar2 begins
- bar9.bpl(28,3): anon0
- bar9.bpl(28,3): anon2_Else
- Inlined call to procedure bar2 ends
- Inlined call to procedure bar2 ends
- Inlined call to procedure bar2 ends
- Inlined call to procedure bar2 ends
- Inlined call to procedure bar2 ends
- Inlined call to procedure bar2 ends
- Inlined call to procedure bar2 ends
- Inlined call to procedure bar2 ends
- Inlined call to procedure bar2 ends
- Inlined call to procedure bar2 ends
- Inlined call to procedure bar2 ends
- bar9.bpl(46,3): anon3
-
-Boogie program verifier finished with 0 verified, 1 error
------
------ Running regression test bar10.bpl
-(0,0): Error BP5001: This assertion might not hold.
-Execution trace:
- bar10.bpl(37,5): anon0
- Inlined call to procedure bar1 begins
- bar10.bpl(18,3): anon0
- bar10.bpl(18,3): anon2_Else
- Inlined call to procedure bar1 ends
- Inlined call to procedure bar2 begins
- bar10.bpl(28,3): anon0
- bar10.bpl(28,3): anon2_Else
- Inlined call to procedure bar2 ends
- Inlined call to procedure foo begins
- bar10.bpl(9,3): anon0
- bar10.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar10.bpl(9,3): anon0
- bar10.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar10.bpl(9,3): anon0
- bar10.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar10.bpl(9,3): anon0
- bar10.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar10.bpl(9,3): anon0
- bar10.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar10.bpl(9,3): anon0
- bar10.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar10.bpl(9,3): anon0
- bar10.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar10.bpl(9,3): anon0
- bar10.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar10.bpl(9,3): anon0
- bar10.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar10.bpl(9,3): anon0
- bar10.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar10.bpl(9,3): anon0
- bar10.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar10.bpl(9,3): anon0
- bar10.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar10.bpl(9,3): anon0
- bar10.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar10.bpl(9,3): anon0
- bar10.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar10.bpl(9,3): anon0
- bar10.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar10.bpl(9,3): anon0
- bar10.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar10.bpl(9,3): anon0
- bar10.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar10.bpl(9,3): anon0
- bar10.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar10.bpl(9,3): anon0
- bar10.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar10.bpl(9,3): anon0
- bar10.bpl(10,9): anon2_Then
- Inlined call to procedure foo begins
- bar10.bpl(9,3): anon0
- bar10.bpl(9,3): anon2_Else
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
- Inlined call to procedure foo ends
-
-Boogie program verifier finished with 0 verified, 1 error
------
------ Running regression test bar11.bpl
-(0,0): Error BP5001: This assertion might not hold.
-Execution trace:
- bar11.bpl(28,3): anon0
- Inlined call to procedure foo begins
- bar11.bpl(17,3): anon0
- value = 0
- Inlined call to procedure bar begins
- bar11.bpl(10,5): anon0
- value = 1
- Inlined call to procedure bar ends
- Inlined call to procedure bar begins
- bar11.bpl(10,5): anon0
- value = 2
- Inlined call to procedure bar ends
- value = 2
- Inlined call to procedure foo ends
-
-Boogie program verifier finished with 0 verified, 1 error
------
------ Running regression test bar12.bpl
-(0,0): Error BP5001: This assertion might not hold.
-Execution trace:
- bar12.bpl(8,4): anon0
-
-Boogie program verifier finished with 0 verified, 1 error
------
------ Running regression test bar13.bpl
-
-Boogie program verifier finished with 1 verified, 0 errors
------
------ Running regression test large.bpl to test for StackOverflowException
-
-Boogie program verifier finished with 1 verified, 0 errors
------
diff --git a/Test/stratifiedinline/runtest.bat b/Test/stratifiedinline/runtest.bat deleted file mode 100644 index 5e0ab83f..00000000 --- a/Test/stratifiedinline/runtest.bat +++ /dev/null @@ -1,46 +0,0 @@ -@echo off
-setlocal
-
-set BGEXE=..\..\Binaries\Boogie.exe
-rem set BGEXE=mono ..\..\Binaries\Boogie.exe
-
-echo ----- Running regression test bar1.bpl
-%BGEXE% %* /stratifiedInline:1 /vc:i bar1.bpl
-echo -----
-echo ----- Running regression test bar2.bpl
-%BGEXE% %* /stratifiedInline:1 /vc:i bar2.bpl
-echo -----
-echo ----- Running regression test bar3.bpl
-%BGEXE% %* /stratifiedInline:1 /vc:i bar3.bpl
-echo -----
-echo ----- Running regression test bar4.bpl
-%BGEXE% %* /stratifiedInline:1 /vc:i bar4.bpl
-echo -----
-echo ----- Running regression test bar6.bpl
-%BGEXE% %* /stratifiedInline:1 /vc:i bar6.bpl
-echo -----
-echo ----- Running regression test bar7.bpl
-%BGEXE% %* /stratifiedInline:1 /vc:i /nonUniformUnfolding bar7.bpl
-echo -----
-echo ----- Running regression test bar8.bpl
-%BGEXE% %* /stratifiedInline:1 /vc:i /nonUniformUnfolding bar8.bpl
-echo -----
-echo ----- Running regression test bar9.bpl
-%BGEXE% %* /stratifiedInline:1 /vc:i /nonUniformUnfolding bar9.bpl
-echo -----
-echo ----- Running regression test bar10.bpl
-%BGEXE% %* /stratifiedInline:1 /vc:i /nonUniformUnfolding bar10.bpl
-echo -----
-echo ----- Running regression test bar11.bpl
-%BGEXE% %* /stratifiedInline:1 /vc:i bar11.bpl
-echo -----
-echo ----- Running regression test bar12.bpl
-%BGEXE% %* /stratifiedInline:1 /vc:i bar12.bpl
-echo -----
-echo ----- Running regression test bar13.bpl
-%BGEXE% %* /stratifiedInline:1 /vc:i bar13.bpl
-echo -----
-echo ----- Running regression test large.bpl to test for StackOverflowException
-%BGEXE% %* /stratifiedInline:1 /vc:i large.bpl
-echo -----
-
|