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/VerificationResultCache.cs | |
| parent | 8f64d5c104efe69c5d561c1b22c3e1320bba04fa (diff) | |
Added /verifySnapshots:3, which prints recycled errors messages with the source locations of the new code.
Diffstat (limited to 'Source/ExecutionEngine/VerificationResultCache.cs')
| -rw-r--r-- | Source/ExecutionEngine/VerificationResultCache.cs | 44 |
1 files changed, 12 insertions, 32 deletions
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;
|