diff options
-rw-r--r-- | Test/snapshots/Snapshots6.v0.bpl | 2 | ||||
-rw-r--r-- | Test/snapshots/Snapshots6.v1.bpl | 3 | ||||
-rw-r--r-- | Test/snapshots/Snapshots7.v0.bpl | 2 | ||||
-rw-r--r-- | Test/snapshots/Snapshots7.v1.bpl | 3 | ||||
-rw-r--r-- | Test/snapshots/Snapshots8.v0.bpl | 15 | ||||
-rw-r--r-- | Test/snapshots/Snapshots8.v1.bpl | 16 | ||||
-rw-r--r-- | Test/snapshots/Snapshots9.v0.bpl | 15 | ||||
-rw-r--r-- | Test/snapshots/Snapshots9.v1.bpl | 16 | ||||
-rw-r--r-- | Test/snapshots/runtest.snapshot | 2 | ||||
-rw-r--r-- | Test/snapshots/runtest.snapshot.expect | 8 |
10 files changed, 77 insertions, 5 deletions
diff --git a/Test/snapshots/Snapshots6.v0.bpl b/Test/snapshots/Snapshots6.v0.bpl index 157fc45b..bdf9c14a 100644 --- a/Test/snapshots/Snapshots6.v0.bpl +++ b/Test/snapshots/Snapshots6.v0.bpl @@ -4,7 +4,7 @@ var y: int; procedure {:checksum "0"} M();
modifies x, y;
-implementation {:checksum "1"} M()
+implementation {:id "M"} {:checksum "1"} M()
{
y := 0;
diff --git a/Test/snapshots/Snapshots6.v1.bpl b/Test/snapshots/Snapshots6.v1.bpl index eb139546..be8b699d 100644 --- a/Test/snapshots/Snapshots6.v1.bpl +++ b/Test/snapshots/Snapshots6.v1.bpl @@ -4,7 +4,7 @@ var y: int; procedure {:checksum "0"} M();
modifies x, y;
-implementation {:checksum "1"} M()
+implementation {:id "M"} {:checksum "1"} M()
{
y := 0;
@@ -14,4 +14,5 @@ implementation {:checksum "1"} M() }
procedure {:checksum "3"} N();
+ // Change: more modified variables
modifies x, y;
diff --git a/Test/snapshots/Snapshots7.v0.bpl b/Test/snapshots/Snapshots7.v0.bpl index 6b99de1b..6e0932c8 100644 --- a/Test/snapshots/Snapshots7.v0.bpl +++ b/Test/snapshots/Snapshots7.v0.bpl @@ -5,7 +5,7 @@ var z: int; procedure {:checksum "0"} M();
modifies x, y, z;
-implementation {:checksum "1"} M()
+implementation {:id "M"} {:checksum "1"} M()
{
z := 0;
diff --git a/Test/snapshots/Snapshots7.v1.bpl b/Test/snapshots/Snapshots7.v1.bpl index bba0978b..8700e91c 100644 --- a/Test/snapshots/Snapshots7.v1.bpl +++ b/Test/snapshots/Snapshots7.v1.bpl @@ -5,7 +5,7 @@ var z: int; procedure {:checksum "0"} M();
modifies x, y, z;
-implementation {:checksum "1"} M()
+implementation {:id "M"} {:checksum "1"} M()
{
z := 0;
@@ -15,5 +15,6 @@ implementation {:checksum "1"} M() }
procedure {:checksum "3"} N();
+ // Change: fewer modified variables
modifies x;
ensures y < z;
diff --git a/Test/snapshots/Snapshots8.v0.bpl b/Test/snapshots/Snapshots8.v0.bpl new file mode 100644 index 00000000..73dcd9aa --- /dev/null +++ b/Test/snapshots/Snapshots8.v0.bpl @@ -0,0 +1,15 @@ +procedure {:checksum "0"} M(n: int);
+ requires 0 < n;
+
+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/Snapshots8.v1.bpl b/Test/snapshots/Snapshots8.v1.bpl new file mode 100644 index 00000000..de241c24 --- /dev/null +++ b/Test/snapshots/Snapshots8.v1.bpl @@ -0,0 +1,16 @@ +procedure {:checksum "0"} M(n: int);
+ requires 0 < n;
+
+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: stronger postcondition
+ ensures 42 < r;
diff --git a/Test/snapshots/Snapshots9.v0.bpl b/Test/snapshots/Snapshots9.v0.bpl new file mode 100644 index 00000000..73dcd9aa --- /dev/null +++ b/Test/snapshots/Snapshots9.v0.bpl @@ -0,0 +1,15 @@ +procedure {:checksum "0"} M(n: int);
+ requires 0 < n;
+
+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/Snapshots9.v1.bpl b/Test/snapshots/Snapshots9.v1.bpl new file mode 100644 index 00000000..d1886a6d --- /dev/null +++ b/Test/snapshots/Snapshots9.v1.bpl @@ -0,0 +1,16 @@ +procedure {:checksum "0"} M(n: int);
+ requires 0 < n;
+
+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/runtest.snapshot b/Test/snapshots/runtest.snapshot index 0a4ef6d9..f67e6be7 100644 --- a/Test/snapshots/runtest.snapshot +++ b/Test/snapshots/runtest.snapshot @@ -1,2 +1,2 @@ -// RUN: %boogie -verifySnapshots -verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl > "%t" +// RUN: %boogie -verifySnapshots -verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect index 0ba6f920..c0a171c4 100644 --- a/Test/snapshots/runtest.snapshot.expect +++ b/Test/snapshots/runtest.snapshot.expect @@ -90,3 +90,11 @@ Boogie program verifier finished with 0 verified, 1 error 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
+
+Boogie program verifier finished with 1 verified, 0 errors
|