From c7a2a70a879e2506f6470e0abab2e03b1b60408a Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Mon, 10 Nov 2014 14:01:58 +0100
Subject: Fixed issue in the verification result caching.

---
 Test/snapshots/Snapshots30.v0.bpl      | 13 +++++++++++++
 Test/snapshots/Snapshots30.v1.bpl      | 14 ++++++++++++++
 Test/snapshots/runtest.snapshot        |  2 +-
 Test/snapshots/runtest.snapshot.expect | 32 +++++++++++++++++++++++++++++++-
 4 files changed, 59 insertions(+), 2 deletions(-)
 create mode 100644 Test/snapshots/Snapshots30.v0.bpl
 create mode 100644 Test/snapshots/Snapshots30.v1.bpl

(limited to 'Test')

diff --git a/Test/snapshots/Snapshots30.v0.bpl b/Test/snapshots/Snapshots30.v0.bpl
new file mode 100644
index 00000000..459c4007
--- /dev/null
+++ b/Test/snapshots/Snapshots30.v0.bpl
@@ -0,0 +1,13 @@
+procedure {:checksum "0"} P();
+
+implementation {:id "P"} {:checksum "1"} P()
+{
+    call Q();
+}
+
+procedure {:checksum "2"} Q();
+  requires 0 == 0;
+  requires 1 == 1;
+  requires 2 != 2;
+  requires 3 == 3;
+  requires 4 == 4;
diff --git a/Test/snapshots/Snapshots30.v1.bpl b/Test/snapshots/Snapshots30.v1.bpl
new file mode 100644
index 00000000..089a1939
--- /dev/null
+++ b/Test/snapshots/Snapshots30.v1.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "0"} P();
+
+implementation {:id "P"} {:checksum "2"} P()
+{
+    call Q();
+    assert 5 == 5;
+}
+
+procedure {:checksum "2"} Q();
+  requires 0 == 0;
+  requires 1 == 1;
+  requires 2 != 2;
+  requires 3 == 3;
+  requires 4 == 4;
diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot
index 484fa8e2..fb476128 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 > "%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 > "%t"
 // RUN: %diff "%s.expect" "%t"
diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index f34fefbe..d8642441 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -72,7 +72,7 @@ Processing command (at Snapshots2.v5.bpl(7,5)) assume {:precondition_previous_sn
 Processing command (at Snapshots2.v5.bpl(7,5)) assert F0();
   >>> MarkAsFullyVerified
 Processing command (at Snapshots2.v5.bpl(3,1)) assert F0();
-  >>> DoNothingToAssert
+  >>> MarkAsFullyVerified
 
 Boogie program verifier finished with 1 verified, 0 errors
 Processing command (at Snapshots3.v0.bpl(2,1)) assert G();
@@ -516,3 +516,33 @@ Processing command (at Snapshots28.v1.bpl(15,5)) assert x == 0;
 Snapshots28.v1.bpl(15,5): Error BP5001: This assertion might not hold.
 
 Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots30.v0.bpl(5,5)) assert 0 == 0;
+  >>> DoNothingToAssert
+Processing command (at Snapshots30.v0.bpl(5,5)) assert 1 == 1;
+  >>> DoNothingToAssert
+Processing command (at Snapshots30.v0.bpl(5,5)) assert 2 != 2;
+  >>> DoNothingToAssert
+Processing command (at Snapshots30.v0.bpl(5,5)) assert 3 == 3;
+  >>> DoNothingToAssert
+Processing command (at Snapshots30.v0.bpl(5,5)) assert 4 == 4;
+  >>> DoNothingToAssert
+Snapshots30.v0.bpl(5,5): Error BP5002: A precondition for this call might not hold.
+Snapshots30.v0.bpl(11,3): Related location: This is the precondition that might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots30.v1.bpl(5,5)) assert 0 == 0;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots30.v1.bpl(5,5)) assert 1 == 1;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots30.v1.bpl(5,5)) assert 2 != 2;
+  >>> RecycleError
+Processing command (at Snapshots30.v1.bpl(5,5)) assert 3 == 3;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots30.v1.bpl(5,5)) assert 4 == 4;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots30.v1.bpl(6,5)) assert 5 == 5;
+  >>> DoNothingToAssert
+Snapshots30.v0.bpl(5,5): Error BP5002: A precondition for this call might not hold.
+Snapshots30.v0.bpl(11,3): Related location: This is the precondition that might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
-- 
cgit v1.2.3