diff options
author | Benjamin Barenblat <bbaren@mit.edu> | 2016-06-05 15:01:52 -0400 |
---|---|---|
committer | Benjamin Barenblat <bbaren@mit.edu> | 2016-06-05 15:01:52 -0400 |
commit | 41082463d783d6f8d8a5aaf69bf459b57bca6000 (patch) | |
tree | 8b9dca4b583b9cb1ea7ed220fe34d611217eb6cc /Source/ExecutionEngine/VerificationResultCache.cs | |
parent | 64e8b33656140b87137d0662d9e6835e004d13c2 (diff) | |
parent | 8ed5dab22d8377924ee6282b83c1b1f8aa8f3573 (diff) |
Merge branch 'upstream' into dfsg_free
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 dfe32103..3159238c 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; |