From 08e1dc93d185e221b65bd59ccc167526937ee4d4 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 28 May 2014 16:32:14 +0100 Subject: Removed old test infrastructure files except for ./AbsHoudini/ ./doomed/ ./z3api/ ./test17/ because their conversion to lit incomplete. --- Test/stratifiedinline/Answer | 519 -------------------------------------- Test/stratifiedinline/runtest.bat | 46 ---- 2 files changed, 565 deletions(-) delete mode 100644 Test/stratifiedinline/Answer delete mode 100644 Test/stratifiedinline/runtest.bat (limited to 'Test/stratifiedinline') 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 ----- - -- cgit v1.2.3