Optimized the way that assertions are marked as partially verified.

4 files changed, 31 insertions, 2 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 7d2ee3ac..5eaadf23 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -578,6 +578,19 @@ namespace VC {
 

     protected Implementation currentImplementation;

 

+    private LocalVariable currentTemporaryVariableForAssertions;

+    protected LocalVariable CurrentTemporaryVariableForAssertions

+    {

+      get

+      {

+        if (currentTemporaryVariableForAssertions == null)

+        {

+          currentTemporaryVariableForAssertions = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "##assertion", Microsoft.Boogie.Type.Bool));

+        }

+        return currentTemporaryVariableForAssertions;

+      }

+    }

+

     protected List<Variable> CurrentLocalVariables = null;

 

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

@@ -1312,7 +1325,9 @@ namespace VC {
       Contract.Requires(mvInfo != null);

 

       currentImplementation = impl;

+      currentTemporaryVariableForAssertions = null;

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

+      currentTemporaryVariableForAssertions = null;

       currentImplementation = null;

 

       RestoreParamWhereClauses(impl);

@@ -1458,7 +1473,13 @@ namespace VC {
               && currentImplementation.InjectedAssumptionVariables != null

               && 2 <= currentImplementation.InjectedAssumptionVariables.Count)

           {

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

+            // Bind the assertion expression to a local variable.

+            var incarnation = CreateIncarnation(CurrentTemporaryVariableForAssertions, new IdentifierExpr(Token.NoToken, CurrentTemporaryVariableForAssertions));

+            var identExpr = new IdentifierExpr(Token.NoToken, incarnation);

+            incarnationMap[incarnation] = identExpr;

+            ((AssertCmd)pc).IncarnationMap[incarnation] = identExpr;

+            passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Eq(identExpr, copy)));

+            copy = identExpr;

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

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

           }

diff --git a/Test/snapshots/Snapshots15.v0.bpl b/Test/snapshots/Snapshots15.v0.bpl
index 3dbf492e..a947157d 100644
--- a/Test/snapshots/Snapshots15.v0.bpl
+++ b/Test/snapshots/Snapshots15.v0.bpl
@@ -2,8 +2,12 @@ procedure {:checksum "0"} M();
 

 implementation {:id "M"} {:checksum "1"} M()

 {

+    assert true;

+

     call N();

 

+    assert true;

+

     call N();

 

     assert false;

diff --git a/Test/snapshots/Snapshots15.v1.bpl b/Test/snapshots/Snapshots15.v1.bpl
index 877b247c..a797ab6c 100644
--- a/Test/snapshots/Snapshots15.v1.bpl
+++ b/Test/snapshots/Snapshots15.v1.bpl
@@ -2,8 +2,12 @@ procedure {:checksum "0"} M();
 

 implementation {:id "M"} {:checksum "1"} M()

 {

+    assert true;

+

     call N();

 

+    assert true;

+

     call N();

 

     assert false;

diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index 48251668..853c5a80 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -137,7 +137,7 @@ Execution trace:
 Boogie program verifier finished with 0 verified, 1 error

 

 Boogie program verifier finished with 1 verified, 0 errors

-Snapshots15.v1.bpl(9,5): Error BP5001: This assertion might not hold.

+Snapshots15.v1.bpl(13,5): Error BP5001: This assertion might not hold.

 Execution trace:

     Snapshots15.v1.bpl(5,5): anon0