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/bitvectors/Answer | 51 --------------------------------------------- Test/bitvectors/runtest.bat | 17 --------------- 2 files changed, 68 deletions(-) delete mode 100644 Test/bitvectors/Answer delete mode 100644 Test/bitvectors/runtest.bat (limited to 'Test/bitvectors') diff --git a/Test/bitvectors/Answer b/Test/bitvectors/Answer deleted file mode 100644 index 6aa2bce2..00000000 --- a/Test/bitvectors/Answer +++ /dev/null @@ -1,51 +0,0 @@ --------------------- arrays.bpl -------------------- - -Boogie program verifier finished with 2 verified, 0 errors --------------------- bv0.bpl -------------------- -bv0.bpl(6,3): Error: mismatched types in assignment command (cannot assign bv31 to bv32) -bv0.bpl(7,3): Error: mismatched types in assignment command (cannot assign int to bv32) -bv0.bpl(8,4): Error: mismatched types in assignment command (cannot assign bv1 to bv32) -bv0.bpl(9,10): Error: start index in extract must be no bigger than the end index -bv0.bpl(10,4): Error: mismatched types in assignment command (cannot assign bv1 to bv32) -bv0.bpl(11,4): Error: mismatched types in assignment command (cannot assign bv1 to bv32) -bv0.bpl(12,4): Error: mismatched types in assignment command (cannot assign concat$bvproxy#10 to bv32) -7 type checking errors detected in bv0.bpl --------------------- bv1.bpl -------------------- - -Boogie program verifier finished with 1 verified, 0 errors --------------------- bv2.bpl -------------------- -bv2.bpl(6,13): Error: bitvector bounds in illegal position -bv2.bpl(8,13): Error: undeclared type: x -bv2.bpl(9,14): Error: bitvector bounds in illegal position -3 name resolution errors detected in bv2.bpl --------------------- bv3.bpl -------------------- -bv3.bpl(4,5): Error: type name: bv16 is registered for bitvectors -1 name resolution errors detected in bv3.bpl --------------------- bv4.bpl -------------------- - -Boogie program verifier finished with 1 verified, 0 errors --------------------- bv7.bpl -------------------- -bv7.bpl(6,14): error: arguments of extract need to be integer literals -bv7.bpl(7,15): error: parentheses around bitvector bounds are not allowed -2 parse errors detected in bv7.bpl --------------------- bv5.bpl -------------------- -bv5.bpl(12,3): Error BP5001: This assertion might not hold. -Execution trace: - bv5.bpl(7,12): anon0 - -Boogie program verifier finished with 0 verified, 1 error --------------------- bv6.bpl -------------------- -bv6.bpl(10,3): Error BP5001: This assertion might not hold. -Execution trace: - bv6.bpl(7,5): anon0 - -Boogie program verifier finished with 0 verified, 1 error --------------------- bv8.bpl -------------------- - -Boogie program verifier finished with 2 verified, 0 errors --------------------- bv10.bpl -------------------- - -Boogie program verifier finished with 1 verified, 0 errors --------------------- bv9.bpl /proverOpt:OPTIMIZE_FOR_BV=true -------------------- - -Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/bitvectors/runtest.bat b/Test/bitvectors/runtest.bat deleted file mode 100644 index 2a140368..00000000 --- a/Test/bitvectors/runtest.bat +++ /dev/null @@ -1,17 +0,0 @@ -@echo off -setlocal - -set BGEXE=..\..\Binaries\Boogie.exe - -for %%f in (arrays.bpl bv0.bpl bv1.bpl bv2.bpl bv3.bpl bv4.bpl bv7.bpl) do ( - echo -------------------- %%f -------------------- - %BGEXE% /proverWarnings:1 %* %%f -) - -for %%f in (bv5.bpl bv6.bpl bv8.bpl bv10.bpl) do ( - echo -------------------- %%f -------------------- - %BGEXE% %* %%f -) - -echo -------------------- bv9.bpl /proverOpt:OPTIMIZE_FOR_BV=true -------------------- -%BGEXE% /proverOpt:OPTIMIZE_FOR_BV=true %* bv9.bpl -- cgit v1.2.3