Make caching of verification results more fine-grained for changes that affect preconditions.

13 files changed, 285 insertions, 72 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index a1a54024..56bfc90f 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2427,6 +2427,28 @@ namespace Microsoft.Boogie {
       functionDependencies.Add(function);

     }

 

+    public bool SignatureEquals(DeclWithFormals other)

+    {

+      Contract.Requires(other != null);

+

+      string sig = null;

+      string otherSig = null;

+      using (var strWr = new System.IO.StringWriter())

+      using (var tokTxtWr = new TokenTextWriter("<no file>", strWr, false, false))

+      {

+        EmitSignature(tokTxtWr, this is Function);

+        sig = strWr.ToString();

+      }

+

+      using (var otherStrWr = new System.IO.StringWriter())

+      using (var otherTokTxtWr = new TokenTextWriter("<no file>", otherStrWr, false, false))

+      {

+        EmitSignature(otherTokTxtWr, other is Function);

+        otherSig = otherStrWr.ToString();

+      }

+      return sig == otherSig;

+    }

+

     protected void EmitSignature(TokenTextWriter stream, bool shortRet) {

       Contract.Requires(stream != null);

       Type.EmitOptionalTypeParams(stream, TypeParameters);

@@ -3295,6 +3317,8 @@ namespace Microsoft.Boogie {
       RecycledFailingAssertions.Add(assertion);

     }

 

+    public Cmd ExplicitAssumptionAboutCachedPrecondition { get; set; }

+

     // Strongly connected components

     private StronglyConnectedComponents<Block/*!*/> scc;

     [ContractInvariantMethod]

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 137e2363..eb8b8e1e 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1144,6 +1144,12 @@ namespace Microsoft.Boogie {
         return;

       }

 

+      if (cmd.IrrelevantForChecksumComputation)

+      {

+        cmd.Checksum = currentChecksum;

+        return;

+      }

+

       var assumeCmd = cmd as AssumeCmd;

       if (assumeCmd != null

           && QKeyValue.FindBoolAttribute(assumeCmd.Attributes, "assumption_variable_initialization"))

@@ -1161,7 +1167,7 @@ namespace Microsoft.Boogie {
         if (havocCmd != null)

         {

           tokTxtWr.Write("havoc ");

-          var relevantVars = havocCmd.Vars.Where(e => usedVariables.Contains(e.Decl) && !e.Decl.Name.StartsWith("a##post##")).OrderBy(e => e.Name).ToList();

+          var relevantVars = havocCmd.Vars.Where(e => usedVariables.Contains(e.Decl) && !e.Decl.Name.StartsWith("a##cached##")).OrderBy(e => e.Name).ToList();

           relevantVars.Emit(tokTxtWr, true);

           tokTxtWr.WriteLine(";");

         }

@@ -1244,6 +1250,7 @@ namespace Microsoft.Boogie {
   public abstract class Cmd : Absy {

     public byte[] Checksum { get; internal set; }

     public byte[] SugaredCmdChecksum { get; internal set; }

+    public bool IrrelevantForChecksumComputation { get; set; }

 

     public Cmd(IToken/*!*/ tok)

       : base(tok) {

@@ -2849,7 +2856,7 @@ namespace Microsoft.Boogie {
       var clauses = procedure.Ensures.Select(e => Substituter.FunctionCallReresolvingApplyReplacingOldExprs(calleeSubstitution, substOldCombined, e.Condition, program)).Concat(modifies);

       // TODO(wuestholz): Try extracting a function for each clause:

       // return Conjunction(clauses.Select(c => extract(c)));

-      var conj = Conjunction(clauses);

+      var conj = Expr.And(clauses, true);

       return conj != null ? extract(conj) : conj;

     }

 

@@ -2860,30 +2867,10 @@ namespace Microsoft.Boogie {
       var clauses = procedure.Requires.Where(r => !r.Free).Select(r => Substituter.FunctionCallReresolvingApplyReplacingOldExprs(calleeSubstitution, calleeSubstitutionOld, r.Condition, program));

       // TODO(wuestholz): Try extracting a function for each clause:

       // return Conjunction(clauses.Select(c => extract(c)));

-      var conj = Conjunction(clauses);

+      var conj = Expr.And(clauses, true);

       return conj != null ? extract(conj) : conj;

     }

 

-    private static Expr Conjunction(IEnumerable<Expr> conjuncts)

-    {

-      // TODO(wuestholz): Maybe we should use 'LiteralExpr.BinaryTreeAnd' instead.

-      Expr result = null;

-      foreach (var c in conjuncts)

-      {

-        if (result != null)

-        {

-          result = LiteralExpr.And(result, c);

-          result.Type = Type.Bool;

-        }

-        else

-        {

-          result = c;

-          result.Type = Type.Bool;

-        }

-      }

-      return result;

-    }

-

     public override Absy StdDispatch(StandardVisitor visitor) {

       //Contract.Requires(visitor != null);

       Contract.Ensures(Contract.Result<Absy>() != null);

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index f3a943b8..c19140d7 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -467,6 +467,29 @@ namespace Microsoft.Boogie {
         var mid = (start + end) / 2;

         return Expr.And(BinaryTreeAnd(terms, start, mid), BinaryTreeAnd(terms, mid + 1, end));

     }

+

+    public static Expr And(IEnumerable<Expr> conjuncts, bool returnNullIfEmpty = false)

+    {

+      Expr result = null;

+      foreach (var c in conjuncts)

+      {

+        if (result != null)

+        {

+          result = LiteralExpr.And(result, c);

+          result.Type = Type.Bool;

+        }

+        else

+        {

+          result = c;

+          result.Type = Type.Bool;

+        }

+      }

+      if (result == null && !returnNullIfEmpty)

+      {

+        result = Expr.True;

+      }

+      return result;

+    }

   }

   [ContractClassFor(typeof(Expr))]

   public abstract class ExprContracts : Expr {

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index 77086f0f..0feb5e35 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -539,7 +539,7 @@ namespace Microsoft.Boogie {
         HavocCmd/*!*/ havocCmd = (HavocCmd)cmd;

         foreach (IdentifierExpr/*!*/ expr in havocCmd.Vars) {

           Contract.Assert(expr != null);

-          if (expr.Decl != null && !(QKeyValue.FindBoolAttribute(expr.Decl.Attributes, "assumption") && expr.Decl.Name.StartsWith("a##post##"))) {

+          if (expr.Decl != null && !(QKeyValue.FindBoolAttribute(expr.Decl.Attributes, "assumption") && expr.Decl.Name.StartsWith("a##cached##"))) {

             liveSet.Remove(expr.Decl);

           }

         }

diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index 181b80a1..7f021c43 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -583,6 +583,15 @@ namespace Microsoft.Boogie {
       return (Expr)new FunctionCallReresolvingReplacingOldSubstituter(program, always, forOld).Visit(expr);

     }

 

+    public static Expr FunctionCallReresolvingApply(Substitution always, Substitution forOld, Expr expr, Program program)

+    {

+      Contract.Requires(always != null);

+      Contract.Requires(forOld != null);

+      Contract.Requires(expr != null);

+      Contract.Ensures(Contract.Result<Expr>() != null);

+      return (Expr)new FunctionCallReresolvingNormalSubstituter(program, always, forOld).Visit(expr);

+    }

+

     // ----------------------------- Substitutions for Cmd -------------------------------

 

     /// <summary>

@@ -660,7 +669,7 @@ namespace Microsoft.Boogie {
 

     // ------------------------------------------------------------

 

-    private sealed class NormalSubstituter : Duplicator

+    private class NormalSubstituter : Duplicator

     {

       private readonly Substitution/*!*/ always;

       private readonly Substitution/*!*/ forold;

@@ -744,6 +753,32 @@ namespace Microsoft.Boogie {
       }

     }

 

+    private sealed class FunctionCallReresolvingNormalSubstituter : NormalSubstituter

+    {

+      readonly Program Program;

+

+      public FunctionCallReresolvingNormalSubstituter(Program program, Substitution always, Substitution forold)

+        : base(always, forold)

+      {

+        Program = program;

+      }

+

+      public override Expr VisitNAryExpr(NAryExpr node)

+      {

+        var result = base.VisitNAryExpr(node);

+        var nAryExpr = result as NAryExpr;

+        if (nAryExpr != null)

+        {

+          var funCall = nAryExpr.Fun as FunctionCall;

+          if (funCall != null)

+          {

+            funCall.Func = Program.FindFunction(funCall.FunctionName);

+          }

+        }

+        return result;

+      }

+    }

+

     private class ReplacingOldSubstituter : Duplicator {

       private readonly Substitution/*!*/ always;

       private readonly Substitution/*!*/ forold;

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 5d20e6e8..63e88dfe 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -96,7 +96,64 @@ namespace Microsoft.Boogie
       assumptionVariableCount = 0;

       temporaryVariableCount = 0;

       currentImplementation = implementation;

-      var result = VisitImplementation(implementation);

+

+      #region Introduce explict assumption about the precondition.

+

+      var oldProc = programInCachedSnapshot.FindProcedure(currentImplementation.Proc.Name);

+      if (oldProc != null

+          && oldProc.DependencyChecksum != currentImplementation.Proc.DependencyChecksum

+          && currentImplementation.ExplicitAssumptionAboutCachedPrecondition == null)

+      {

+        var axioms = new List<Axiom>();

+        var after = new List<Cmd>();

+        Expr assumedExpr = new LiteralExpr(Token.NoToken, false);

+        var canUseSpecs = DependencyCollector.CanExpressOldSpecs(oldProc, Program, true);

+        if (canUseSpecs && oldProc.SignatureEquals(currentImplementation.Proc))

+        {

+          var always = Substituter.SubstitutionFromHashtable(currentImplementation.GetImplFormalMap(), true, currentImplementation.Proc);

+          var forOld = Substituter.SubstitutionFromHashtable(new Dictionary<Variable, Expr>());

+          var clauses = oldProc.Requires.Select(r => Substituter.FunctionCallReresolvingApply(always, forOld, r.Condition, Program));

+          var conj = Expr.And(clauses, true);

+          assumedExpr = conj != null ? FunctionExtractor.Extract(conj, Program, axioms) : new LiteralExpr(Token.NoToken, true);

+        }

+

+        if (assumedExpr != null)

+        {

+          var lv = new LocalVariable(Token.NoToken,

+            new TypedIdent(Token.NoToken, string.Format("a##cached##{0}", FreshAssumptionVariableName), Type.Bool),

+            new QKeyValue(Token.NoToken, "assumption", new List<object>(), null));

+          currentImplementation.InjectAssumptionVariable(lv, !canUseSpecs);

+          var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, lv));

+          var rhs = LiteralExpr.And(new IdentifierExpr(Token.NoToken, lv), assumedExpr);

+          var assumed = new AssignCmd(currentImplementation.tok, new List<AssignLhs> { lhs }, new List<Expr> { rhs });

+          currentImplementation.ExplicitAssumptionAboutCachedPrecondition = assumed;

+          after.Add(assumed);

+        }

+

+        if (CommandLineOptions.Clo.TraceCachingForTesting || CommandLineOptions.Clo.TraceCachingForBenchmarking)

+        {

+          using (var tokTxtWr = new TokenTextWriter("<console>", Console.Out, false, false))

+          {

+            var loc = currentImplementation.tok != null && currentImplementation.tok != Token.NoToken ? string.Format("{0}({1},{2})", currentImplementation.tok.filename, currentImplementation.tok.line, currentImplementation.tok.col) : "<unknown location>";

+            Console.Out.WriteLine("Processing implementation {0} (at {1}):", currentImplementation.Name, loc);

+            foreach (var a in axioms)

+            {

+              Console.Out.Write("  >>> added axiom: ");

+              a.Expr.Emit(tokTxtWr);

+              Console.Out.WriteLine();

+            }

+            foreach (var b in after)

+            {

+              Console.Out.Write("  >>> added after assuming the current precondition: ");

+              b.Emit(tokTxtWr, 0);

+            }

+          }

+        }

+      }

+

+      #endregion

+

+      var result = VisitImplementation(currentImplementation);

       currentImplementation = null;

       this.programInCachedSnapshot = null;

       return result;

@@ -192,7 +249,7 @@ namespace Microsoft.Boogie
         Expr assumedExpr = new LiteralExpr(Token.NoToken, false);

         // TODO(wuestholz): Try out two alternatives: only do this for low priority implementations or not at all.

         var canUseSpecs = DependencyCollector.CanExpressOldSpecs(oldProc, Program);

-        if (canUseSpecs)

+        if (canUseSpecs && oldProc.SignatureEquals(node.Proc))

         {

           var desugaring = node.Desugaring;

           Contract.Assert(desugaring != null);

@@ -231,12 +288,16 @@ namespace Microsoft.Boogie
           }

           

           assumedExpr = node.Postcondition(oldProc, eqs, oldSubst, Program, e => FunctionExtractor.Extract(e, Program, axioms));

+          if (assumedExpr == null)

+          {

+            assumedExpr = new LiteralExpr(Token.NoToken, true);

+          }

         }

 

         if (assumedExpr != null)

         {

           var lv = new LocalVariable(Token.NoToken,

-            new TypedIdent(Token.NoToken, string.Format("a##post##{0}", FreshAssumptionVariableName), Type.Bool),

+            new TypedIdent(Token.NoToken, string.Format("a##cached##{0}", FreshAssumptionVariableName), Type.Bool),

             new QKeyValue(Token.NoToken, "assumption", new List<object>(), null));

           node.AssignedAssumptionVariable = lv;

           currentImplementation.InjectAssumptionVariable(lv, !canUseSpecs);

@@ -431,7 +492,7 @@ namespace Microsoft.Boogie
       }

     }

 

-    public static bool CanExpressOldSpecs(Procedure oldProc, Program newProg)

+    public static bool CanExpressOldSpecs(Procedure oldProc, Program newProg, bool ignoreModifiesClauses = false)

     {

       Contract.Requires(oldProc != null && newProg != null);

 

@@ -439,7 +500,7 @@ namespace Microsoft.Boogie
       var globals = newProg.GlobalVariables;

       return oldProc.DependenciesCollected

              && (oldProc.FunctionDependencies == null || oldProc.FunctionDependencies.All(dep => funcs.Any(f => f.Name == dep.Name && f.DependencyChecksum == dep.DependencyChecksum)))

-             && oldProc.Modifies.All(m => globals.Any(g => g.Name == m.Name));

+             && (ignoreModifiesClauses || oldProc.Modifies.All(m => globals.Any(g => g.Name == m.Name)));

     }

 

     public override Procedure VisitProcedure(Procedure node)

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);

diff --git a/Test/snapshots/Snapshots34.v0.bpl b/Test/snapshots/Snapshots34.v0.bpl
new file mode 100644
index 00000000..e3522645
--- /dev/null
+++ b/Test/snapshots/Snapshots34.v0.bpl
@@ -0,0 +1,7 @@
+procedure {:checksum "0"} P();

+  requires 0 != 0;

+

+implementation {:id "P"} {:checksum "1"} P()

+{

+    assert 1 != 1;

+}

diff --git a/Test/snapshots/Snapshots34.v1.bpl b/Test/snapshots/Snapshots34.v1.bpl
new file mode 100644
index 00000000..b374f7c0
--- /dev/null
+++ b/Test/snapshots/Snapshots34.v1.bpl
@@ -0,0 +1,6 @@
+procedure {:checksum "2"} P();

+

+implementation {:id "P"} {:checksum "1"} P()

+{

+    assert 1 != 1;

+}

diff --git a/Test/snapshots/Snapshots35.v0.bpl b/Test/snapshots/Snapshots35.v0.bpl
new file mode 100644
index 00000000..adfd6a69
--- /dev/null
+++ b/Test/snapshots/Snapshots35.v0.bpl
@@ -0,0 +1,7 @@
+procedure {:checksum "0"} P(b: bool);

+  requires b;

+

+implementation {:id "P"} {:checksum "1"} P(p: bool)

+{

+    assert p;

+}

diff --git a/Test/snapshots/Snapshots35.v1.bpl b/Test/snapshots/Snapshots35.v1.bpl
new file mode 100644
index 00000000..bec381af
--- /dev/null
+++ b/Test/snapshots/Snapshots35.v1.bpl
@@ -0,0 +1,6 @@
+procedure {:checksum "2"} P(b: bool);

+

+implementation {:id "P"} {:checksum "1"} P(p: bool)

+{

+    assert p;

+}

diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot
index a203ffac..01a231fe 100644
--- a/Test/snapshots/runtest.snapshot
+++ b/Test/snapshots/runtest.snapshot
@@ -1,2 +1,2 @@
-// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately -noinfer Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl Snapshots22.bpl Snapshots23.bpl Snapshots24.bpl Snapshots25.bpl Snapshots26.bpl Snapshots27.bpl Snapshots28.bpl Snapshots30.bpl Snapshots31.bpl Snapshots32.bpl Snapshots33.bpl > "%t"

+// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately -noinfer Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl Snapshots22.bpl Snapshots23.bpl Snapshots24.bpl Snapshots25.bpl Snapshots26.bpl Snapshots27.bpl Snapshots28.bpl Snapshots30.bpl Snapshots31.bpl Snapshots32.bpl Snapshots33.bpl Snapshots34.bpl Snapshots35.bpl > "%t"

 // RUN: %diff "%s.expect" "%t"

diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index 8f3c2015..637dd088 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -40,8 +40,13 @@ Snapshots1.v1.bpl(13,5): Error BP5001: This assertion might not hold.
 

 Boogie program verifier finished with 1 verified, 1 error

 Processing call to procedure P2 in implementation P1 (at Snapshots1.v2.bpl(5,5)):

+  >>> added after: a##cached##0 := a##cached##0 && true;

+Processing implementation P2 (at Snapshots1.v2.bpl(12,51)):

+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && true;

 Processing command (at Snapshots1.v2.bpl(5,5)) assert false;

   >>> DoNothingToAssert

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && true;

+  >>> AssumeNegationOfAssumptionVariable

 Snapshots1.v2.bpl(5,5): Error BP5002: A precondition for this call might not hold.

 Snapshots1.v2.bpl(10,3): Related location: This is the precondition that might not hold.

 Processing command (at Snapshots1.v2.bpl(14,5)) assert 2 != 2;

@@ -52,34 +57,45 @@ Boogie program verifier finished with 1 verified, 1 error
 Boogie program verifier finished with 1 verified, 0 errors

 

 Boogie program verifier finished with 1 verified, 0 errors

+Processing implementation P0 (at Snapshots2.v2.bpl(4,51)):

+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && true;

 Processing call to procedure P0 in implementation P0 (at Snapshots2.v2.bpl(6,5)):

+  >>> added after: a##cached##1 := a##cached##1 && true;

 Processing command (at Snapshots2.v2.bpl(6,5)) assert F0();

   >>> DoNothingToAssert

 

 Boogie program verifier finished with 1 verified, 0 errors

+Processing implementation P0 (at Snapshots2.v3.bpl(4,51)):

+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false;

 Processing call to procedure P0 in implementation P0 (at Snapshots2.v3.bpl(6,5)):

-  >>> added after: a##post##0 := a##post##0 && false;

+  >>> added after: a##cached##1 := a##cached##1 && false;

 Processing command (at Snapshots2.v3.bpl(6,5)) assert F0();

   >>> DoNothingToAssert

 

 Boogie program verifier finished with 1 verified, 0 errors

 

 Boogie program verifier finished with 1 verified, 0 errors

-Processing call to procedure P0 in implementation P0 (at Snapshots2.v5.bpl(7,5)):

+Processing implementation P0 (at Snapshots2.v5.bpl(5,51)):

   >>> added axiom: ##extracted_function##1() == F0()

-  >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1();

-Processing command (at Snapshots2.v5.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##1();

-  >>> MarkAsFullyVerified

+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1();

+Processing call to procedure P0 in implementation P0 (at Snapshots2.v5.bpl(7,5)):

+  >>> added axiom: ##extracted_function##2() == F0()

+  >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##2();

+  >>> added after: a##cached##1 := a##cached##1 && true;

+Processing command (at Snapshots2.v5.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##2();

+  >>> MarkAsPartiallyVerified

 Processing command (at Snapshots2.v5.bpl(7,5)) assert F0();

-  >>> MarkAsFullyVerified

+  >>> MarkAsPartiallyVerified

 Processing command (at Snapshots2.v5.bpl(3,1)) assert F0();

-  >>> MarkAsFullyVerified

+  >>> MarkAsPartiallyVerified

 

 Boogie program verifier finished with 1 verified, 0 errors

 Processing command (at Snapshots3.v0.bpl(2,1)) assert G();

   >>> DoNothingToAssert

 

 Boogie program verifier finished with 1 verified, 0 errors

+Processing implementation P0 (at Snapshots3.v1.bpl(4,51)):

+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false;

 Processing command (at Snapshots3.v1.bpl(2,1)) assert G();

   >>> DoNothingToAssert

 Snapshots3.v1.bpl(6,1): Error BP5003: A postcondition might not hold on this return path.

@@ -89,7 +105,7 @@ Boogie program verifier finished with 0 verified, 1 error
 

 Boogie program verifier finished with 3 verified, 0 errors

 Processing call to procedure P2 in implementation P1 (at Snapshots4.v1.bpl(14,5)):

-  >>> added after: a##post##0 := a##post##0 && false;

+  >>> added after: a##cached##0 := a##cached##0 && false;

 Processing command (at Snapshots4.v1.bpl(23,5)) assert false;

   >>> DoNothingToAssert

 Snapshots4.v1.bpl(23,5): Error BP5001: This assertion might not hold.

@@ -103,6 +119,8 @@ Processing command (at Snapshots5.v0.bpl(5,5)) assert false;
   >>> DoNothingToAssert

 

 Boogie program verifier finished with 1 verified, 0 errors

+Processing implementation P0 (at Snapshots5.v1.bpl(3,51)):

+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false;

 Processing command (at Snapshots5.v1.bpl(5,5)) assert false;

   >>> DoNothingToAssert

 Snapshots5.v1.bpl(5,5): Error BP5001: This assertion might not hold.

@@ -115,8 +133,8 @@ Boogie program verifier finished with 1 verified, 0 errors
 Processing call to procedure N in implementation M (at Snapshots6.v1.bpl(11,5)):

   >>> added axiom: (forall y##old##0: int, y: int :: {:weight 30} { ##extracted_function##1(y##old##0, y) } ##extracted_function##1(y##old##0, y) == (y##old##0 == y))

   >>> added before: y##old##0 := y;

-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(y##old##0, y);

-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(y##old##0, y);

+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1(y##old##0, y);

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1(y##old##0, y);

   >>> AssumeNegationOfAssumptionVariable

 Processing command (at Snapshots6.v1.bpl(13,5)) assert y == 0;

   >>> MarkAsPartiallyVerified

@@ -130,8 +148,8 @@ Boogie program verifier finished with 1 verified, 0 errors
 Processing call to procedure N in implementation M (at Snapshots7.v1.bpl(12,5)):

   >>> added axiom: (forall y: int, z: int :: {:weight 30} { ##extracted_function##1(y, z) } ##extracted_function##1(y, z) == (y < z))

   >>> added before: y##old##0 := y;

-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(y, z);

-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(y, z);

+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1(y, z);

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1(y, z);

   >>> AssumeNegationOfAssumptionVariable

 Processing command (at Snapshots7.v1.bpl(14,5)) assert y < 0;

   >>> MarkAsPartiallyVerified

@@ -147,12 +165,12 @@ Processing call to procedure N in implementation M (at Snapshots8.v1.bpl(8,5)):
   >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n))

   >>> added axiom: (forall call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r))

   >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);

-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);

+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);

 Processing command (at Snapshots8.v1.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);

   >>> MarkAsFullyVerified

 Processing command (at Snapshots8.v1.bpl(8,5)) assert 0 < call0formal#AT#n;

   >>> MarkAsFullyVerified

-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);

   >>> AssumeNegationOfAssumptionVariable

 Processing command (at Snapshots8.v1.bpl(10,5)) assert 0 <= x;

   >>> MarkAsPartiallyVerified

@@ -170,12 +188,12 @@ Processing call to procedure N in implementation M (at Snapshots9.v1.bpl(8,5)):
   >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n && true))

   >>> added axiom: (forall call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r && true))

   >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);

-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);

+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);

 Processing command (at Snapshots9.v1.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);

   >>> MarkAsFullyVerified

 Processing command (at Snapshots9.v1.bpl(8,5)) assert 0 < call0formal#AT#n;

   >>> MarkAsFullyVerified

-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);

   >>> AssumeNegationOfAssumptionVariable

 Processing command (at Snapshots9.v1.bpl(10,5)) assert 0 <= x;

   >>> MarkAsPartiallyVerified

