From c8c15f672dc42fca1db9b0f20549ef49b48889e8 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Wed, 29 Oct 2014 14:11:54 +0100
Subject: Added a test for the verification result caching.

---
 Test/snapshots/Snapshots29.v0.bpl         | 15 +++++++++++++++
 Test/snapshots/Snapshots29.v1.bpl         | 15 +++++++++++++++
 Test/snapshots/runtest.AI.snapshot        |  2 ++
 Test/snapshots/runtest.AI.snapshot.expect |  9 +++++++++
 4 files changed, 41 insertions(+)
 create mode 100644 Test/snapshots/Snapshots29.v0.bpl
 create mode 100644 Test/snapshots/Snapshots29.v1.bpl
 create mode 100644 Test/snapshots/runtest.AI.snapshot
 create mode 100644 Test/snapshots/runtest.AI.snapshot.expect

(limited to 'Test/snapshots')

diff --git a/Test/snapshots/Snapshots29.v0.bpl b/Test/snapshots/Snapshots29.v0.bpl
new file mode 100644
index 00000000..f4087f90
--- /dev/null
+++ b/Test/snapshots/Snapshots29.v0.bpl
@@ -0,0 +1,15 @@
+procedure {:checksum "0"} P();
+
+implementation {:id "P"} {:checksum "1"} P()
+{
+    var i: int;
+
+    i := 0;
+
+    while (*)
+    {
+        i := 0;
+    }
+
+    assert i == 0;
+}
diff --git a/Test/snapshots/Snapshots29.v1.bpl b/Test/snapshots/Snapshots29.v1.bpl
new file mode 100644
index 00000000..5211f832
--- /dev/null
+++ b/Test/snapshots/Snapshots29.v1.bpl
@@ -0,0 +1,15 @@
+procedure {:checksum "0"} P();
+
+implementation {:id "P"} {:checksum "2"} P()
+{
+    var i: int;
+
+    i := 0;
+
+    while (*)
+    {
+        i := 1;
+    }
+
+    assert i == 0;
+}
diff --git a/Test/snapshots/runtest.AI.snapshot b/Test/snapshots/runtest.AI.snapshot
new file mode 100644
index 00000000..51de91e8
--- /dev/null
+++ b/Test/snapshots/runtest.AI.snapshot
@@ -0,0 +1,2 @@
+// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately Snapshots29.bpl > "%t"
+// RUN: %diff "%s.expect" "%t"
diff --git a/Test/snapshots/runtest.AI.snapshot.expect b/Test/snapshots/runtest.AI.snapshot.expect
new file mode 100644
index 00000000..be2666d4
--- /dev/null
+++ b/Test/snapshots/runtest.AI.snapshot.expect
@@ -0,0 +1,9 @@
+Processing command (at Snapshots29.v0.bpl(14,5)) assert i == 0 /* checksum: 15-7D-7A-B4-3A-9B-FD-1E-77-5A-56-1F-3A-18-C1-FD */ ;
+  >>> did nothing
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots29.v1.bpl(14,5)) assert i == 0 /* checksum: 8F-25-CD-62-0E-E2-33-AF-1A-28-E2-9A-F5-AC-02-2D */ ;
+  >>> did nothing
+Snapshots29.v1.bpl(14,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
-- 
cgit v1.2.3