Added more tests for the verification result caching.

5 files changed, 74 insertions, 29 deletions

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index e042402f..091ccc25 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -204,6 +204,8 @@ namespace Microsoft.Boogie
         var canUseSpecs = DependencyCollector.AllFunctionDependenciesAreDefinedAndUnchanged(oldProc, Program);

         if (canUseSpecs)

         {

+          var desugaring = node.Desugaring;

+          Contract.Assert(desugaring != null);

           var precond = node.CheckedPrecondition(oldProc, Program);

           if (precond != null)

           {

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

+

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

+{

+    var x: int;

+

+    assume x == 0;

+

+    while (*)

+    {

+    }

+

+    assert 0 == 0;

+    assert x == 0;

+}

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

+

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

+{

+    var x: int;

+

+    assume x == 0;

+

+    while (*)

+    {

+        x := 1;

+    }

+

+    assert 0 == 0;

+    assert x == 0;  // TODO(wuestholz): This should fail.

+}

diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot
index 2924b15a..484fa8e2 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 Snapshots25.bpl Snapshots26.bpl Snapshots27.bpl > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately -noinfer 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 Snapshots28.bpl > "%t"

+// RUN: %diff "%s.expect" "%t"

diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index bc847ebe..3b47d2f3 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -280,11 +280,11 @@ Snapshots16.v1.bpl(14,5): Error BP5001: This assertion might not hold.
 Boogie program verifier finished with 0 verified, 1 error

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

   >>> did nothing

-Processing command (at Snapshots17.v0.bpl(25,9)) assert false /* checksum: 3A-F2-06-60-5D-63-00-9C-7B-76-0A-81-C9-40-A4-8F */ ;

+Processing command (at Snapshots17.v0.bpl(25,9)) assert false /* checksum: EC-EF-B7-8D-C2-CE-CF-21-05-72-63-D5-B0-54-C2-52 */ ;

   >>> did nothing

-Processing command (at Snapshots17.v0.bpl(12,13)) assert true /* checksum: B6-DA-0F-69-58-5E-00-18-D7-B8-16-13-5A-2B-AA-EF */ ;

+Processing command (at Snapshots17.v0.bpl(12,13)) assert true /* checksum: A0-25-98-E6-65-11-A1-47-ED-3C-DD-47-3D-BF-CC-50 */ ;

   >>> did nothing

-Processing command (at Snapshots17.v0.bpl(20,13)) assert x == 1 /* checksum: 8E-DA-C3-A4-92-2F-9B-29-8C-B4-61-B1-66-35-D7-99 */ ;

+Processing command (at Snapshots17.v0.bpl(20,13)) assert x == 1 /* checksum: 48-21-D4-6B-67-A4-0A-BE-B6-30-6E-E5-01-A9-31-E6 */ ;

   >>> did nothing

 

 Boogie program verifier finished with 1 verified, 0 errors

@@ -296,21 +296,21 @@ 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: 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: 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: 67-12-2A-C6-D4-FB-58-80-9D-35-EF-42-01-EF-4A-7B */ ;

-  >>> did nothing

+Processing command (at Snapshots17.v1.bpl(25,9)) assert false /* checksum: EC-EF-B7-8D-C2-CE-CF-21-05-72-63-D5-B0-54-C2-52 */ ;

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

+Processing command (at Snapshots17.v1.bpl(12,13)) assert true /* checksum: A0-25-98-E6-65-11-A1-47-ED-3C-DD-47-3D-BF-CC-50 */ ;

+  >>> turned assertion into assume statement

+Processing command (at Snapshots17.v1.bpl(20,13)) assert x == 1 /* checksum: 48-21-D4-6B-67-A4-0A-BE-B6-30-6E-E5-01-A9-31-E6 */ ;

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

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

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

 

 Boogie program verifier finished with 0 verified, 2 errors

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

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

+Processing command (at Snapshots18.v0.bpl(17,9)) assert 1 != 1 /* checksum: 9D-3B-BC-FC-10-33-1E-0A-90-26-FB-08-74-DE-3D-D8 */ ;

   >>> did nothing

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

+Processing command (at Snapshots18.v0.bpl(20,5)) assert 2 != 2 /* checksum: 40-A9-8B-52-39-8E-77-50-4D-48-DF-80-1D-47-41-84 */ ;

   >>> did nothing

 

 Boogie program verifier finished with 1 verified, 0 errors

@@ -318,11 +318,11 @@ 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: B1-21-7E-D6-6E-15-08-55-9F-FC-DD-C4-73-7C-FE-66 */ ;

+Processing command (at Snapshots18.v1.bpl(7,9)) 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 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 */ ;

+Processing command (at Snapshots18.v1.bpl(17,9)) assert 1 != 1 /* checksum: 9D-3B-BC-FC-10-33-1E-0A-90-26-FB-08-74-DE-3D-D8 */ ;

   >>> 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 */ ;

+Processing command (at Snapshots18.v1.bpl(20,5)) assert 2 != 2 /* checksum: 40-A9-8B-52-39-8E-77-50-4D-48-DF-80-1D-47-41-84 */ ;

   >>> 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,45 +459,57 @@ 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 */ ;

+Processing command (at Snapshots25.v0.bpl(12,5)) assert 0 == 0 /* checksum: 53-43-22-D6-88-33-A6-55-1F-1E-BB-26-33-C2-18-44 */ ;

   >>> 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 */ ;

+Processing command (at Snapshots25.v0.bpl(13,5)) assert x != x /* checksum: 4F-C4-09-77-BD-18-D6-2D-EB-01-5B-7B-B8-DF-5C-06 */ ;

   >>> 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 */ ;

+Processing command (at Snapshots25.v1.bpl(12,5)) assert 0 == 0 /* checksum: 53-43-22-D6-88-33-A6-55-1F-1E-BB-26-33-C2-18-44 */ ;

   >>> 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 */ ;

+Processing command (at Snapshots25.v1.bpl(13,5)) assert x != x /* checksum: 4F-C4-09-77-BD-18-D6-2D-EB-01-5B-7B-B8-DF-5C-06 */ ;

   >>> 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 */ ;

+Processing command (at Snapshots26.v0.bpl(12,5)) assert 0 == 0 /* checksum: 53-43-22-D6-88-33-A6-55-1F-1E-BB-26-33-C2-18-44 */ ;

   >>> 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 */ ;

+Processing command (at Snapshots26.v0.bpl(13,5)) assert x != x /* checksum: 4F-C4-09-77-BD-18-D6-2D-EB-01-5B-7B-B8-DF-5C-06 */ ;

   >>> 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 */ ;

+Processing command (at Snapshots26.v1.bpl(13,5)) assert 0 == 0 /* checksum: 53-43-22-D6-88-33-A6-55-1F-1E-BB-26-33-C2-18-44 */ ;

   >>> 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 */ ;

+Processing command (at Snapshots26.v1.bpl(14,5)) assert x != x /* checksum: 4F-C4-09-77-BD-18-D6-2D-EB-01-5B-7B-B8-DF-5C-06 */ ;

   >>> 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 */ ;

+Processing command (at Snapshots27.v0.bpl(12,5)) assert 0 == 0 /* checksum: 53-43-22-D6-88-33-A6-55-1F-1E-BB-26-33-C2-18-44 */ ;

   >>> 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 */ ;

+Processing command (at Snapshots27.v0.bpl(13,5)) assert x != x /* checksum: 4F-C4-09-77-BD-18-D6-2D-EB-01-5B-7B-B8-DF-5C-06 */ ;

   >>> 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 */ ;

+Processing command (at Snapshots27.v1.bpl(14,5)) assert 0 == 0 /* checksum: 53-43-22-D6-88-33-A6-55-1F-1E-BB-26-33-C2-18-44 */ ;

   >>> 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 */ ;

+Processing command (at Snapshots27.v1.bpl(15,5)) assert x != x /* checksum: 4F-C4-09-77-BD-18-D6-2D-EB-01-5B-7B-B8-DF-5C-06 */ ;

   >>> 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

+Processing command (at Snapshots28.v0.bpl(13,5)) assert 0 == 0 /* checksum: AB-78-39-B7-C9-1E-4B-24-B5-1A-52-BE-B2-1A-90-D9 */ ;

+  >>> did nothing

+Processing command (at Snapshots28.v0.bpl(14,5)) assert x == 0 /* checksum: 01-A7-D9-2B-A8-C4-4F-BB-44-22-BE-B6-E1-5F-6E-BF */ ;

+  >>> did nothing

+

+Boogie program verifier finished with 1 verified, 0 errors

+Processing command (at Snapshots28.v1.bpl(14,5)) assert 0 == 0 /* checksum: AB-78-39-B7-C9-1E-4B-24-B5-1A-52-BE-B2-1A-90-D9 */ ;

+  >>> turned assertion into assume statement

+Processing command (at Snapshots28.v1.bpl(15,5)) assert x == 0 /* checksum: 01-A7-D9-2B-A8-C4-4F-BB-44-22-BE-B6-E1-5F-6E-BF */ ;

+  >>> turned assertion into assume statement

+

+Boogie program verifier finished with 1 verified, 0 errors