@@ -191,12 +209,12 @@ Processing call to procedure N in implementation M (at Snapshots10.v1.bpl(8,5)):
   >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n))

   >>> added axiom: (forall call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r))

   >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);

-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);

+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);

 Processing command (at Snapshots10.v1.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);

   >>> MarkAsFullyVerified

 Processing command (at Snapshots10.v1.bpl(8,5)) assert 0 < call0formal#AT#n;

   >>> MarkAsFullyVerified

-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);

   >>> AssumeNegationOfAssumptionVariable

 Processing command (at Snapshots10.v1.bpl(12,5)) assert 0 <= x;

   >>> MarkAsPartiallyVerified

@@ -214,7 +232,7 @@ Processing call to procedure N in implementation M (at Snapshots11.v1.bpl(7,5)):
   >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n))

   >>> added axiom: (forall call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r))

   >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);

-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);

+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);

 Processing command (at Snapshots11.v1.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);

   >>> DropAssume

 Processing command (at Snapshots11.v1.bpl(7,5)) assert 0 < call0formal#AT#n;

@@ -230,7 +248,7 @@ Processing command (at Snapshots12.v0.bpl(7,5)) assert false;
 

 Boogie program verifier finished with 1 verified, 0 errors

 Processing call to procedure N in implementation M (at Snapshots12.v1.bpl(5,5)):

