Worked on an extension of the existing verification result caching.

13 files changed, 221 insertions, 1 deletions

diff --git a/Test/snapshots/Snapshots10.v0.bpl b/Test/snapshots/Snapshots10.v0.bpl
new file mode 100644
index 00000000..bdbb6b63
--- /dev/null
+++ b/Test/snapshots/Snapshots10.v0.bpl
@@ -0,0 +1,20 @@
+procedure {:checksum "0"} M(n: int);

+  requires 0 < n;

+

+implementation {:id "M"} {:checksum "1"} M(n: int)

+{

+    var x: int;

+

+    call x := N(n);

+

+    call O();

+

+    assert 0 <= x;

+}

+

+procedure {:checksum "2"} N(n: int) returns (r: int);

+  requires 0 < n;

+  ensures 0 < r;

+

+procedure {:checksum "3"} O();

+  ensures true;

diff --git a/Test/snapshots/Snapshots10.v1.bpl b/Test/snapshots/Snapshots10.v1.bpl
new file mode 100644
index 00000000..d4c09a5f
--- /dev/null
+++ b/Test/snapshots/Snapshots10.v1.bpl
@@ -0,0 +1,21 @@
+procedure {:checksum "0"} M(n: int);

+  requires 0 < n;

+

+implementation {:id "M"} {:checksum "1"} M(n: int)

+{

+    var x: int;

+

+    call x := N(n);

+

+    call O();

+

+    assert 0 <= x;

+}

+

+procedure {:checksum "4"} N(n: int) returns (r: int);

+  requires 0 < n;

+  // Change: stronger postcondition

+  ensures 42 < r;

+

+procedure {:checksum "3"} O();

+  ensures true;

diff --git a/Test/snapshots/Snapshots11.v0.bpl b/Test/snapshots/Snapshots11.v0.bpl
new file mode 100644
index 00000000..10b4ed43
--- /dev/null
+++ b/Test/snapshots/Snapshots11.v0.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "0"} M(n: int);

+

+implementation {:id "M"} {:checksum "1"} M(n: int)

+{

+    var x: int;

+

+    call x := N(n);

+

+    assert 0 <= x;

+}

+

+procedure {:checksum "2"} N(n: int) returns (r: int);

+  requires 0 < n;

+  ensures 0 < r;

diff --git a/Test/snapshots/Snapshots11.v1.bpl b/Test/snapshots/Snapshots11.v1.bpl
new file mode 100644
index 00000000..3c3ea476
--- /dev/null
+++ b/Test/snapshots/Snapshots11.v1.bpl
@@ -0,0 +1,15 @@
+procedure {:checksum "0"} M(n: int);

+

+implementation {:id "M"} {:checksum "1"} M(n: int)

+{

+    var x: int;

+

+    call x := N(n);

+

+    assert 0 <= x;

+}

+

+procedure {:checksum "3"} N(n: int) returns (r: int);

+  requires 0 < n;

+  // Change: weaker postcondition

+  ensures 0 <= r;

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

+

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

+{

+    call N();

+

+    assert false;

+}

+

+procedure {:checksum "2"} N();

+  ensures F();

+

+function {:checksum "3"} F() : bool

+{

+    false

+}

diff --git a/Test/snapshots/Snapshots12.v1.bpl b/Test/snapshots/Snapshots12.v1.bpl
new file mode 100644
index 00000000..f71e3c5f
--- /dev/null
+++ b/Test/snapshots/Snapshots12.v1.bpl
@@ -0,0 +1,16 @@
+procedure {:checksum "0"} M();

+

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

+{

+    call N();

+

+    assert false;

+}

+

+procedure {:checksum "2"} N();

+  ensures F();

+

+function {:checksum "4"} F() : bool

+{

+    true

+}

diff --git a/Test/snapshots/Snapshots13.v0.bpl b/Test/snapshots/Snapshots13.v0.bpl
new file mode 100644
index 00000000..79dfe2c3
--- /dev/null
+++ b/Test/snapshots/Snapshots13.v0.bpl
@@ -0,0 +1,21 @@
+procedure {:checksum "0"} M();

+

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

+{

+    call N();

+

+    assert false;

+}

+

+procedure {:checksum "2"} N();

+  ensures F() && G();

+

+function {:checksum "3"} F() : bool

+{

+    true

+}

+

+function {:checksum "4"} G() : bool

+{

+    false

+}

