Merge branch 'master' of https://github.com/boogie-org/boogie

14 files changed, 421 insertions, 54 deletions

diff --git a/Test/prover/usedot.bpl b/Test/prover/usedot.bpl
new file mode 100644
index 00000000..5815236e
--- /dev/null
+++ b/Test/prover/usedot.bpl
@@ -0,0 +1,9 @@
+// RUN: %boogie -typeEncoding:m -proverLog:"%t.smt2" "%s"
+// RUN: %OutputCheck "%s" --file-to-check="%t.smt2"
+procedure foo() {
+  // . is an illegal starting character in SMT-LIBv2
+  // so test that we don't emit it as a symbol name.
+  // CHECK-L:(declare-fun q@.x () Int)
+  var .x:int;
+  assert .x == 0;
+}
diff --git a/Test/secure/tworound.bpl b/Test/secure/tworound.bpl
new file mode 100644
index 00000000..a78c4af4
--- /dev/null
+++ b/Test/secure/tworound.bpl
@@ -0,0 +1,116 @@
+type T = bv4;
+function {:bvbuiltin "bvult"} bvlt(p1: T, p2: T) : bool; // unsigned less than
+function {:bvbuiltin "bvxor"} xorT(p1: T, p2: T) : T;
+function {:bvbuiltin "bvadd"} bvadd(p1: T, p2: T) : T;
+
+
+procedure bar({:visible} v: T)
+  returns ({:hidden} h: T)
+  ensures true;
+{
+  h := v;
+}
+
+procedure foo0({:visible} x1: T, {:visible} x2: T, {:hidden} y1: T, {:hidden} y2: T)
+  returns ({:visible} r1: bool, {:visible} r2: bool, 
+      {:visible} s1: T, {:visible} s2: T, {:visible} s3: T, {:visible} s4: T)
+  ensures (r2 == bvlt(bvadd(x1,x2), bvadd(y1,y2))) && (r1 == bvlt(x1, y1));
+{
+   var {:hidden} t1, t2: T;
+
+   r1 := bvlt(x1, y1);
+
+   havoc s1;
+   havoc s2;
+
+   s3 := xorT(x1, s1);
+   s4 := xorT(y1, s2);
+
+   t1 := xorT(s1, s3);
+   t2 := xorT(s2, s4);
+
+   r2 := bvlt(bvadd(x2, t1), bvadd(y2, t2));
+}
+
+
+procedure foo1({:visible} x1: T, {:visible} x2: T, {:hidden} y1: T, {:hidden} y2: T)
+  returns ({:visible} r1: bool, {:visible} r2: bool, 
+      {:visible} s1: T, {:visible} s2: T, {:hidden} s3: T, {:hidden} s4: T)
+  ensures (r2 == bvlt(bvadd(x1,x2), bvadd(y1,y2))) && (r1 == bvlt(x1, y1));
+{
+   var {:hidden} t1, t2: T;
+
+   r1 := bvlt(x1, y1);
+
+   havoc s1;
+   havoc s2;
+
+   s3 := xorT(x1, s1);
+   s4 := xorT(y1, s2);
+
+   t1 := xorT(s1, s3);
+   t2 := xorT(s2, s4);
+
+   r2 := bvlt(bvadd(x2, t1), bvadd(y2, t2));
+}
+
+
+
+procedure foo2({:visible} x1: T, {:visible} x2: T, {:hidden} y1: T, {:hidden} y2: T)
+  returns ({:visible} r1: bool, {:visible} r2: bool, 
+      {:visible} s1: T, {:visible} s2: T)
+  ensures (r2 == bvlt(bvadd(x1,x2), bvadd(y1,y2))) && (r1 == bvlt(x1, y1)); 
+{
+   var {:hidden} t1, t2: T;
+   var {:hidden} s3, s4: T;
+
+   r1 := bvlt(x1, y1);
+
+   havoc s1;
+   havoc s2;
+
+   s3 := xorT(x1, s1);
+   s4 := xorT(y1, s2);
+
+   t1 := xorT(s1, s3);
+   t2 := xorT(s2, s4);
+
+   r2 := bvlt(bvadd(x2, t1), bvadd(y2, t2));
+}
+
+procedure foo3({:visible} x1: T, {:visible} x2: T, {:hidden} y1: T, {:hidden} y2: T)
+  returns ({:visible} r1: bool, {:visible} r2: bool, 
+      {:visible} s1: T, {:visible} s2: T, {:hidden} s3: T, {:hidden} s4: T)
+  ensures (r2 == bvlt(bvadd(x1,x2), bvadd(y1,y2))) && (r1 == bvlt(x1, y1)) && (s4 == xorT(y1,s2)) && (s3 == xorT(x1, s1));
+{
+   var {:hidden} t1, t2: T;
+
+   r1 := bvlt(x1, y1);
+
+   havoc s1;
+   havoc s2;
+
+   s3 := xorT(x1, s1);
+   s4 := xorT(y1, s2);
+
+   t1 := xorT(s1, s3);
+   t2 := xorT(s2, s4);
+
+   r2 := bvlt(bvadd(x2, t1), bvadd(y2, t2));
+}
+
+
+
+procedure bid({:visible} x1: T, {:visible} x2: T, {:hidden} y1: T, {:hidden} y2: T)
+  returns ({:visible} r: bool)
+  ensures r == bvlt(bvadd(x1,x2), bvadd(y1,y2));
+{
+  var {:hidden} r1, r2: bool;
+  var {:hidden} s1, s2, s3, s4: T;
+
+  call r1, r2, s1, s2, s3, s4 := foo1(x1, x2, y1, y2);
+
+  r := r2;
+}
+
+
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

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