-  >>> added after: a##post##0 := a##post##0 && false;

+  >>> added after: a##cached##0 := a##cached##0 && false;

 Processing command (at Snapshots12.v1.bpl(7,5)) assert false;

   >>> DoNothingToAssert

 Snapshots12.v1.bpl(7,5): Error BP5001: This assertion might not hold.

@@ -241,7 +259,7 @@ Processing command (at Snapshots13.v0.bpl(7,5)) assert false;
 

 Boogie program verifier finished with 1 verified, 0 errors

 Processing call to procedure N in implementation M (at Snapshots13.v1.bpl(5,5)):

-  >>> added after: a##post##0 := a##post##0 && false;

+  >>> added after: a##cached##0 := a##cached##0 && false;

 Processing command (at Snapshots13.v1.bpl(7,5)) assert false;

   >>> DoNothingToAssert

 Snapshots13.v1.bpl(7,5): Error BP5001: This assertion might not hold.

@@ -253,8 +271,8 @@ Processing command (at Snapshots14.v0.bpl(7,5)) assert false;
 Boogie program verifier finished with 1 verified, 0 errors

 Processing call to procedure N in implementation M (at Snapshots14.v1.bpl(5,5)):

   >>> added axiom: ##extracted_function##1() == (F() && G())

-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##1();

