diff options
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 6 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 9 | ||||
| -rw-r--r-- | Test/snapshots/Answer | 8 | ||||
| -rw-r--r-- | Test/snapshots/runtest.bat | 7 |
4 files changed, 16 insertions, 14 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index f23eaf3b..37d5b51b 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -364,6 +364,7 @@ namespace Microsoft.Boogie { }
public bool VerifySnapshots;
+ public bool VerifySeparately;
public string PrintFile = null;
public int PrintUnstructured = 0;
public int DoomStrategy = -1;
@@ -1321,7 +1322,8 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("useProverEvaluate", ref UseProverEvaluate) ||
ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) ||
ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops) ||
- ps.CheckBooleanFlag("verifySnapshots", ref VerifySnapshots)
+ ps.CheckBooleanFlag("verifySnapshots", ref VerifySnapshots) ||
+ ps.CheckBooleanFlag("verifySeparately", ref VerifySeparately)
) {
// one of the boolean flags matched
return true;
@@ -1641,6 +1643,8 @@ namespace Microsoft.Boogie { /verifySnapshots
verify several program snapshots (named <filename>.v0.bpl
to <filename>.vN.bpl) using verification result caching
+ /verifySeparately
+ verify each input program separately
/removeEmptyBlocks:<c>
0 - do not remove empty blocks during VC generation
1 - remove empty blocks (default)
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 21d0c014..7d4754c4 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -363,6 +363,15 @@ namespace Microsoft.Boogie {
Contract.Requires(cce.NonNullElements(fileNames));
+ if (CommandLineOptions.Clo.VerifySeparately && 1 < fileNames.Count)
+ {
+ foreach (var f in fileNames)
+ {
+ ProcessFiles(new List<string> { f }, lookForSnapshots);
+ }
+ return;
+ }
+
if (CommandLineOptions.Clo.VerifySnapshots && lookForSnapshots)
{
var snapshotsByVersion = new List<List<string>>();
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
+
|