Worked on the verification result caching.

8 files changed, 139 insertions, 10 deletions

diff --git a/Test/snapshots/Snapshots25.v0.bpl b/Test/snapshots/Snapshots25.v0.bpl
new file mode 100644
index 00000000..5276f1dd
--- /dev/null
+++ b/Test/snapshots/Snapshots25.v0.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "0"} M();

+

+implementation {:id "M"} {:checksum "1"} M()

+{

+    var x: int;

+

+    while (*)

+    {

+        x := 0;

+    }

+

+    assert 0 == 0;

+    assert x != x;

+}

diff --git a/Test/snapshots/Snapshots25.v1.bpl b/Test/snapshots/Snapshots25.v1.bpl
new file mode 100644
index 00000000..fb735930
--- /dev/null
+++ b/Test/snapshots/Snapshots25.v1.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "0"} M();

+

+implementation {:id "M"} {:checksum "2"} M()

+{

+    var x: int;

+

+    while (*)

+    {

+        x := 1;

+    }

+

+    assert 0 == 0;

+    assert x != x;

+}

diff --git a/Test/snapshots/Snapshots26.v0.bpl b/Test/snapshots/Snapshots26.v0.bpl
new file mode 100644
index 00000000..5276f1dd
--- /dev/null
+++ b/Test/snapshots/Snapshots26.v0.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "0"} M();

+

+implementation {:id "M"} {:checksum "1"} M()

+{

+    var x: int;

+

+    while (*)

+    {

+        x := 0;

+    }

+

+    assert 0 == 0;

+    assert x != x;

+}

diff --git a/Test/snapshots/Snapshots26.v1.bpl b/Test/snapshots/Snapshots26.v1.bpl
new file mode 100644
index 00000000..7c2e3292
--- /dev/null
+++ b/Test/snapshots/Snapshots26.v1.bpl
@@ -0,0 +1,15 @@
+procedure {:checksum "0"} M();

+

+implementation {:id "M"} {:checksum "2"} M()

+{

+    var x: int;

+

+    while (*)

+    {

+        x := 0;

+        x := x + 1;

+    }

+

+    assert 0 == 0;

+    assert x != x;

+}

diff --git a/Test/snapshots/Snapshots27.v0.bpl b/Test/snapshots/Snapshots27.v0.bpl
new file mode 100644
index 00000000..5276f1dd
--- /dev/null
+++ b/Test/snapshots/Snapshots27.v0.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "0"} M();

+

+implementation {:id "M"} {:checksum "1"} M()

+{

+    var x: int;

+

+    while (*)

+    {

+        x := 0;

+    }

+

+    assert 0 == 0;

+    assert x != x;

+}

diff --git a/Test/snapshots/Snapshots27.v1.bpl b/Test/snapshots/Snapshots27.v1.bpl
new file mode 100644
index 00000000..4d60e149
--- /dev/null
+++ b/Test/snapshots/Snapshots27.v1.bpl
@@ -0,0 +1,16 @@
+procedure {:checksum "0"} M();

+

+implementation {:id "M"} {:checksum "2"} M()

+{

+    var x: int;

+    var y: int;

+

+    while (*)

+    {

+        x := 0;

+        y := 0;

+    }

+

+    assert 0 == 0;

+    assert x != x;

+}

diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot
index d5907196..2924b15a 100644
--- a/Test/snapshots/runtest.snapshot
+++ b/Test/snapshots/runtest.snapshot
@@ -1,2 +1,2 @@
-// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl Snapshots22.bpl Snapshots23.bpl Snapshots24.bpl > "%t"
+// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl Snapshots22.bpl Snapshots23.bpl Snapshots24.bpl Snapshots25.bpl Snapshots26.bpl Snapshots27.bpl > "%t"
 // RUN: %diff "%s.expect" "%t"
diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index f8b36963..bc847ebe 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -296,11 +296,11 @@ Processing call to procedure N in implementation M (at Snapshots17.v1.bpl(23,9))
   >>> added after: a##post##2 := a##post##2 && false;

 Processing command (at Snapshots17.v1.bpl(28,5)) assert true /* checksum: 17-6D-05-FB-27-8E-09-CB-76-67-1B-D1-AC-28-1E-BC */ ;

   >>> turned assertion into assume statement

-Processing command (at Snapshots17.v1.bpl(25,9)) assert false /* checksum: 80-58-47-CB-BE-BA-FC-22-49-6B-79-1F-00-B0-76-C8 */ ;

+Processing command (at Snapshots17.v1.bpl(25,9)) assert false /* checksum: BD-BA-41-4E-2B-2F-D9-9F-50-DD-54-70-B0-DE-5B-39 */ ;

   >>> did nothing

-Processing command (at Snapshots17.v1.bpl(12,13)) assert true /* checksum: 8C-AC-68-E0-D9-25-3C-E2-A1-47-07-CD-ED-9B-B8-8A */ ;

+Processing command (at Snapshots17.v1.bpl(12,13)) assert true /* checksum: 1F-12-2A-83-92-12-7B-F9-9A-F1-94-FC-3D-F5-37-95 */ ;

   >>> did nothing

-Processing command (at Snapshots17.v1.bpl(20,13)) assert x == 1 /* checksum: B4-68-64-D5-1B-10-5F-E3-FA-C7-B8-F7-D1-C5-45-2C */ ;

+Processing command (at Snapshots17.v1.bpl(20,13)) assert x == 1 /* checksum: 67-12-2A-C6-D4-FB-58-80-9D-35-EF-42-01-EF-4A-7B */ ;

   >>> did nothing

 Snapshots17.v1.bpl(20,13): Error BP5001: This assertion might not hold.

 Snapshots17.v1.bpl(25,9): Error BP5001: This assertion might not hold.

@@ -318,12 +318,12 @@ Processing call to procedure N in implementation M (at Snapshots18.v1.bpl(9,9)):
   >>> added after: a##post##0 := a##post##0 && false;

 Processing call to procedure N in implementation M (at Snapshots18.v1.bpl(10,9)):

   >>> added after: a##post##1 := a##post##1 && false;

-Processing command (at Snapshots18.v1.bpl(7,9)) assert 0 == 0 /* checksum: EB-9A-F3-AB-2C-6D-D5-85-C7-CA-03-01-F2-ED-12-D6 */ ;

-  >>> did nothing

-Processing command (at Snapshots18.v1.bpl(17,9)) assert 1 != 1 /* checksum: DA-9B-89-CB-B7-20-E4-60-00-D9-C2-64-D5-7A-B2-39 */ ;

-  >>> did nothing

-Processing command (at Snapshots18.v1.bpl(20,5)) assert 2 != 2 /* checksum: A8-A9-15-48-2F-DC-37-54-4D-12-CB-D8-39-07-DB-E6 */ ;

-  >>> did nothing

+Processing command (at Snapshots18.v1.bpl(7,9)) assert 0 == 0 /* checksum: B1-21-7E-D6-6E-15-08-55-9F-FC-DD-C4-73-7C-FE-66 */ ;

+  >>> turned assertion into assume statement

+Processing command (at Snapshots18.v1.bpl(17,9)) assert 1 != 1 /* checksum: 40-C2-E2-EC-B1-48-97-30-58-1B-D0-87-76-8D-5E-C9 */ ;

+  >>> added assume statement for assertion that has been partially verified under "a##post##0#AT#0 && a##post##1#AT#0"

+Processing command (at Snapshots18.v1.bpl(20,5)) assert 2 != 2 /* checksum: 18-79-6F-32-17-AC-69-D4-4D-E2-27-78-5D-13-E3-C6 */ ;

+  >>> added assume statement for assertion that has been partially verified under "a##post##0#AT#1 && a##post##1#AT#1"

 Snapshots18.v1.bpl(17,9): Error BP5001: This assertion might not hold.

 Snapshots18.v1.bpl(20,5): Error BP5001: This assertion might not hold.

 

