Worked on adding support for "canned errors".

2 files changed, 14 insertions, 9 deletions

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>>());

       }

     }