Worked on improving program snapshot verification.

6 files changed, 79 insertions, 19 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index fd62f334..021897f0 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -1953,6 +1953,7 @@ namespace Microsoft.Boogie {
 

     // the body is only set if the function is declared with {:inline}

     public Expr Body;

+    public Axiom DefinitionAxiom;

     public bool doingExpansion;

 

     private bool neverTrigger;

@@ -2123,7 +2124,8 @@ namespace Microsoft.Boogie {
                              new Trigger(tok, true, new ExprSeq(call), null),

                              def);

       }

-      return new Axiom(tok, def);

+      DefinitionAxiom = new Axiom(tok, def);

+      return DefinitionAxiom;

     }

   }

 

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 25854ec5..f4c25796 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -1111,18 +1111,27 @@ namespace Microsoft.Boogie
 

       public override Procedure VisitProcedure(Procedure node)

       {

-        var result = base.VisitProcedure(node);

+        dependencies.Add(node);

+

+        return base.VisitProcedure(node);

+      }

 

+      public override Function VisitFunction(Function node)

+      {

         dependencies.Add(node);

 

-        return result;

+        return base.VisitFunction(node);

       }

 

       public override Cmd VisitCallCmd(CallCmd node)

       {

         var result = base.VisitCallCmd(node);

 

-        dependencies.Add(node.Proc);

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

+        if (!visited)

+        {

+          VisitProcedure(node.Proc);

+        }

 

         return result;

       }

@@ -1134,7 +1143,15 @@ namespace Microsoft.Boogie
         var funCall = node.Fun as FunctionCall;

         if (funCall != null)

         {

-          dependencies.Add(funCall.Func);

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

+          if (!visited)

+          {

+            VisitFunction(funCall.Func);

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

+            {

+              VisitAxiom(funCall.Func.DefinitionAxiom);

+            }

+          }

         }

 

         return result;

diff --git a/Test/snapshots/Answer b/Test/snapshots/Answer
index a7a6b0be..676f0323 100644
--- a/Test/snapshots/Answer
+++ b/Test/snapshots/Answer
@@ -1,4 +1,5 @@
--------------------- Snapshots0.bpl --------------------

+

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

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

 Execution trace:

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

@@ -27,7 +28,7 @@ Execution trace:
 

 Boogie program verifier finished with 2 verified, 1 error

 

--------------------- Snapshots1.bpl --------------------

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

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

 Execution trace:

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

@@ -45,7 +46,9 @@ Execution trace:
 

 Boogie program verifier finished with 1 verified, 1 error

 

--------------------- Snapshots2.bpl --------------------

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

+

+Boogie program verifier finished with 1 verified, 0 errors

 

 Boogie program verifier finished with 1 verified, 0 errors

 

@@ -57,4 +60,12 @@ 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/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/runtest.bat b/Test/snapshots/runtest.bat
index fa45d56a..663cef07 100644
--- a/Test/snapshots/runtest.bat
+++ b/Test/snapshots/runtest.bat
@@ -1,17 +1,11 @@
-

 @echo off

 setlocal

 

 set BOOGIEDIR=..\..\Binaries

 set BGEXE=%BOOGIEDIR%\Boogie.exe

 

-echo -------------------- Snapshots0.bpl --------------------

-%BGEXE% %* /verifySnapshots Snapshots0.bpl

-

-echo.

-echo -------------------- Snapshots1.bpl --------------------

-%BGEXE% %* /verifySnapshots Snapshots1.bpl

-

-echo.

-echo -------------------- Snapshots2.bpl --------------------

-%BGEXE% %* /verifySnapshots Snapshots2.bpl

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

+  echo.

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

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

+)