private class SymbolicExecutionTreeBuilder.AnalyzerProofVisitor extends java.lang.Object implements ProofVisitor
ProofVisitor
is used to transfer the proof tree in KeY
into IExecutionNode
s which forms the symbolic execution tree.Modifier and Type | Field and Description |
---|---|
private java.util.Map<Node,AbstractExecutionNode<?>> |
addToMapping
Maps the
Node in KeY's proof tree to the IExecutionNode of the symbolic execution tree where the Node s children should be added to. |
private SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions |
completions
The
SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions to update. |
private ImmutableList<Node> |
joinNodes
Contains all
Node s which are closed after a join. |
private java.util.Map<AbstractExecutionNode<?>,java.util.List<ExecutionBranchCondition>> |
parentToBranchConditionMapping
This utility
Map helps to find a List in SymbolicExecutionTreeBuilder.branchConditionsStack
for the given parent node to that elements in the List should be added. |
Constructor and Description |
---|
AnalyzerProofVisitor(SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions completions)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
void |
completeTree()
Completes the execution tree model after all
Node s were visited
in visit(Proof, Node) . |
protected void |
finishBlockCompletion(IExecutionBranchCondition node) |
void |
injectLinks()
Instantiates all missing
IExecutionLink s and injects them into the symbolic execution tree. |
void |
visit(Proof proof,
Node visitedNode) |
private final SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions completions
SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions
to update.private java.util.Map<Node,AbstractExecutionNode<?>> addToMapping
Node
in KeY's proof tree to the IExecutionNode
of the symbolic execution tree where the Node
s children should be added to.private java.util.Map<AbstractExecutionNode<?>,java.util.List<ExecutionBranchCondition>> parentToBranchConditionMapping
Map
helps to find a List
in SymbolicExecutionTreeBuilder.branchConditionsStack
for the given parent node to that elements in the List
should be added.private ImmutableList<Node> joinNodes
Node
s which are closed after a join.public AnalyzerProofVisitor(SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions completions)
completions
- The SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions
to update.public void visit(Proof proof, Node visitedNode)
visit
in interface ProofVisitor
public void injectLinks()
IExecutionLink
s and injects them into the symbolic execution tree.public void completeTree()
Completes the execution tree model after all Node
s were visited
in visit(Proof, Node)
. The task of this method is to add
ExecutionBranchCondition
to the model if they have at least one child.
Fore more details have a look at the documentation of SymbolicExecutionTreeBuilder.branchConditionsStack
.
protected void finishBlockCompletion(IExecutionBranchCondition node)