Worked on improving program snapshot verification.

2 files changed, 24 insertions, 5 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;