From 6d5ddf853694b2b8014585dd1e40cc10efbaddea Mon Sep 17 00:00:00 2001
From: Valentin Wüstholz <wuestholz@gmail.com>
Date: Sun, 17 May 2015 13:06:58 +0200
Subject: Make caching of verification results more fine-grained for changes
 that affect preconditions.

---
 Source/VCGeneration/ConditionGeneration.cs | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

(limited to 'Source/VCGeneration')

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 206e0ee7..a19f983a 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -768,6 +768,7 @@ namespace VC {
         Contract.Assert(req != null);
         Expr e = Substituter.Apply(formalProcImplSubst, req.Condition);
         Cmd c = new AssumeCmd(req.tok, e);
+        c.IrrelevantForChecksumComputation = true;
         insertionPoint.Cmds.Add(c);
         if (debugWriter != null) {
           c.Emit(debugWriter, 1);
@@ -775,6 +776,11 @@ namespace VC {
       }
       origStartBlock.Predecessors.Add(insertionPoint);
 
+      if (impl.ExplicitAssumptionAboutCachedPrecondition != null)
+      {
+        insertionPoint.Cmds.Add(impl.ExplicitAssumptionAboutCachedPrecondition);
+      }
+
       if (debugWriter != null) {
         debugWriter.WriteLine();
       }
@@ -1275,7 +1281,7 @@ namespace VC {
           IdentifierExpr v_prime_exp = new IdentifierExpr(v_prime.tok, v_prime);
           #endregion
           #region Create the assume command itself
-          AssumeCmd ac = new AssumeCmd(v.tok, TypedExprEq(v_prime_exp, pred_incarnation_exp, v_prime.Name.Contains("a##post##")));
+          AssumeCmd ac = new AssumeCmd(v.tok, TypedExprEq(v_prime_exp, pred_incarnation_exp, v_prime.Name.Contains("a##cached##")));
           pred.Cmds.Add(ac);
           #endregion
           #endregion
@@ -1697,7 +1703,7 @@ namespace VC {
             }
           
             #region Create an assume command with the new variable
-            assumptions.Add(TypedExprEq(x_prime_exp, copies[i], x_prime_exp.Decl != null && x_prime_exp.Decl.Name.Contains("a##post##")));
+            assumptions.Add(TypedExprEq(x_prime_exp, copies[i], x_prime_exp.Decl != null && x_prime_exp.Decl.Name.Contains("a##cached##")));
             #endregion
           }
         }
@@ -1720,6 +1726,7 @@ namespace VC {
         if (currentImplementation != null
             && currentImplementation.HasCachedSnapshot
             && !currentImplementation.AnyErrorsInCachedSnapshot
+            && currentImplementation.DoomedInjectedAssumptionVariables.Count == 0
             && currentImplementation.InjectedAssumptionVariables.Count == 1
             && assign.Lhss.Count == 1)
         {
@@ -1744,7 +1751,7 @@ namespace VC {
         // We do not need to havoc it if we have performed a modular proof of the loop (i.e., using only the loop
         // invariant) in the previous snapshot and, consequently, the corresponding assumption did not affect the
         // anything after the loop. We can achieve this by simply not updating/adding it in the incarnation map.
-        List<IdentifierExpr> havocVars = hc.Vars.Where(v => !(QKeyValue.FindBoolAttribute(v.Decl.Attributes, "assumption") && v.Decl.Name.StartsWith("a##post##"))).ToList();
+        List<IdentifierExpr> havocVars = hc.Vars.Where(v => !(QKeyValue.FindBoolAttribute(v.Decl.Attributes, "assumption") && v.Decl.Name.StartsWith("a##cached##"))).ToList();
         // First, compute the new incarnations
         foreach (IdentifierExpr ie in havocVars) {
           Contract.Assert(ie != null);
-- 
cgit v1.2.3