From 98bcde1368eb6a5df44cf252e3a2f8d8f509a0df Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Mon, 23 Jun 2014 23:34:23 +0200
Subject: Worked on an extension of the existing verification result caching.

---
 Test/snapshots/Snapshots10.v0.bpl      | 20 ++++++++++++++++++
 Test/snapshots/Snapshots10.v1.bpl      | 21 +++++++++++++++++++
 Test/snapshots/Snapshots11.v0.bpl      | 14 +++++++++++++
 Test/snapshots/Snapshots11.v1.bpl      | 15 ++++++++++++++
 Test/snapshots/Snapshots12.v0.bpl      | 16 +++++++++++++++
 Test/snapshots/Snapshots12.v1.bpl      | 16 +++++++++++++++
 Test/snapshots/Snapshots13.v0.bpl      | 21 +++++++++++++++++++
 Test/snapshots/Snapshots13.v1.bpl      | 16 +++++++++++++++
 Test/snapshots/Snapshots14.v0.bpl      | 21 +++++++++++++++++++
 Test/snapshots/Snapshots14.v1.bpl      | 21 +++++++++++++++++++
 Test/snapshots/Snapshots9.v0.bpl       |  2 ++
 Test/snapshots/runtest.snapshot        |  2 +-
 Test/snapshots/runtest.snapshot.expect | 37 ++++++++++++++++++++++++++++++++++
 13 files changed, 221 insertions(+), 1 deletion(-)
 create mode 100644 Test/snapshots/Snapshots10.v0.bpl
 create mode 100644 Test/snapshots/Snapshots10.v1.bpl
 create mode 100644 Test/snapshots/Snapshots11.v0.bpl
 create mode 100644 Test/snapshots/Snapshots11.v1.bpl
 create mode 100644 Test/snapshots/Snapshots12.v0.bpl
 create mode 100644 Test/snapshots/Snapshots12.v1.bpl
 create mode 100644 Test/snapshots/Snapshots13.v0.bpl
 create mode 100644 Test/snapshots/Snapshots13.v1.bpl
 create mode 100644 Test/snapshots/Snapshots14.v0.bpl
 create mode 100644 Test/snapshots/Snapshots14.v1.bpl

(limited to 'Test/snapshots')

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
-- 
cgit v1.2.3