Make it preserve the fact that the value of an assumption variable never becomes logically weaker after a havoc.

3 files changed, 62 insertions, 17 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 515ec16d..206e0ee7 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1742,8 +1742,8 @@ namespace VC {
         Contract.Assert(c != null);

         // If an assumption variable for postconditions is included here, it must have been assigned within a loop.

         // 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 are therefore not going refer to the assumption variable after

-        // the loop. We can achieve this by simply not updating/adding it in the incarnation map.

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

         // First, compute the new incarnations

         foreach (IdentifierExpr ie in havocVars) {

@@ -1767,6 +1767,18 @@ namespace VC {
             }

           }

         }

+

+        // Add the following assume-statement for each assumption variable 'v', where 'v_post' is the new incarnation and 'v_pre' is the old one:

+        // assume v_post ==> v_pre;

+        foreach (IdentifierExpr ie in havocVars)

+        {

+          if (QKeyValue.FindBoolAttribute(ie.Decl.Attributes, "assumption"))

+          {

+            var preInc = (Expr)(preHavocIncarnationMap[ie.Decl].Clone());

+            var postInc = (Expr)(incarnationMap[ie.Decl].Clone());

+            passiveCmds.Add(new AssumeCmd(c.tok, Expr.Imp(postInc, preInc)));

+          }

+        }

       }

       #endregion

  else if (c is CommentCmd) {

diff --git a/Test/test2/AssumptionVariables0.bpl b/Test/test2/AssumptionVariables0.bpl
index cc73707c..766c9d1e 100644
--- a/Test/test2/AssumptionVariables0.bpl
+++ b/Test/test2/AssumptionVariables0.bpl
@@ -28,13 +28,46 @@ procedure Test2()
 }

 

 

-var {:assumption} a0: bool;

+var {:assumption} ga0: bool;

 

 

 procedure Test3()

-  modifies a0;

+  modifies ga0;

 {

-    a0 := a0 && true;

+    ga0 := ga0 && true;

 

-    assert a0;  // error

+    assert ga0;  // error

+}

+

+

+procedure Test4()

+{

+    var {:assumption} a0: bool;

+    var tmp: bool;

+

+    tmp := a0;

+

+    havoc a0;

+

+    assert a0 ==> tmp;

+}

+

+

+procedure Test5(A: bool)

+{

+    var {:assumption} a0: bool;

+    var tmp0, tmp1: bool;

+

+    a0 := a0 && A;

+    tmp0 := a0;

+

+    havoc a0;

+

+    assert a0 ==> tmp0;

+

+    tmp1 := a0;

+

+    havoc a0;

+

+    assert a0 ==> tmp1;

 }

diff --git a/Test/test2/AssumptionVariables0.bpl.expect b/Test/test2/AssumptionVariables0.bpl.expect
index 54ddb2a9..44292082 100644
--- a/Test/test2/AssumptionVariables0.bpl.expect
+++ b/Test/test2/AssumptionVariables0.bpl.expect
@@ -1,11 +1,11 @@
-AssumptionVariables0.bpl(17,5): Error BP5001: This assertion might not hold.
-Execution trace:
-    AssumptionVariables0.bpl(15,8): anon0
-AssumptionVariables0.bpl(27,5): Error BP5001: This assertion might not hold.
-Execution trace:
-    AssumptionVariables0.bpl(25,5): anon0
-AssumptionVariables0.bpl(39,5): Error BP5001: This assertion might not hold.
-Execution trace:
-    AssumptionVariables0.bpl(37,8): anon0
-
-Boogie program verifier finished with 1 verified, 3 errors
+AssumptionVariables0.bpl(17,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    AssumptionVariables0.bpl(15,8): anon0

+AssumptionVariables0.bpl(27,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    AssumptionVariables0.bpl(25,5): anon0

+AssumptionVariables0.bpl(39,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    AssumptionVariables0.bpl(37,9): anon0

+

+Boogie program verifier finished with 3 verified, 3 errors