From 21f1cfff139759d9b9f91ed800da2158daca8ed4 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Thu, 27 Aug 2015 20:10:41 -0700
Subject: Added /verifySnapshots:3, which prints recycled errors messages with
 the source locations of the new code.

---
 Source/ExecutionEngine/VerificationResultCache.cs | 44 +++++++----------------
 1 file changed, 12 insertions(+), 32 deletions(-)

(limited to 'Source/ExecutionEngine/VerificationResultCache.cs')

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;
-- 
cgit v1.2.3