-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1();

+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1();

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1();

   >>> AssumeNegationOfAssumptionVariable

 Processing command (at Snapshots14.v1.bpl(7,5)) assert false;

   >>> MarkAsPartiallyVerified

@@ -270,9 +288,9 @@ Processing command (at Snapshots15.v0.bpl(13,5)) assert false;
 

 Boogie program verifier finished with 1 verified, 0 errors

 Processing call to procedure N in implementation M (at Snapshots15.v1.bpl(7,5)):

-  >>> added after: a##post##0 := a##post##0 && false;

+  >>> added after: a##cached##0 := a##cached##0 && false;

 Processing call to procedure N in implementation M (at Snapshots15.v1.bpl(11,5)):

-  >>> added after: a##post##1 := a##post##1 && false;

+  >>> added after: a##cached##1 := a##cached##1 && false;

 Processing command (at Snapshots15.v1.bpl(5,5)) assert true;

   >>> MarkAsFullyVerified

 Processing command (at Snapshots15.v1.bpl(9,5)) assert true;

@@ -302,11 +320,11 @@ Processing command (at Snapshots17.v0.bpl(20,13)) assert x == 1;
 

 Boogie program verifier finished with 1 verified, 0 errors

 Processing call to procedure N in implementation M (at Snapshots17.v1.bpl(14,13)):

-  >>> added after: a##post##0 := a##post##0 && false;

+  >>> added after: a##cached##0 := a##cached##0 && false;

 Processing call to procedure N in implementation M (at Snapshots17.v1.bpl(16,13)):

-  >>> added after: a##post##1 := a##post##1 && false;

+  >>> added after: a##cached##1 := a##cached##1 && false;

 Processing call to procedure N in implementation M (at Snapshots17.v1.bpl(23,9)):

-  >>> added after: a##post##2 := a##post##2 && false;

+  >>> added after: a##cached##2 := a##cached##2 && false;

 Processing command (at Snapshots17.v1.bpl(28,5)) assert true;

   >>> MarkAsFullyVerified

 Processing command (at Snapshots17.v1.bpl(25,9)) assert false;

@@ -328,9 +346,9 @@ Processing command (at Snapshots18.v0.bpl(20,5)) assert 2 != 2;
 

 Boogie program verifier finished with 1 verified, 0 errors

 Processing call to procedure N in implementation M (at Snapshots18.v1.bpl(9,9)):

-  >>> added after: a##post##0 := a##post##0 && false;

+  >>> added after: a##cached##0 := a##cached##0 && false;

 Processing call to procedure N in implementation M (at Snapshots18.v1.bpl(10,9)):

-  >>> added after: a##post##1 := a##post##1 && false;