diff --git a/Test/snapshots/Snapshots13.v1.bpl b/Test/snapshots/Snapshots13.v1.bpl
new file mode 100644
index 00000000..a7ec6bfb
--- /dev/null
+++ b/Test/snapshots/Snapshots13.v1.bpl
@@ -0,0 +1,16 @@
+procedure {:checksum "0"} M();

+

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

+{

+    call N();

+

+    assert false;

+}

+

+procedure {:checksum "2"} N();

+  ensures F();

+

+function {:checksum "3"} F() : bool

+{

+    true

+}

diff --git a/Test/snapshots/Snapshots14.v0.bpl b/Test/snapshots/Snapshots14.v0.bpl
new file mode 100644
index 00000000..79dfe2c3
--- /dev/null
+++ b/Test/snapshots/Snapshots14.v0.bpl
@@ -0,0 +1,21 @@
+procedure {:checksum "0"} M();

+

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

+{

+    call N();

+

+    assert false;

+}

+

+procedure {:checksum "2"} N();

+  ensures F() && G();

+

+function {:checksum "3"} F() : bool

+{

+    true

+}

+

+function {:checksum "4"} G() : bool

+{

+    false

+}

diff --git a/Test/snapshots/Snapshots14.v1.bpl b/Test/snapshots/Snapshots14.v1.bpl
new file mode 100644
index 00000000..b33c3430
--- /dev/null
+++ b/Test/snapshots/Snapshots14.v1.bpl
@@ -0,0 +1,21 @@
+procedure {:checksum "0"} M();

+

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

+{

+    call N();

+

+    assert false;

+}

+

+procedure {:checksum "2"} N();

+  ensures F();

+

+function {:checksum "3"} F() : bool

+{

+    true

+}

+

+function {:checksum "4"} G() : bool

+{

+    false

+}

diff --git a/Test/snapshots/Snapshots9.v0.bpl b/Test/snapshots/Snapshots9.v0.bpl
index 73dcd9aa..5b2cf68c 100644
--- a/Test/snapshots/Snapshots9.v0.bpl
+++ b/Test/snapshots/Snapshots9.v0.bpl
@@ -12,4 +12,6 @@ implementation {:id "M"} {:checksum "1"} M(n: int)
 

 procedure {:checksum "2"} N(n: int) returns (r: int);

   requires 0 < n;

+  requires true;

   ensures 0 < r;

+  ensures true;

diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot
index 6646d9ea..d61e9e4a 100644
--- a/Test/snapshots/runtest.snapshot
+++ b/Test/snapshots/runtest.snapshot
@@ -1,2 +1,2 @@
-// RUN: %boogie -verifySnapshots:1 -verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl > "%t"
+// RUN: %boogie -verifySnapshots:2 -verifySeparately 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 > "%t"
 // RUN: %diff "%s.expect" "%t"
diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index c0a171c4..a370cbae 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -98,3 +98,40 @@ Boogie program verifier finished with 1 verified, 0 errors
 Boogie program verifier finished with 1 verified, 0 errors

 

 Boogie program verifier finished with 1 verified, 0 errors

+

+Boogie program verifier finished with 1 verified, 0 errors

+

+Boogie program verifier finished with 1 verified, 0 errors

+Snapshots11.v0.bpl(7,5): Error BP5002: A precondition for this call might not hold.

+Snapshots11.v0.bpl(13,3): Related location: This is the precondition that might not hold.

+Execution trace:

+    Snapshots11.v0.bpl(7,5): anon0

+

+Boogie program verifier finished with 0 verified, 1 error

+Snapshots11.v1.bpl(7,5): Error BP5002: A precondition for this call might not hold.

+Snapshots11.v1.bpl(13,3): Related location: This is the precondition that might not hold.

+Execution trace:

+    Snapshots11.v1.bpl(7,5): anon0

+

+Boogie program verifier finished with 0 verified, 1 error

+

+Boogie program verifier finished with 1 verified, 0 errors

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

+Execution trace:

+    Snapshots12.v1.bpl(5,5): anon0

+

+Boogie program verifier finished with 0 verified, 1 error

+

+Boogie program verifier finished with 1 verified, 0 errors

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

+Execution trace:

+    Snapshots13.v1.bpl(5,5): anon0

+

+Boogie program verifier finished with 0 verified, 1 error

+

+Boogie program verifier finished with 1 verified, 0 errors

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

+Execution trace:

+    Snapshots14.v1.bpl(5,5): anon0

+

+Boogie program verifier finished with 0 verified, 1 error