From 30de798ff34bbb34ee474ee510aba08c43e9ac7c Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Sun, 23 Nov 2014 19:36:53 +0100
Subject: Worked on the verification result caching.

---
 Source/Core/Absy.cs                               | 20 ++++++++++++++
 Source/ExecutionEngine/VerificationResultCache.cs | 32 +++++++++++++++++++++--
 2 files changed, 50 insertions(+), 2 deletions(-)

(limited to 'Source')

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index a53165b6..9d446ebd 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -1455,6 +1455,26 @@ namespace Microsoft.Boogie {
       this.Attributes = kv;
     }
 
+    public bool DependenciesCollected { get; set; }
+
+    ISet<Function> functionDependencies;
+
+    public ISet<Function> FunctionDependencies
+    {
+      get { return functionDependencies; }
+    }
+
+    public void AddFunctionDependency(Function function)
+    {
+      Contract.Requires(function != null);
+
+      if (functionDependencies == null)
+      {
+        functionDependencies = new HashSet<Function>();
+      }
+      functionDependencies.Add(function);
+    }
+
     public override void Emit(TokenTextWriter stream, int level) {
       //Contract.Requires(stream != null);
       if (Comment != null) {
diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index e25c9306..bacdfaf8 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -324,6 +324,7 @@ namespace Microsoft.Boogie
   sealed class DependencyCollector : ReadOnlyVisitor
   {
     private DeclWithFormals currentDeclaration;
+    private Axiom currentAxiom;
 
     public static void Collect(Program program)
     {
@@ -389,6 +390,26 @@ namespace Microsoft.Boogie
       return result;
     }
 
+    public override Axiom VisitAxiom(Axiom node)
+    {
+      if (node.DependenciesCollected)
+      {
+        if (currentDeclaration != null && node.FunctionDependencies != null)
+        {
+          foreach (var f in node.FunctionDependencies)
+          {
+            currentDeclaration.AddFunctionDependency(f);
+          }
+        }
+        return node;
+      }
+      currentAxiom = node;
+      var result = base.VisitAxiom(node);
+      node.DependenciesCollected = true;
+      currentAxiom = null;
+      return result;
+    }
+
     public override Function VisitFunction(Function node)
     {
       currentDeclaration = node;
@@ -427,9 +448,16 @@ namespace Microsoft.Boogie
     public override Expr VisitNAryExpr(NAryExpr node)
     {
       var funCall = node.Fun as FunctionCall;
-      if (funCall != null && currentDeclaration != null)
+      if (funCall != null)
       {
-        currentDeclaration.AddFunctionDependency(funCall.Func);
+        if (currentDeclaration != null)
+        {
+          currentDeclaration.AddFunctionDependency(funCall.Func);
+        }
+        if (currentAxiom != null)
+        {
+          currentAxiom.AddFunctionDependency(funCall.Func);
+        }
       }
 
       return base.VisitNAryExpr(node);
-- 
cgit v1.2.3