diff options
| author |  wuestholz <unknown> | 2013-07-05 17:19:48 -0700 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-07-05 17:19:48 -0700 |
| commit | 11e2d2b6d6a8cb6da6d98bc8f102d8375fca26f5 (patch) | |
| tree | b6c8e9d53c0b1fa75a00309069d41621bfba506a /Test/snapshots | |
| parent | 5fe9141ded93f6eab4e213c1d082b68ac557d81a (diff) | |
Added an option to verify each input file separately.
Diffstat (limited to 'Test/snapshots')
| -rw-r--r-- | Test/snapshots/Answer | 8 | ||||
| -rw-r--r-- | Test/snapshots/runtest.bat | 7 |
2 files changed, 2 insertions, 13 deletions
diff --git a/Test/snapshots/Answer b/Test/snapshots/Answer index 676f0323..dc0ee8c1 100644 --- a/Test/snapshots/Answer +++ b/Test/snapshots/Answer @@ -1,5 +1,3 @@ -
--------------------- Snapshots0 --------------------
Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
Execution trace:
Snapshots0.v0.bpl(41,5): anon0
@@ -27,8 +25,6 @@ Execution trace: Snapshots0.v0.bpl(41,5): anon0
Boogie program verifier finished with 2 verified, 1 error
-
--------------------- Snapshots1 --------------------
Snapshots1.v0.bpl(13,5): Error BP5001: This assertion might not hold.
Execution trace:
Snapshots1.v0.bpl(13,5): anon0
@@ -46,8 +42,6 @@ Execution trace: Boogie program verifier finished with 1 verified, 1 error
--------------------- Snapshots2 --------------------
-
Boogie program verifier finished with 1 verified, 0 errors
Boogie program verifier finished with 1 verified, 0 errors
@@ -60,8 +54,6 @@ Boogie program verifier finished with 1 verified, 0 errors Boogie program verifier finished with 1 verified, 0 errors
--------------------- Snapshots3 --------------------
-
Boogie program verifier finished with 1 verified, 0 errors
Snapshots3.v1.bpl(6,1): Error BP5003: A postcondition might not hold on this return path.
Snapshots3.v1.bpl(2,1): Related location: This is the postcondition that might not hold.
diff --git a/Test/snapshots/runtest.bat b/Test/snapshots/runtest.bat index 663cef07..e54a19bc 100644 --- a/Test/snapshots/runtest.bat +++ b/Test/snapshots/runtest.bat @@ -4,8 +4,5 @@ setlocal set BOOGIEDIR=..\..\Binaries
set BGEXE=%BOOGIEDIR%\Boogie.exe
-for %%f in (Snapshots0 Snapshots1 Snapshots2 Snapshots3) do (
- echo.
- echo -------------------- %%f --------------------
- %BGEXE% %* /verifySnapshots %%f.bpl
-)
+%BGEXE% %* /verifySnapshots /verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl
+
|