diff options
| author |  Rustan Leino <leino@microsoft.com> | 2015-08-27 20:10:41 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2015-08-28 13:29:56 -0700 |
| commit | 21f1cfff139759d9b9f91ed800da2158daca8ed4 (patch) | |
| tree | e9665d1ed7561e244372f167fcc6d90abd32127b /Source/ExecutionEngine | |
| parent | 8f64d5c104efe69c5d561c1b22c3e1320bba04fa (diff) | |
Added /verifySnapshots:3, which prints recycled errors messages with the source locations of the new code.
Diffstat (limited to 'Source/ExecutionEngine')
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 45 | ||||
| -rw-r--r-- | Source/ExecutionEngine/VerificationResultCache.cs | 44 |
2 files changed, 31 insertions, 58 deletions
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 67ce49a5..a408642a 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -151,25 +151,18 @@ namespace Microsoft.Boogie {
Contract.Requires(message != null);
- if (category != null)
- {
+ if (category != null) {
message = string.Format("{0}: {1}", category, message);
}
string s;
- if (tok != null)
- {
+ if (tok != null) {
s = string.Format("{0}({1},{2}): {3}", ExecutionEngine.GetFileNameForConsole(tok.filename), tok.line, tok.col, message);
- }
- else
- {
+ } else {
s = message;
}
- if (error)
- {
+ if (error) {
ErrorWriteLine(tw, s);
- }
- else
- {
+ } else {
tw.WriteLine(s);
}
}
@@ -1114,23 +1107,23 @@ namespace Microsoft.Boogie printer.Inform(string.Format("Verifying {0} ...", impl.Name), output);
int priority = 0;
- if (0 < CommandLineOptions.Clo.VerifySnapshots)
- {
- verificationResult = Cache.Lookup(impl, out priority);
- }
-
var wasCached = false;
- if (verificationResult != null && priority == Priority.SKIP)
- {
- if (CommandLineOptions.Clo.XmlSink != null)
- {
- CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start);
- }
+ if (0 < CommandLineOptions.Clo.VerifySnapshots) {
+ var cachedResults = Cache.Lookup(impl, out priority);
+ if (cachedResults != null && priority == Priority.SKIP) {
+ if (CommandLineOptions.Clo.XmlSink != null) {
+ CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, cachedResults.Start);
+ }
- printer.Inform(string.Format("Retrieving cached verification result for implementation {0}...", impl.Name), output);
- wasCached = true;
+ printer.Inform(string.Format("Retrieving cached verification result for implementation {0}...", impl.Name), output);
+ if (CommandLineOptions.Clo.VerifySnapshots < 3 || cachedResults.Outcome == ConditionGeneration.Outcome.Correct) {
+ verificationResult = cachedResults;
+ wasCached = true;
+ }
+ }
}
- else
+
+ if (!wasCached)
{
#region Verify the implementation
diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs index a18cee05..f8aca0e9 100644 --- a/Source/ExecutionEngine/VerificationResultCache.cs +++ b/Source/ExecutionEngine/VerificationResultCache.cs @@ -172,48 +172,28 @@ namespace Microsoft.Boogie var vr = ExecutionEngine.Cache.Lookup(impl, out priority);
if (vr != null && vr.ProgramId == programId)
{
- if (priority == Priority.LOW)
- {
+ if (priority == Priority.LOW) {
run.LowPriorityImplementationCount++;
- if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds)
- {
- SetErrorAndAssertionChecksumsInCachedSnapshot(impl, vr);
- if (vr.ProgramId != null)
- {
- var p = ExecutionEngine.CachedProgram(vr.ProgramId);
- if (p != null)
- {
- eai.Inject(impl, p);
- run.TransformedImplementationCount++;
- }
- }
- }
- }
- else if (priority == Priority.MEDIUM)
- {
+ } else if (priority == Priority.MEDIUM) {
run.MediumPriorityImplementationCount++;
- if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds)
- {
+ } else if (priority == Priority.HIGH) {
+ run.HighPriorityImplementationCount++;
+ } else if (priority == Priority.SKIP) {
+ run.SkippedImplementationCount++;
+ }
+
+ if (priority == Priority.LOW || priority == Priority.MEDIUM || 3 <= CommandLineOptions.Clo.VerifySnapshots) {
+ if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds) {
SetErrorAndAssertionChecksumsInCachedSnapshot(impl, vr);
- if (vr.ProgramId != null)
- {
+ if (vr.ProgramId != null) {
var p = ExecutionEngine.CachedProgram(vr.ProgramId);
- if (p != null)
- {
+ if (p != null) {
eai.Inject(impl, p);
run.TransformedImplementationCount++;
}
}
}
}
- else if (priority == Priority.HIGH)
- {
- run.HighPriorityImplementationCount++;
- }
- else if (priority == Priority.SKIP)
- {
- run.SkippedImplementationCount++;
- }
}
}
run.End = DateTime.UtcNow;
|