Added more tests (snapshots).

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