Make the dependency analysis for snapshot verification take 'where' clauses into account.

17 files changed, 62 insertions, 22 deletions

diff --git a/Test/snapshots/Answer b/Test/snapshots/Answer
index dc0ee8c1..7826d2f0 100644
--- a/Test/snapshots/Answer
+++ b/Test/snapshots/Answer
@@ -61,3 +61,21 @@ Execution trace:
     Snapshots3.v1.bpl(6,1): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

+

+Boogie program verifier finished with 3 verified, 0 errors

+Snapshots4.v1.bpl(23,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    Snapshots4.v1.bpl(23,5): anon0

+Snapshots4.v1.bpl(33,1): Error BP5003: A postcondition might not hold on this return path.

+Snapshots4.v1.bpl(28,3): Related location: This is the postcondition that might not hold.

+Execution trace:

+    Snapshots4.v1.bpl(33,1): anon0

+

+Boogie program verifier finished with 2 verified, 2 errors

+

+Boogie program verifier finished with 1 verified, 0 errors

+Snapshots5.v1.bpl(5,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    Snapshots5.v1.bpl(5,5): anon0

+

+Boogie program verifier finished with 0 verified, 1 error

diff --git a/Test/snapshots/Snapshots1.v0.bpl b/Test/snapshots/Snapshots1.v0.bpl
index d6d4332e..ea2c06bb 100644
--- a/Test/snapshots/Snapshots1.v0.bpl
+++ b/Test/snapshots/Snapshots1.v0.bpl
@@ -1,6 +1,6 @@
 procedure {:checksum "P1$proc#0"} P1();

 // Action: verify

-implementation {:checksum "P1$impl#0"} P1()

+implementation {:id "P1"} {:checksum "P1$impl#0"} P1()

 {

     call P2();

 }

@@ -8,7 +8,7 @@ implementation {:checksum "P1$impl#0"} P1()
 

 procedure {:checksum "P2$proc#0"} P2();

 // Action: verify

-implementation {:checksum "P2$impl#0"} P2()

+implementation {:id "P2"} {:checksum "P2$impl#0"} P2()

 {

     assert 1 != 1;

 }

diff --git a/Test/snapshots/Snapshots1.v1.bpl b/Test/snapshots/Snapshots1.v1.bpl
index c0014a03..9fbe44af 100644
--- a/Test/snapshots/Snapshots1.v1.bpl
+++ b/Test/snapshots/Snapshots1.v1.bpl
@@ -1,6 +1,6 @@
 procedure {:checksum "P1$proc#0"} P1();

 // Action: skip

-implementation {:checksum "P1$impl#0"} P1()

+implementation {:id "P1"} {:checksum "P1$impl#0"} P1()

 {

     call P2();

 }

@@ -8,7 +8,7 @@ implementation {:checksum "P1$impl#0"} P1()
 

 procedure {:checksum "P2$proc#0"} P2();

 // Action: verify

-implementation {:checksum "P2$impl#1"} P2()

+implementation {:id "P2"} {:checksum "P2$impl#1"} P2()

 {

     assert 2 != 2;

 }

diff --git a/Test/snapshots/Snapshots1.v2.bpl b/Test/snapshots/Snapshots1.v2.bpl
index 49e8b389..c699631e 100644
--- a/Test/snapshots/Snapshots1.v2.bpl
+++ b/Test/snapshots/Snapshots1.v2.bpl
@@ -1,6 +1,6 @@
 procedure {:checksum "P1$proc#0"} P1();

 // Action: verify

-implementation {:checksum "P1$impl#0"} P1()

+implementation {:id "P1"} {:checksum "P1$impl#0"} P1()

 {

     call P2();

 }

@@ -9,7 +9,7 @@ implementation {:checksum "P1$impl#0"} P1()
 procedure {:checksum "P2$proc#1"} P2();

   requires false;

 // Action: verify

-implementation {:checksum "P2$impl#1"} P2()

+implementation {:id "P2"} {:checksum "P2$impl#1"} P2()

 {

     assert 2 != 2;

 }

diff --git a/Test/snapshots/Snapshots2.v0.bpl b/Test/snapshots/Snapshots2.v0.bpl
index 63f1995d..91f05a0d 100644
--- a/Test/snapshots/Snapshots2.v0.bpl
+++ b/Test/snapshots/Snapshots2.v0.bpl
@@ -1,6 +1,6 @@
 procedure {:checksum "P0$proc#0"} P0();

 // Action: verify

-implementation {:checksum "P0$impl#0"} P0()

+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()

 {

     call P0();

 }

diff --git a/Test/snapshots/Snapshots2.v1.bpl b/Test/snapshots/Snapshots2.v1.bpl
index a00bdecb..1dec4954 100644
--- a/Test/snapshots/Snapshots2.v1.bpl
+++ b/Test/snapshots/Snapshots2.v1.bpl
@@ -1,6 +1,6 @@
 procedure {:checksum "P0$proc#0"} P0();

 // Action: skip

-implementation {:checksum "P0$impl#0"} P0()

+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()

 {

     call P0();

 }

diff --git a/Test/snapshots/Snapshots2.v2.bpl b/Test/snapshots/Snapshots2.v2.bpl
index 02c5e6df..567191d3 100644
--- a/Test/snapshots/Snapshots2.v2.bpl
+++ b/Test/snapshots/Snapshots2.v2.bpl
@@ -1,7 +1,7 @@
 procedure {:checksum "P0$proc#2"} P0();

 requires F0();

 // Action: verify (procedure changed)

-implementation {:checksum "P0$impl#0"} P0()

+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()

 {

     call P0();

 }

diff --git a/Test/snapshots/Snapshots2.v3.bpl b/Test/snapshots/Snapshots2.v3.bpl
index 5bf59435..7f6c4a82 100644
--- a/Test/snapshots/Snapshots2.v3.bpl
+++ b/Test/snapshots/Snapshots2.v3.bpl
@@ -1,7 +1,7 @@
 procedure {:checksum "P0$proc#2"} P0();

 requires F0();

 // Action: verify (function changed)

-implementation {:checksum "P0$impl#0"} P0()

+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()

 {

     call P0();

 }

diff --git a/Test/snapshots/Snapshots2.v4.bpl b/Test/snapshots/Snapshots2.v4.bpl
index 3d11ee27..abbf5e86 100644
--- a/Test/snapshots/Snapshots2.v4.bpl
+++ b/Test/snapshots/Snapshots2.v4.bpl
@@ -1,7 +1,7 @@
 procedure {:checksum "P0$proc#2"} P0();

 requires F0();

 // Action: skip

-implementation {:checksum "P0$impl#0"} P0()

+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()

 {

     call P0();

 }

diff --git a/Test/snapshots/Snapshots2.v5.bpl b/Test/snapshots/Snapshots2.v5.bpl
index 5ff7bb4d..55d08527 100644
--- a/Test/snapshots/Snapshots2.v5.bpl
+++ b/Test/snapshots/Snapshots2.v5.bpl
@@ -2,7 +2,7 @@ procedure {:checksum "P0$proc#5"} P0();
 requires F0();

 ensures F0();

 // Action: verify (procedure changed)

-implementation {:checksum "P0$impl#0"} P0()

+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()

 {

     call P0();

 }

diff --git a/Test/snapshots/Snapshots3.v0.bpl b/Test/snapshots/Snapshots3.v0.bpl
index 65dd49ff..7ab7aa5c 100644
--- a/Test/snapshots/Snapshots3.v0.bpl
+++ b/Test/snapshots/Snapshots3.v0.bpl
@@ -1,7 +1,7 @@
 procedure {:checksum "P0$proc#0"} P0();

 ensures G();

 // Action: verify

-implementation {:checksum "P0$impl#0"} P0()

+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()

 {

 }

 

diff --git a/Test/snapshots/Snapshots3.v1.bpl b/Test/snapshots/Snapshots3.v1.bpl
index 329382ac..5eb57e78 100644
--- a/Test/snapshots/Snapshots3.v1.bpl
+++ b/Test/snapshots/Snapshots3.v1.bpl
@@ -1,7 +1,7 @@
 procedure {:checksum "P0$proc#0"} P0();

 ensures G();

 // Action: verify

-implementation {:checksum "P0$impl#0"} P0()

+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()

 {

 }

 

diff --git a/Test/snapshots/Snapshots4.v0.bpl b/Test/snapshots/Snapshots4.v0.bpl
index 430aee99..59a42289 100644
--- a/Test/snapshots/Snapshots4.v0.bpl
+++ b/Test/snapshots/Snapshots4.v0.bpl
@@ -1,13 +1,13 @@
 procedure {:checksum "P0$proc#0"} P0();

 // Action: verify

-implementation {:checksum "P0$impl#0"} P0()

+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()

 {

 }

 

 

 procedure {:checksum "P1$proc#0"} P1();

 // Action: verify

-implementation {:checksum "P1$impl#0"} P1()

+implementation {:id "P1"} {:checksum "P1$impl#0"} P1()

 {

     call P2();

 }

@@ -19,7 +19,7 @@ procedure {:checksum "P2$proc#0"} P2();
 

 procedure {:checksum "P3$proc#0"} P3();

 // Action: verify

-implementation {:checksum "P3$impl#0"} P3()

+implementation {:id "P3"} {:checksum "P3$impl#0"} P3()

 {

 }

 

diff --git a/Test/snapshots/Snapshots4.v1.bpl b/Test/snapshots/Snapshots4.v1.bpl
index 025a3f5f..392a1648 100644
--- a/Test/snapshots/Snapshots4.v1.bpl
+++ b/Test/snapshots/Snapshots4.v1.bpl
@@ -1,7 +1,7 @@
 procedure {:checksum "P0$proc#0"} P0();

 // Action: skip

 // Priority: 0

-implementation {:checksum "P0$impl#0"} P0()

+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()

 {

 }

 

@@ -9,7 +9,7 @@ implementation {:checksum "P0$impl#0"} P0()
 procedure {:checksum "P1$proc#0"} P1();

 // Action: verify

 // Priority: 1

-implementation {:checksum "P1$impl#0"} P1()

+implementation {:id "P1"} {:checksum "P1$impl#0"} P1()

 {

     call P2();

 }

@@ -18,7 +18,7 @@ implementation {:checksum "P1$impl#0"} P1()
 procedure {:checksum "P3$proc#0"} P3();

 // Action: verify

 // Priority: 2

-implementation {:checksum "P3$impl#1"} P3()

+implementation {:id "P3"} {:checksum "P3$impl#1"} P3()

 {

     assert false;

 }

@@ -28,7 +28,7 @@ procedure {:checksum "P2$proc#0"} P2();
   ensures G();

 // Action: verify

 // Priority: 3

-implementation {:checksum "P2$impl#0"} P2()

+implementation {:id "P2"} {:checksum "P2$impl#0"} P2()

 {

 }

 

diff --git a/Test/snapshots/Snapshots5.v0.bpl b/Test/snapshots/Snapshots5.v0.bpl
new file mode 100644
index 00000000..b8652c7b
--- /dev/null
+++ b/Test/snapshots/Snapshots5.v0.bpl
@@ -0,0 +1,11 @@
+procedure {:checksum "P0$proc#0"} P0(n: int where F(n));

+// Action: verify

+implementation {:id "P0"} {:checksum "P0$impl#0"} P0(n: int)

+{

+    assert false;

+}

+

+function {:checksum "F#1"} F(n: int) : bool

+{

+    false

+}

diff --git a/Test/snapshots/Snapshots5.v1.bpl b/Test/snapshots/Snapshots5.v1.bpl
new file mode 100644
index 00000000..b42b1576
--- /dev/null
+++ b/Test/snapshots/Snapshots5.v1.bpl
@@ -0,0 +1,11 @@
+procedure {:checksum "P0$proc#0"} P0(n: int where F(n));

+// Action: verify

+implementation {:id "P0"} {:checksum "P0$impl#0"} P0(n: int)

+{

+    assert false;

+}

+

+function {:checksum "F#0"} F(n: int) : bool

+{

+    true

+}

diff --git a/Test/snapshots/runtest.bat b/Test/snapshots/runtest.bat
index e54a19bc..b7cb641a 100644
--- a/Test/snapshots/runtest.bat
+++ b/Test/snapshots/runtest.bat
@@ -4,5 +4,5 @@ setlocal
 set BOOGIEDIR=..\..\Binaries

 set BGEXE=%BOOGIEDIR%\Boogie.exe

 

-%BGEXE% %* /verifySnapshots /verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl

+%BGEXE% %* /verifySnapshots /verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl