summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2014-06-23 23:34:23 +0200
committerGravatar wuestholz <unknown>2014-06-23 23:34:23 +0200
commit98bcde1368eb6a5df44cf252e3a2f8d8f509a0df (patch)
tree0a6643566ab3c2e4884f1ba3f2858dd65fe8ee5a /Test
parent81e96e8c695b582402a17c8957616ee72d6ebb29 (diff)
Worked on an extension of the existing verification result caching.
Diffstat (limited to 'Test')
-rw-r--r--Test/snapshots/Snapshots10.v0.bpl20
-rw-r--r--Test/snapshots/Snapshots10.v1.bpl21
-rw-r--r--Test/snapshots/Snapshots11.v0.bpl14
-rw-r--r--Test/snapshots/Snapshots11.v1.bpl15
-rw-r--r--Test/snapshots/Snapshots12.v0.bpl16
-rw-r--r--Test/snapshots/Snapshots12.v1.bpl16
-rw-r--r--Test/snapshots/Snapshots13.v0.bpl21
-rw-r--r--Test/snapshots/Snapshots13.v1.bpl16
-rw-r--r--Test/snapshots/Snapshots14.v0.bpl21
-rw-r--r--Test/snapshots/Snapshots14.v1.bpl21
-rw-r--r--Test/snapshots/Snapshots9.v0.bpl2
-rw-r--r--Test/snapshots/runtest.snapshot2
-rw-r--r--Test/snapshots/runtest.snapshot.expect37
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