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/ExecutionEngine.cs         | 45 ++++++++++-------------
 Source/ExecutionEngine/VerificationResultCache.cs | 44 ++++++----------------
 2 files changed, 31 insertions(+), 58 deletions(-)

(limited to 'Source/ExecutionEngine')

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