diff options
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 13 | ||||
| -rw-r--r-- | Source/Core/LambdaHelper.cs | 2 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 8 | ||||
| -rw-r--r-- | Test/snapshots/runtest.snapshot | 2 |
4 files changed, 15 insertions, 10 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 5ab1942f..2a995fc2 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -364,7 +364,7 @@ namespace Microsoft.Boogie { Contract.Invariant(0 <= PrintUnstructured && PrintUnstructured < 3); // 0 = print only structured, 1 = both structured and unstructured, 2 = only unstructured
}
- public bool VerifySnapshots;
+ public int VerifySnapshots;
public bool VerifySeparately;
public string PrintFile = null;
public int PrintUnstructured = 0;
@@ -1312,6 +1312,10 @@ namespace Microsoft.Boogie { case "errorLimit":
ps.GetNumericArgument(ref ProverCCLimit);
return true;
+
+ case "verifySnapshots":
+ ps.GetNumericArgument(ref VerifySnapshots, 2);
+ return true;
case "useSmtOutputFormat": {
if (ps.ConfirmArgumentCount(0)) {
@@ -1415,7 +1419,6 @@ 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("verifySeparately", ref VerifySeparately) ||
ps.CheckBooleanFlag("trustAtomicityTypes", ref TrustAtomicityTypes) ||
ps.CheckBooleanFlag("trustNonInterference", ref TrustNonInterference) ||
@@ -1743,9 +1746,11 @@ namespace Microsoft.Boogie { 1 = perform live variable analysis (default)
2 = perform interprocedural live variable analysis
/noVerify skip VC generation and invocation of the theorem prover
- /verifySnapshots
+ /verifySnapshots:<n>
verify several program snapshots (named <filename>.v0.bpl
- to <filename>.vN.bpl) using verification result caching
+ to <filename>.vN.bpl) using verification result caching:
+ 0 - do not use any verification result caching (default)
+ 1 - use verification result caching
/verifySeparately
verify each input program separately
/removeEmptyBlocks:<c>
diff --git a/Source/Core/LambdaHelper.cs b/Source/Core/LambdaHelper.cs index 51c9ee23..6b435836 100644 --- a/Source/Core/LambdaHelper.cs +++ b/Source/Core/LambdaHelper.cs @@ -93,7 +93,7 @@ namespace Microsoft.Boogie { Substituter.SubstitutionFromHashtable(oldSubst),
lambda.Attributes);
- if (CommandLineOptions.Clo.VerifySnapshots && QKeyValue.FindStringAttribute(lambdaAttrs, "checksum") == null)
+ if (0 < CommandLineOptions.Clo.VerifySnapshots && QKeyValue.FindStringAttribute(lambdaAttrs, "checksum") == null)
{
// Attach a dummy checksum to avoid issues in the dependency analysis.
var checksumAttr = new QKeyValue(lambda.tok, "checksum", new List<object> { "dummy" }, null);
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 24e9d7f7..6a4dbc07 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -419,7 +419,7 @@ namespace Microsoft.Boogie return;
}
- if (CommandLineOptions.Clo.VerifySnapshots && lookForSnapshots)
+ if (0 < CommandLineOptions.Clo.VerifySnapshots && lookForSnapshots)
{
var snapshotsByVersion = new List<List<string>>();
for (int version = 0; true; version++)
@@ -842,7 +842,7 @@ namespace Microsoft.Boogie // operate on a stable copy, in case it gets updated while we're running
Implementation[] stablePrioritizedImpls = null;
- if (CommandLineOptions.Clo.VerifySnapshots)
+ if (0 < CommandLineOptions.Clo.VerifySnapshots)
{
impls.Iter(impl => { impl.DependenciesChecksum = DependencyCollector.DependenciesChecksum(impl); });
stablePrioritizedImpls = impls.OrderByDescending(
@@ -977,7 +977,7 @@ namespace Microsoft.Boogie printer.Inform("", output); // newline
printer.Inform(string.Format("Verifying {0} ...", impl.Name), output);
- if (CommandLineOptions.Clo.VerifySnapshots)
+ if (0 < CommandLineOptions.Clo.VerifySnapshots)
{
verificationResult = Cache.Lookup(impl);
}
@@ -1072,7 +1072,7 @@ namespace Microsoft.Boogie #region Cache the verification result
- if (CommandLineOptions.Clo.VerifySnapshots && !string.IsNullOrEmpty(impl.Checksum))
+ if (0 < CommandLineOptions.Clo.VerifySnapshots && !string.IsNullOrEmpty(impl.Checksum))
{
Cache.Insert(impl.Id, verificationResult);
}
diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot index f67e6be7..6646d9ea 100644 --- a/Test/snapshots/runtest.snapshot +++ b/Test/snapshots/runtest.snapshot @@ -1,2 +1,2 @@ -// RUN: %boogie -verifySnapshots -verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl > "%t" +// RUN: %boogie -verifySnapshots:1 -verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl > "%t" // RUN: %diff "%s.expect" "%t" |