Worked on an extension of the existing verification result caching.

1 files changed, 39 insertions, 0 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 8fe4a5c6..afd2d3e6 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -576,6 +576,8 @@ namespace VC {
 

     private bool _disposed;

 

+    protected Implementation currentImplementation;

+

     protected List<Variable> CurrentLocalVariables = null;

 

     // shared across each implementation; created anew for each implementation

@@ -1309,7 +1311,9 @@ namespace VC {
       Contract.Requires(impl != null);

       Contract.Requires(mvInfo != null);

 

+      currentImplementation = impl;

       Dictionary<Variable, Expr> r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies, mvInfo);

+      currentImplementation = null;

 

       RestoreParamWhereClauses(impl);

 

@@ -1448,6 +1452,28 @@ namespace VC {
           ((AssertCmd)pc).OrigExpr = pc.Expr;

           Contract.Assert(((AssertCmd)pc).IncarnationMap == null);

           ((AssertCmd)pc).IncarnationMap = (Dictionary<Variable, Expr>)cce.NonNull(new Dictionary<Variable, Expr>(incarnationMap));

+

+          if (currentImplementation != null

+              && currentImplementation.NoErrorsInCachedSnapshot

+              && currentImplementation.InjectedAssumptionVariables != null

+              && 2 <= currentImplementation.InjectedAssumptionVariables.Count)

+          {

+            // TODO(wuestholz): Maybe store the assertion expression in a local variable.

+            var expr = LiteralExpr.Imp(currentImplementation.ConjunctionOfInjectedAssumptionVariables(), copy);

+            passiveCmds.Add(new AssumeCmd(Token.NoToken, expr));

+          }

+          else if (currentImplementation != null

+                   && currentImplementation.AnyErrorsInCachedSnapshot)

+          {

+            // TODO(wuestholz): Add an assume statement if the assertion was verified in the previous snapshot.

+          }

+        }

+        else if (pc is AssumeCmd

+                 && QKeyValue.FindStringAttribute(pc.Attributes, "precondition_previous_snapshot") != null

+                 && currentImplementation.InjectedAssumptionVariables != null

+                 && currentImplementation.InjectedAssumptionVariables.Any())

+        {

+          copy = LiteralExpr.Imp(currentImplementation.ConjunctionOfInjectedAssumptionVariables(), copy);

         }

         pc.Expr = copy;

         passiveCmds.Add(pc);

@@ -1521,6 +1547,19 @@ namespace VC {
           }

           passiveCmds.Add(new AssumeCmd(c.tok, assumption));

         }

+

+        if (currentImplementation != null

+            && currentImplementation.NoErrorsInCachedSnapshot

+            && currentImplementation.InjectedAssumptionVariables != null

+            && currentImplementation.InjectedAssumptionVariables.Count == 1

+            && assign.Lhss.Count == 1)

+        {

+          var identExpr = assign.Lhss[0].AsExpr as IdentifierExpr;

+          if (identExpr != null && identExpr.Decl != null && QKeyValue.FindBoolAttribute(identExpr.Decl.Attributes, "assumption"))

+          {

+            passiveCmds.Add(new AssumeCmd(c.tok, new IdentifierExpr(Token.NoToken, currentImplementation.InjectedAssumptionVariables.First())));

+          }

+        }

       }

       #endregion

       #region havoc w |--> assume whereClauses, out := in( w |-> w' )