Merge

15 files changed, 286 insertions, 1 deletions

diff --git a/Test/snapshots/Answer b/Test/snapshots/Answer
index 434cdfda..676f0323 100644
--- a/Test/snapshots/Answer
+++ b/Test/snapshots/Answer
@@ -1,3 +1,5 @@
+

+-------------------- Snapshots0 --------------------

 Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.

 Execution trace:

     Snapshots0.v0.bpl(41,5): anon0

@@ -25,3 +27,45 @@ Execution trace:
     Snapshots0.v0.bpl(41,5): anon0

 

 Boogie program verifier finished with 2 verified, 1 error

+

+-------------------- Snapshots1 --------------------

+Snapshots1.v0.bpl(13,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    Snapshots1.v0.bpl(13,5): anon0

+

+Boogie program verifier finished with 1 verified, 1 error

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

+Execution trace:

+    Snapshots1.v1.bpl(13,5): anon0

+

+Boogie program verifier finished with 1 verified, 1 error

+Snapshots1.v2.bpl(5,5): Error BP5002: A precondition for this call might not hold.

+Snapshots1.v2.bpl(10,3): Related location: This is the precondition that might not hold.

+Execution trace:

+    Snapshots1.v2.bpl(5,5): anon0

+

+Boogie program verifier finished with 1 verified, 1 error

+

+-------------------- Snapshots2 --------------------

+

+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

+

+-------------------- Snapshots3 --------------------

+

+Boogie program verifier finished with 1 verified, 0 errors

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

+Snapshots3.v1.bpl(2,1): Related location: This is the postcondition that might not hold.

+Execution trace:

+    Snapshots3.v1.bpl(6,1): anon0

+

+Boogie program verifier finished with 0 verified, 1 error

diff --git a/Test/snapshots/Snapshots1.v0.bpl b/Test/snapshots/Snapshots1.v0.bpl
new file mode 100644
index 00000000..d6d4332e
--- /dev/null
+++ b/Test/snapshots/Snapshots1.v0.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "P1$proc#0"} P1();

+// Action: verify

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

+{

+    call P2();

+}

+

+

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

+// Action: verify

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

+{

+    assert 1 != 1;

+}

diff --git a/Test/snapshots/Snapshots1.v1.bpl b/Test/snapshots/Snapshots1.v1.bpl
new file mode 100644
index 00000000..c0014a03
--- /dev/null
+++ b/Test/snapshots/Snapshots1.v1.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "P1$proc#0"} P1();

+// Action: skip

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

+{

+    call P2();

+}

+

+

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

+// Action: verify

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

+{

+    assert 2 != 2;

+}

diff --git a/Test/snapshots/Snapshots1.v2.bpl b/Test/snapshots/Snapshots1.v2.bpl
new file mode 100644
index 00000000..49e8b389
--- /dev/null
+++ b/Test/snapshots/Snapshots1.v2.bpl
@@ -0,0 +1,15 @@
+procedure {:checksum "P1$proc#0"} P1();

+// Action: verify

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

+{

+    call P2();

+}

+

+

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

+  requires false;

+// Action: verify

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

+{

+    assert 2 != 2;

+}

diff --git a/Test/snapshots/Snapshots2.v0.bpl b/Test/snapshots/Snapshots2.v0.bpl
new file mode 100644
index 00000000..63f1995d
--- /dev/null
+++ b/Test/snapshots/Snapshots2.v0.bpl
@@ -0,0 +1,12 @@
+procedure {:checksum "P0$proc#0"} P0();

+// Action: verify

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

+{

+    call P0();

+}

+

+

+function F0() : bool

+{

+    true

+}

diff --git a/Test/snapshots/Snapshots2.v1.bpl b/Test/snapshots/Snapshots2.v1.bpl
new file mode 100644
index 00000000..a00bdecb
--- /dev/null
+++ b/Test/snapshots/Snapshots2.v1.bpl
@@ -0,0 +1,12 @@
+procedure {:checksum "P0$proc#0"} P0();

+// Action: skip

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

+{

+    call P0();

+}

+

+

+function F0() : bool

+{

+    true

+}

diff --git a/Test/snapshots/Snapshots2.v2.bpl b/Test/snapshots/Snapshots2.v2.bpl
new file mode 100644
index 00000000..02c5e6df
--- /dev/null
+++ b/Test/snapshots/Snapshots2.v2.bpl
@@ -0,0 +1,13 @@
+procedure {:checksum "P0$proc#2"} P0();

+requires F0();

+// Action: verify (procedure changed)

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

+{

+    call P0();

+}

+

+

+function {:checksum "F0#0"} F0() : bool

+{

+    true

+}

