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/test7 | |
| parent | 68bb2d0882069c9468e7e36c78a0eef710b7c677 (diff) | |
Removed old test infrastructure files except for
./AbsHoudini/
./doomed/
./z3api/
./test17/
because their conversion to lit incomplete.
Diffstat (limited to 'Test/test7')
| -rw-r--r-- | Test/test7/Answer | 64 | ||||
| -rw-r--r-- | Test/test7/runtest.bat | 34 |
2 files changed, 0 insertions, 98 deletions
diff --git a/Test/test7/Answer b/Test/test7/Answer deleted file mode 100644 index 00b9069f..00000000 --- a/Test/test7/Answer +++ /dev/null @@ -1,64 +0,0 @@ ------------------------------- NestedVC.bpl ---------------------
-NestedVC.bpl(17,4): Error BP5001: This assertion might not hold.
-Execution trace:
- NestedVC.bpl(16,1): A
- NestedVC.bpl(17,1): B
-
-Boogie program verifier finished with 1 verified, 1 error
------------------------------- UnreachableBlocks.bpl ---------------------
-
-Boogie program verifier finished with 4 verified, 0 errors
------------------------------- MultipleErrors.bpl ---------------------
-
------ /vc:block
-MultipleErrors.bpl(28,3): Error BP5001: This assertion might not hold.
-Execution trace:
- MultipleErrors.bpl(24,1): start
- MultipleErrors.bpl(27,1): A
-
-Boogie program verifier finished with 0 verified, 1 error
-
------ /vc:local
-MultipleErrors.bpl(32,3): Error BP5001: This assertion might not hold.
-Execution trace:
- MultipleErrors.bpl(31,1): B
-
-Boogie program verifier finished with 0 verified, 1 error
-
------ /vc:dag
-MultipleErrors.bpl(28,3): Error BP5001: This assertion might not hold.
-Execution trace:
- MultipleErrors.bpl(24,1): start
- MultipleErrors.bpl(27,1): A
-
-Boogie program verifier finished with 0 verified, 1 error
-
------ /errorLimit:10 /vc:local
-MultipleErrors.bpl(28,3): Error BP5001: This assertion might not hold.
-Execution trace:
- MultipleErrors.bpl(27,1): A
-MultipleErrors.bpl(32,3): Error BP5001: This assertion might not hold.
-Execution trace:
- MultipleErrors.bpl(31,1): B
-MultipleErrors.bpl(36,3): Error BP5001: This assertion might not hold.
-Execution trace:
- MultipleErrors.bpl(35,1): C
-
-Boogie program verifier finished with 0 verified, 3 errors
-
------ /errorLimit:10 /vc:dag
-MultipleErrors.bpl(28,3): Error BP5001: This assertion might not hold.
-Execution trace:
- MultipleErrors.bpl(24,1): start
- MultipleErrors.bpl(27,1): A
-MultipleErrors.bpl(32,3): Error BP5001: This assertion might not hold.
-Execution trace:
- MultipleErrors.bpl(24,1): start
- MultipleErrors.bpl(31,1): B
-MultipleErrors.bpl(36,3): Error BP5001: This assertion might not hold.
-Execution trace:
- MultipleErrors.bpl(24,1): start
- MultipleErrors.bpl(27,1): A
- MultipleErrors.bpl(35,1): C
-
-Boogie program verifier finished with 0 verified, 3 errors
diff --git a/Test/test7/runtest.bat b/Test/test7/runtest.bat deleted file mode 100644 index 8da87233..00000000 --- a/Test/test7/runtest.bat +++ /dev/null @@ -1,34 +0,0 @@ -@echo off
-setlocal
-
-set BOOGIEDIR=..\..\Binaries
-set BGEXE=%BOOGIEDIR%\Boogie.exe
-
-echo ------------------------------ NestedVC.bpl ---------------------
-%BGEXE% %* /vc:nested NestedVC.bpl
-
-echo ------------------------------ UnreachableBlocks.bpl ---------------------
-%BGEXE% %* /vc:nested UnreachableBlocks.bpl
-
-echo ------------------------------ MultipleErrors.bpl ---------------------
-rem The following tests are rather fickle at the moment--different errors
-rem may be reported during different runs. Moreover, it is conceivable that
-rem the error trace would be reported in different orders, since we do not
-rem attempt to sort the trace labels at this time.
-rem An interesting thing is that /vc:local can with Simplify report more than one
-rem error for this file, even with /errorLimit:1. Other than that, only
-rem local and dag produce VCs to which Simplify actually produces different
-rem counterexamples.
-
-setlocal
-for %%f in (block local dag) do (
- echo.
- echo ----- /vc:%%f
- %BGEXE% %* /errorLimit:1 /errorTrace:1 /vc:%%f /logPrefix:-1%%f MultipleErrors.bpl
-)
-for %%f in (local dag) do (
- echo.
- echo ----- /errorLimit:10 /vc:%%f
- %BGEXE% %* /errorLimit:10 /errorTrace:1 /vc:%%f /logPrefix:-10%%f MultipleErrors.bpl
-)
-endlocal
|