diff options
| author |  wuestholz <unknown> | 2014-11-23 19:36:53 +0100 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-11-23 19:36:53 +0100 |
| commit | 30de798ff34bbb34ee474ee510aba08c43e9ac7c (patch) | |
| tree | f839eeaa83d596d869228c1a80dad0d43e5593ab /Source | |
| parent | 8849f5af53d27be7eded969c68bf391b3f8028c0 (diff) | |
Worked on the verification result caching.
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Core/Absy.cs | 20 | ||||
| -rw-r--r-- | Source/ExecutionEngine/VerificationResultCache.cs | 32 |
2 files changed, 50 insertions, 2 deletions
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);
|