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

18 files changed, 79 insertions, 34 deletions

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index e3d3d109..7ccdaa19 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -45,6 +45,14 @@ namespace Microsoft.Boogie
     {

       dependencies.Add(node);

 

+      foreach (var param in node.InParams)

+      {

+        if (param.TypedIdent != null && param.TypedIdent.WhereExpr != null)

+        {

+          param.TypedIdent.WhereExpr = VisitExpr(param.TypedIdent.WhereExpr);

+        }

+      }

+

       return base.VisitProcedure(node);

     }

 

@@ -52,41 +60,38 @@ namespace Microsoft.Boogie
     {

       dependencies.Add(node);

 

+      if (node.DefinitionAxiom != null)

+      {

+        node.DefinitionAxiom = VisitAxiom(node.DefinitionAxiom);

+      }

+

       return base.VisitFunction(node);

     }

 

     public override Cmd VisitCallCmd(CallCmd node)

     {

-      var result = base.VisitCallCmd(node);

-

       var visited = dependencies.Contains(node.Proc);

       if (!visited)

       {

-        VisitProcedure(node.Proc);

+        node.Proc = VisitProcedure(node.Proc);

       }

 

-      return result;

+      return base.VisitCallCmd(node);

     }

 

     public override Expr VisitNAryExpr(NAryExpr node)

     {

-      var result = base.VisitNAryExpr(node);

-

       var funCall = node.Fun as FunctionCall;

       if (funCall != null)

       {

         var visited = dependencies.Contains(funCall.Func);

         if (!visited)

         {

-          VisitFunction(funCall.Func);

-          if (funCall.Func.DefinitionAxiom != null)

-          {

-            VisitAxiom(funCall.Func.DefinitionAxiom);

-          }

+          funCall.Func = VisitFunction(funCall.Func);

         }

       }

 

-      return result;

+      return base.VisitNAryExpr(node);

     }

   }

 

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