diff --git a/Test/snapshots/Snapshots2.v3.bpl b/Test/snapshots/Snapshots2.v3.bpl
new file mode 100644
index 00000000..5bf59435
--- /dev/null
+++ b/Test/snapshots/Snapshots2.v3.bpl
@@ -0,0 +1,13 @@
+procedure {:checksum "P0$proc#2"} P0();

+requires F0();

+// Action: verify (function changed)

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

+{

+    call P0();

+}

+

+

+function {:checksum "F0#1"} F0() : bool

+{

+    false

+}

diff --git a/Test/snapshots/Snapshots2.v4.bpl b/Test/snapshots/Snapshots2.v4.bpl
new file mode 100644
index 00000000..3d11ee27
--- /dev/null
+++ b/Test/snapshots/Snapshots2.v4.bpl
@@ -0,0 +1,13 @@
+procedure {:checksum "P0$proc#2"} P0();

+requires F0();

+// Action: skip

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

+{

+    call P0();

+}

+

+

+function {:checksum "F0#1"} F0() : bool

+{

+    false

+}

diff --git a/Test/snapshots/Snapshots2.v5.bpl b/Test/snapshots/Snapshots2.v5.bpl
new file mode 100644
index 00000000..5ff7bb4d
--- /dev/null
+++ b/Test/snapshots/Snapshots2.v5.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "P0$proc#5"} P0();

+requires F0();

+ensures F0();

+// Action: verify (procedure changed)

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

+{

+    call P0();

+}

+

+

+function {:checksum "F0#1"} F0() : bool

+{

+    false

+}

diff --git a/Test/snapshots/Snapshots3.v0.bpl b/Test/snapshots/Snapshots3.v0.bpl
new file mode 100644
index 00000000..65dd49ff
--- /dev/null
+++ b/Test/snapshots/Snapshots3.v0.bpl
@@ -0,0 +1,18 @@
+procedure {:checksum "P0$proc#0"} P0();

+ensures G();

+// Action: verify

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

+{

+}

+

+

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

+{

+    true

+}

+

+

+function {:checksum "G#0"} G() : bool

+{

+    F()

+}

diff --git a/Test/snapshots/Snapshots3.v1.bpl b/Test/snapshots/Snapshots3.v1.bpl
new file mode 100644
index 00000000..329382ac
--- /dev/null
+++ b/Test/snapshots/Snapshots3.v1.bpl
@@ -0,0 +1,18 @@
+procedure {:checksum "P0$proc#0"} P0();

+ensures G();

+// Action: verify

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

+{

+}

+

+

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

+{

+    false

+}

+

+

+function {:checksum "G#0"} G() : bool

+{

+    F()

+}

diff --git a/Test/snapshots/Snapshots4.v0.bpl b/Test/snapshots/Snapshots4.v0.bpl
new file mode 100644
index 00000000..430aee99
--- /dev/null
+++ b/Test/snapshots/Snapshots4.v0.bpl
@@ -0,0 +1,36 @@
+procedure {:checksum "P0$proc#0"} P0();

+// Action: verify

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

+{

+}

+

+

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

+// Action: verify

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

+{

+    call P2();

+}

+

+

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

+  ensures G();

+

+

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

+// Action: verify

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

+{

+}

+

+

+function {:checksum "G#0"} G() : bool

+{

+    F()

+}

+

+

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

+{

+    true

+}

diff --git a/Test/snapshots/Snapshots4.v1.bpl b/Test/snapshots/Snapshots4.v1.bpl
new file mode 100644
index 00000000..025a3f5f
--- /dev/null
+++ b/Test/snapshots/Snapshots4.v1.bpl
@@ -0,0 +1,45 @@
+procedure {:checksum "P0$proc#0"} P0();

+// Action: skip

+// Priority: 0

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

+{

+}

+

+

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

+// Action: verify

+// Priority: 1

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

+{

+    call P2();

+}

+

+

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

+// Action: verify

+// Priority: 2

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

+{

+    assert false;

+}

+

+

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

+  ensures G();

+// Action: verify

+// Priority: 3

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

+{

+}

+

+

+function {:checksum "G#0"} G() : bool

+{

+    F()

+}

+

+

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

+{

+    false

+}

diff --git a/Test/snapshots/runtest.bat b/Test/snapshots/runtest.bat
index 05421b85..663cef07 100644
--- a/Test/snapshots/runtest.bat
+++ b/Test/snapshots/runtest.bat
@@ -4,4 +4,8 @@ setlocal
 set BOOGIEDIR=..\..\Binaries

 set BGEXE=%BOOGIEDIR%\Boogie.exe

 

-%BGEXE% %* /verifySnapshots Snapshots0.bpl

+for %%f in (Snapshots0 Snapshots1 Snapshots2 Snapshots3) do (

+  echo.

+  echo -------------------- %%f --------------------

+  %BGEXE% %* /verifySnapshots %%f.bpl

+)