+  >>> added after: a##cached##1 := a##cached##1 && false;

 Processing command (at Snapshots18.v1.bpl(7,9)) assert 0 == 0;

   >>> MarkAsFullyVerified

 Processing command (at Snapshots18.v1.bpl(17,9)) assert 1 != 1;

@@ -351,13 +369,14 @@ Boogie program verifier finished with 0 verified, 1 error
 Processing call to procedure N in implementation M (at Snapshots19.v1.bpl(5,5)):

   >>> added axiom: ##extracted_function##1() == (2 == 2)

   >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1();

+  >>> added after: a##cached##0 := a##cached##0 && true;

 Processing command (at Snapshots19.v1.bpl(5,5)) assume {:precondition_previous_snapshot} ##extracted_function##1();

   >>> MarkAsFullyVerified

 Processing command (at Snapshots19.v1.bpl(5,5)) assert 2 == 2;

   >>> MarkAsFullyVerified

 Processing command (at Snapshots19.v1.bpl(7,5)) assert 1 != 1;

-  >>> RecycleError

-Snapshots19.v0.bpl(7,5): Error BP5001: This assertion might not hold.

+  >>> DoNothingToAssert

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

 

 Boogie program verifier finished with 0 verified, 1 error

 Processing command (at Snapshots20.v0.bpl(9,9)) assert 1 != 1;

