diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Core/Absy.cs | 4 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 25 |
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;
|