diff --git a/Test/test2/CallVerifiedUnder0.bpl b/Test/test2/CallVerifiedUnder0.bpl
new file mode 100644
index 00000000..9ac9dec7
--- /dev/null
+++ b/Test/test2/CallVerifiedUnder0.bpl
@@ -0,0 +1,42 @@
+// RUN: %boogie -noinfer "%s" > "%t"

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

+

+procedure A(P: bool);

+  requires P;

+

+procedure Test0()

+{

+    call {:verified_under false} A(false);  // error

+}

+

+

+procedure Test1()

+{

+    call {:verified_under true} A(false);

+}

+

+

+procedure Test2(P: bool, A: bool)

+{

+    call {:verified_under A} A(P);  // error

+}

+

+

+procedure Test3(P: bool, A: bool)

+  requires !A ==> P;

+{

+    call {:verified_under A} A(P);

+}

+

+

+procedure Test4(P: bool, A: bool)

+{

+    call {:verified_under A} {:verified_under true} A(P);  // error

+}

+

+

+procedure Test5(P: bool, A: bool)

+  requires !A ==> P;

+{

+    call {:verified_under A} {:verified_under true} A(P);

+}

diff --git a/Test/test2/CallVerifiedUnder0.bpl.expect b/Test/test2/CallVerifiedUnder0.bpl.expect
new file mode 100644
index 00000000..5d407874
--- /dev/null
+++ b/Test/test2/CallVerifiedUnder0.bpl.expect
@@ -0,0 +1,14 @@
+CallVerifiedUnder0.bpl(9,5): Error BP5002: A precondition for this call might not hold.

+CallVerifiedUnder0.bpl(5,3): Related location: This is the precondition that might not hold.

+Execution trace:

+    CallVerifiedUnder0.bpl(9,5): anon0

+CallVerifiedUnder0.bpl(21,5): Error BP5002: A precondition for this call might not hold.

+CallVerifiedUnder0.bpl(5,3): Related location: This is the precondition that might not hold.

+Execution trace:

+    CallVerifiedUnder0.bpl(21,5): anon0

+CallVerifiedUnder0.bpl(34,5): Error BP5002: A precondition for this call might not hold.

+CallVerifiedUnder0.bpl(5,3): Related location: This is the precondition that might not hold.

+Execution trace:

+    CallVerifiedUnder0.bpl(34,5): anon0

+

+Boogie program verifier finished with 3 verified, 3 errors

diff --git a/Test/test2/InvariantVerifiedUnder0.bpl b/Test/test2/InvariantVerifiedUnder0.bpl
new file mode 100644
index 00000000..6cade5a5
--- /dev/null
+++ b/Test/test2/InvariantVerifiedUnder0.bpl
@@ -0,0 +1,54 @@
+// RUN: %boogie -noinfer "%s" > "%t"

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

+

+procedure Test0()

+{

+    while (*)

+      invariant {:verified_under false} false;  // error

+    {}

+}

+

+

+procedure Test1()

+{

+    while (*)

+      invariant {:verified_under true} false;

+    {}

+}

+

+

+procedure Test2(P: bool, Q: bool, A: bool)

+{

+    while (*)

+      invariant {:verified_under A} P;  // error

+      invariant {:verified_under A} Q;  // error

+    {}

+}

+

+

+procedure Test3(P: bool, Q: bool, A: bool)

+  requires !A ==> P;

+{

+    while (*)

+      invariant {:verified_under A} P;

+      invariant {:verified_under A} Q;  // error

+    {}

+}

+

+procedure Test4(P: bool, Q: bool, A: bool)

+{

+    while (*)

+      invariant {:verified_under A} {:verified_under true} P;  // error

+      invariant {:verified_under A} {:verified_under true} Q;  // error

+    {}

+}

+

+

+procedure Test5(P: bool, Q: bool, A: bool)

+  requires !A ==> Q;

+{

+    while (*)

+      invariant {:verified_under A} {:verified_under true} P;  // error

+      invariant {:verified_under A} {:verified_under true} Q;

+    {}

+}

diff --git a/Test/test2/InvariantVerifiedUnder0.bpl.expect b/Test/test2/InvariantVerifiedUnder0.bpl.expect
new file mode 100644
index 00000000..171a6760
--- /dev/null
+++ b/Test/test2/InvariantVerifiedUnder0.bpl.expect
@@ -0,0 +1,23 @@
+InvariantVerifiedUnder0.bpl(7,7): Error BP5001: This assertion might not hold.

+Execution trace:

+    InvariantVerifiedUnder0.bpl(6,5): anon0

+InvariantVerifiedUnder0.bpl(23,7): Error BP5004: This loop invariant might not hold on entry.

+Execution trace:

+    InvariantVerifiedUnder0.bpl(22,5): anon0

+InvariantVerifiedUnder0.bpl(24,7): Error BP5004: This loop invariant might not hold on entry.

+Execution trace:

+    InvariantVerifiedUnder0.bpl(22,5): anon0

+InvariantVerifiedUnder0.bpl(34,7): Error BP5004: This loop invariant might not hold on entry.

+Execution trace:

+    InvariantVerifiedUnder0.bpl(32,5): anon0

+InvariantVerifiedUnder0.bpl(41,7): Error BP5004: This loop invariant might not hold on entry.

+Execution trace:

+    InvariantVerifiedUnder0.bpl(40,5): anon0

+InvariantVerifiedUnder0.bpl(42,7): Error BP5004: This loop invariant might not hold on entry.

+Execution trace:

+    InvariantVerifiedUnder0.bpl(40,5): anon0

+InvariantVerifiedUnder0.bpl(51,7): Error BP5004: This loop invariant might not hold on entry.

+Execution trace:

+    InvariantVerifiedUnder0.bpl(50,5): anon0

+

+Boogie program verifier finished with 1 verified, 7 errors