@@ -371,7 +390,7 @@ Snapshots20.v0.bpl(13,9): Error BP5001: This assertion might not hold.
 Boogie program verifier finished with 0 verified, 1 error

 Processing call to procedure N in implementation M (at Snapshots20.v1.bpl(7,9)):

   >>> added axiom: ##extracted_function##1() == (0 != 0)

-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##1();

+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1();

 Processing command (at Snapshots20.v1.bpl(9,9)) assert 1 != 1;

   >>> MarkAsPartiallyVerified

 Processing command (at Snapshots20.v1.bpl(13,9)) assert 2 != 2;

@@ -567,8 +586,8 @@ Processing command (at Snapshots31.v0.bpl(10,5)) assert 0 < g;
 Boogie program verifier finished with 1 verified, 0 errors

 Processing call to procedure Q in implementation P (at Snapshots31.v1.bpl(9,5)):

   >>> added axiom: (forall call0old#AT#g: int, g: int :: {:weight 30} { ##extracted_function##1(call0old#AT#g, g) } ##extracted_function##1(call0old#AT#g, g) == (call0old#AT#g < g))

-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#g, g);

-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#g, g);

+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1(call0old#AT#g, g);

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1(call0old#AT#g, g);

   >>> AssumeNegationOfAssumptionVariable

 Processing command (at Snapshots31.v1.bpl(10,5)) assert 0 < g;

   >>> MarkAsPartiallyVerified

@@ -582,8 +601,8 @@ Boogie program verifier finished with 1 verified, 0 errors
 Processing call to procedure Q in implementation P (at Snapshots32.v1.bpl(8,5)):

   >>> added axiom: (forall g##old##0: int, g: int :: {:weight 30} { ##extracted_function##1(g##old##0, g) } ##extracted_function##1(g##old##0, g) == (g##old##0 < g))

   >>> added before: g##old##0 := g;

-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(g##old##0, g);

-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(g##old##0, g);

+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1(g##old##0, g);

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1(g##old##0, g);

   >>> AssumeNegationOfAssumptionVariable

 Processing command (at Snapshots32.v1.bpl(9,5)) assert 0 < g;

   >>> MarkAsPartiallyVerified

@@ -594,7 +613,38 @@ Processing command (at Snapshots33.v0.bpl(10,5)) assert 0 < g;
   >>> DoNothingToAssert

 

 Boogie program verifier finished with 1 verified, 0 errors

+Processing implementation P (at Snapshots33.v1.bpl(3,42)):

+  >>> added axiom: (forall g: int :: {:weight 30} { ##extracted_function##1(g) } ##extracted_function##1(g) == (g == 0))

+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1(g);

 Processing call to procedure Q in implementation P (at Snapshots33.v1.bpl(5,5)):

-  >>> added after: a##post##0 := a##post##0 && false;

+  >>> added after: a##cached##1 := a##cached##1 && false;

+

+Boogie program verifier finished with 1 verified, 0 errors

+Processing command (at Snapshots34.v0.bpl(6,5)) assert 1 != 1;

+  >>> DoNothingToAssert

+

+Boogie program verifier finished with 1 verified, 0 errors

+Processing implementation P (at Snapshots34.v1.bpl(3,42)):

+  >>> added axiom: ##extracted_function##1() == (0 != 0)

+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1();

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1();

+  >>> AssumeNegationOfAssumptionVariable

+Processing command (at Snapshots34.v1.bpl(5,5)) assert 1 != 1;

+  >>> MarkAsPartiallyVerified

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

+

+Boogie program verifier finished with 0 verified, 1 error

+Processing command (at Snapshots35.v0.bpl(6,5)) assert p;

+  >>> DoNothingToAssert

 

 Boogie program verifier finished with 1 verified, 0 errors

+Processing implementation P (at Snapshots35.v1.bpl(3,42)):

+  >>> added axiom: (forall p: bool :: {:weight 30} { ##extracted_function##1(p) } ##extracted_function##1(p) == p)

+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1(p);

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1(p);

+  >>> AssumeNegationOfAssumptionVariable

+Processing command (at Snapshots35.v1.bpl(5,5)) assert p;

+  >>> MarkAsPartiallyVerified

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

+

+Boogie program verifier finished with 0 verified, 1 error