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/VCGeneration/ConditionGeneration.cs | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'Source/VCGeneration/ConditionGeneration.cs')

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index abbcf4aa..33f36a31 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1513,7 +1513,7 @@ namespace VC {
                       && currentImplementation.InjectedAssumptionVariables.Any()
                       && ac.Checksum != null
                       && (currentImplementation.AssertionChecksumsInPreviousSnapshot != null && currentImplementation.AssertionChecksumsInPreviousSnapshot.Contains(ac.Checksum))
-                      && !currentImplementation.ErrorChecksumsInCachedSnapshot.Contains(ac.Checksum))))
+                      && !currentImplementation.ErrorChecksumToCachedError.ContainsKey(ac.Checksum))))
           {
             // Bind the assertion expression to a local variable.
             var incarnation = CreateIncarnation(CurrentTemporaryVariableForAssertions, new IdentifierExpr(Token.NoToken, CurrentTemporaryVariableForAssertions));
@@ -1529,10 +1529,11 @@ namespace VC {
                    && currentImplementation.AnyErrorsInCachedSnapshot
                    && ac.Checksum != null
                    && (currentImplementation.AssertionChecksumsInPreviousSnapshot != null && currentImplementation.AssertionChecksumsInPreviousSnapshot.Contains(ac.Checksum))
-                   && currentImplementation.ErrorChecksumsInCachedSnapshot.Contains(ac.Checksum)
+                   && currentImplementation.ErrorChecksumToCachedError.ContainsKey(ac.Checksum)
                    && (currentImplementation.InjectedAssumptionVariables == null || !currentImplementation.InjectedAssumptionVariables.Any(v => incarnationMap.ContainsKey(v))))
           {
-            // TODO(wuestholz): Uncomment this once the canned errors are reported.
+            // Turn it into an assume statement.
+            // TODO(wuestholz): Uncomment this once the canned errors are reported.            
             // pc = new AssumeCmd(ac.tok, copy);
             pc.Attributes = new QKeyValue(Token.NoToken, "canned_failing_assertion", new List<object>(), pc.Attributes);
             currentImplementation.AddCannedFailingAssertion(ac);
@@ -1552,7 +1553,7 @@ namespace VC {
             || (currentImplementation.AnyErrorsInCachedSnapshot
                 && pc.Checksum != null
                 && (currentImplementation.AssertionChecksumsInPreviousSnapshot != null && currentImplementation.AssertionChecksumsInPreviousSnapshot.Contains(pc.Checksum))
-                && !currentImplementation.ErrorChecksumsInCachedSnapshot.Contains(pc.Checksum)))
+                && !currentImplementation.ErrorChecksumToCachedError.ContainsKey(pc.Checksum)))
         {
           passiveCmds.Add(pc);
         }
-- 
cgit v1.2.3