@@ -459,3 +459,45 @@ Processing command (at Snapshots24.v1.bpl(24,5)) assert {:subsumption 0} 3 == 3
 Snapshots24.v0.bpl(15,9): Error BP5001: This assertion might not hold.

 

 Boogie program verifier finished with 0 verified, 1 error

+Processing command (at Snapshots25.v0.bpl(12,5)) assert 0 == 0 /* checksum: 8E-3A-E8-C6-21-14-6B-23-57-EB-5C-6D-B1-C9-FF-55 */ ;

+  >>> did nothing

+Processing command (at Snapshots25.v0.bpl(13,5)) assert x != x /* checksum: 70-DF-0F-67-3A-59-39-5B-A3-D6-DA-D2-FA-F6-55-71 */ ;

+  >>> did nothing

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

+

+Boogie program verifier finished with 0 verified, 1 error

+Processing command (at Snapshots25.v1.bpl(12,5)) assert 0 == 0 /* checksum: 8E-3A-E8-C6-21-14-6B-23-57-EB-5C-6D-B1-C9-FF-55 */ ;

+  >>> turned assertion into assume statement

+Processing command (at Snapshots25.v1.bpl(13,5)) assert x != x /* checksum: 70-DF-0F-67-3A-59-39-5B-A3-D6-DA-D2-FA-F6-55-71 */ ;

+  >>> recycled error and turned assertion into assume statement

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

+

+Boogie program verifier finished with 0 verified, 1 error

+Processing command (at Snapshots26.v0.bpl(12,5)) assert 0 == 0 /* checksum: 8E-3A-E8-C6-21-14-6B-23-57-EB-5C-6D-B1-C9-FF-55 */ ;

+  >>> did nothing

+Processing command (at Snapshots26.v0.bpl(13,5)) assert x != x /* checksum: 70-DF-0F-67-3A-59-39-5B-A3-D6-DA-D2-FA-F6-55-71 */ ;

+  >>> did nothing

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

+

+Boogie program verifier finished with 0 verified, 1 error

+Processing command (at Snapshots26.v1.bpl(13,5)) assert 0 == 0 /* checksum: 8E-3A-E8-C6-21-14-6B-23-57-EB-5C-6D-B1-C9-FF-55 */ ;

+  >>> turned assertion into assume statement

+Processing command (at Snapshots26.v1.bpl(14,5)) assert x != x /* checksum: 70-DF-0F-67-3A-59-39-5B-A3-D6-DA-D2-FA-F6-55-71 */ ;

+  >>> recycled error and turned assertion into assume statement

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

+

+Boogie program verifier finished with 0 verified, 1 error

+Processing command (at Snapshots27.v0.bpl(12,5)) assert 0 == 0 /* checksum: 8E-3A-E8-C6-21-14-6B-23-57-EB-5C-6D-B1-C9-FF-55 */ ;

+  >>> did nothing

+Processing command (at Snapshots27.v0.bpl(13,5)) assert x != x /* checksum: 70-DF-0F-67-3A-59-39-5B-A3-D6-DA-D2-FA-F6-55-71 */ ;

+  >>> did nothing

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

+

+Boogie program verifier finished with 0 verified, 1 error

+Processing command (at Snapshots27.v1.bpl(14,5)) assert 0 == 0 /* checksum: 8E-3A-E8-C6-21-14-6B-23-57-EB-5C-6D-B1-C9-FF-55 */ ;

+  >>> turned assertion into assume statement

+Processing command (at Snapshots27.v1.bpl(15,5)) assert x != x /* checksum: 70-DF-0F-67-3A-59-39-5B-A3-D6-DA-D2-FA-F6-55-71 */ ;

+  >>> recycled error and turned assertion into assume statement

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

+

+Boogie program verifier finished with 0 verified, 1 error