de.uka.ilkd.key.symbolic_execution

Class SymbolicExecutionTreeBuilder.AnalyzerProofVisitor

java.lang.Object

de.uka.ilkd.key.symbolic_execution.SymbolicExecutionTreeBuilder.AnalyzerProofVisitor

All Implemented Interfaces:

ProofVisitor

Enclosing class:

SymbolicExecutionTreeBuilder

private class SymbolicExecutionTreeBuilder.AnalyzerProofVisitor
extends java.lang.Object
implements ProofVisitor

This ProofVisitor is used to transfer the proof tree in KeY into IExecutionNodes which forms the symbolic execution tree.

Author:

Martin Hentschel

Field Summary

Fields

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 Nodes children should be added to.
private SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions	completions The SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions to update.
private ImmutableList<Node>	joinNodes Contains all Nodes 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 Summary

Constructors

Constructor and Description
AnalyzerProofVisitor(SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions completions) Constructor.

Method Summary

Modifier and Type	Method and Description
void	completeTree() Completes the execution tree model after all Nodes were visited in visit(Proof, Node).
protected void	finishBlockCompletion(IExecutionBranchCondition node)
void	injectLinks() Instantiates all missing IExecutionLinks and injects them into the symbolic execution tree.
void	visit(Proof proof, Node visitedNode)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

completions

private final SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions completions

The SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions to update.

addToMapping

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 Nodes children should be added to.

parentToBranchConditionMapping

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.

joinNodes

private ImmutableList<Node> joinNodes

Contains all Nodes which are closed after a join.

Constructor Detail

AnalyzerProofVisitor

public AnalyzerProofVisitor(SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions completions)

Constructor.

Parameters:

completions - The SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions to update.

Method Detail

visit

public void visit(Proof proof,
                  Node visitedNode)

Specified by:

visit in interface ProofVisitor

injectLinks

public void injectLinks()

Instantiates all missing IExecutionLinks and injects them into the symbolic execution tree.

completeTree

public void completeTree()

Completes the execution tree model after all Nodes 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.

finishBlockCompletion

protected void finishBlockCompletion(IExecutionBranchCondition node)