From 15279d479f3d97952a7345043a1e50b36c88c189 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Mon, 7 Jul 2014 03:20:23 +0200
Subject: Worked on adding support for "canned errors".

---
 Source/ExecutionEngine/ExecutionEngine.cs         | 15 ++++++++++-----
 Source/ExecutionEngine/VerificationResultCache.cs |  8 ++++----
 2 files changed, 14 insertions(+), 9 deletions(-)

(limited to 'Source/ExecutionEngine')

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 48a35e80..04726cff 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -420,15 +420,20 @@ namespace Microsoft.Boogie
     static IDictionary<string, IList<CancellationTokenSource>> RequestIdToCancellationTokenSources = new ConcurrentDictionary<string, IList<CancellationTokenSource>>();
 
 
-    public static void ProcessFiles(List<string> fileNames, bool lookForSnapshots = true)
+    public static void ProcessFiles(List<string> fileNames, bool lookForSnapshots = true, string programId = null)
     {
       Contract.Requires(cce.NonNullElements(fileNames));
 
+      if (programId == null)
+      {
+        programId = "main_program_id";
+      }
+
       if (CommandLineOptions.Clo.VerifySeparately && 1 < fileNames.Count)
       {
         foreach (var f in fileNames)
         {
-          ProcessFiles(new List<string> { f }, lookForSnapshots);
+          ProcessFiles(new List<string> { f }, lookForSnapshots, f);
         }
         return;
       }
@@ -438,7 +443,7 @@ namespace Microsoft.Boogie
         var snapshotsByVersion = LookForSnapshots(fileNames);
         foreach (var s in snapshotsByVersion)
         {
-          ProcessFiles(new List<string>(s), false);
+          ProcessFiles(new List<string>(s), false, programId);
         }
         return;
       }
@@ -493,7 +498,7 @@ namespace Microsoft.Boogie
         Inline(program);
 
         var stats = new PipelineStatistics();
-        oc = InferAndVerify(program, stats, 1 < CommandLineOptions.Clo.VerifySnapshots ? "main_program_id" : null);
+        oc = InferAndVerify(program, stats, 1 < CommandLineOptions.Clo.VerifySnapshots ? programId : null);
         switch (oc)
         {
           case PipelineOutcome.Done:
@@ -886,7 +891,7 @@ namespace Microsoft.Boogie
 
       if (1 < CommandLineOptions.Clo.VerifySnapshots)
       {
-        CachedVerificationResultInjector.Inject(program, stablePrioritizedImpls, requestId);
+        CachedVerificationResultInjector.Inject(program, stablePrioritizedImpls, requestId, programId);
       }
 
       #region Verify each implementation
diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 916340a5..b9c04661 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -112,7 +112,7 @@ namespace Microsoft.Boogie
       return result;
     }
 
-    public static void Inject(Program program, IEnumerable<Implementation> implementations, string requestId)
+    public static void Inject(Program program, IEnumerable<Implementation> implementations, string requestId, string programId)
     {
       var eai = new CachedVerificationResultInjector(program, implementations);
 
@@ -121,7 +121,7 @@ namespace Microsoft.Boogie
       {
         int priority;
         var vr = ExecutionEngine.Cache.Lookup(impl, out priority);
-        if (vr != null)
+        if (vr != null && vr.ProgramId == programId)
         {
           if (priority == Priority.LOW)
           {
@@ -172,11 +172,11 @@ namespace Microsoft.Boogie
     {
       if (result.Errors != null && result.Errors.Count < CommandLineOptions.Clo.ProverCCLimit)
       {
-        implementation.SetErrorChecksumsInCachedSnapshot(result.Errors.Select(cex => cex.Checksum));
+        implementation.SetErrorChecksumToCachedError(result.Errors.Select(cex => new Tuple<byte[], object>(cex.Checksum, cex)));
       }
       else if (result.Outcome == ConditionGeneration.Outcome.Correct)
       {
-        implementation.SetErrorChecksumsInCachedSnapshot(new List<byte[]>());
+        implementation.SetErrorChecksumToCachedError(new List<Tuple<byte[], object>>());
       }
     }
 
-- 
cgit v1.2.3