Package | Description |
---|---|
de.uka.ilkd.key.symbolic_execution | |
de.uka.ilkd.key.symbolic_execution.model.impl |
Modifier and Type | Method and Description |
---|---|
protected AbstractExecutionNode<?> |
SymbolicExecutionTreeBuilder.addNodeToTreeAndUpdateParent(Node node,
AbstractExecutionNode<?> parentToAddTo,
AbstractExecutionNode<?> executionNode)
Adds the new created
AbstractExecutionNode to the symbolic execution tree
if available and returns the new parent for future detected nodes. |
protected AbstractExecutionNode<?> |
SymbolicExecutionTreeBuilder.analyzeNode(Node node,
AbstractExecutionNode<?> parentToAddTo,
SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions completions)
Analyzes the given
Proof and his contained proof tree by
filling the start node SymbolicExecutionTreeBuilder.getStartNode()
with IExecutionNode s which are instantiated if a Node
in KeY's proof tree applies a rule of symbolic execution. |
protected AbstractExecutionNode<?> |
SymbolicExecutionTreeBuilder.createExecutionTreeModelRepresentation(AbstractExecutionNode<?> parent,
Node node,
SourceElement statement)
Creates a new execution tree model representation (
IExecutionNode )
if possible for the given Node in KeY's proof tree. |
Modifier and Type | Method and Description |
---|---|
java.util.Set<AbstractExecutionNode<?>> |
SymbolicExecutionTreeBuilder.prune(Node node)
Prunes the symbolic execution tree at the first
IExecutionNode in the parent hierarchy of the given
Node (including the Node itself). |
Modifier and Type | Method and Description |
---|---|
protected void |
SymbolicExecutionTreeBuilder.addChild(AbstractExecutionNode<?> parent,
AbstractExecutionNode<?> child)
Adds the child to the parent.
|
protected void |
SymbolicExecutionTreeBuilder.addChild(AbstractExecutionNode<?> parent,
AbstractExecutionNode<?> child)
Adds the child to the parent.
|
protected AbstractExecutionNode<?> |
SymbolicExecutionTreeBuilder.addNodeToTreeAndUpdateParent(Node node,
AbstractExecutionNode<?> parentToAddTo,
AbstractExecutionNode<?> executionNode)
Adds the new created
AbstractExecutionNode to the symbolic execution tree
if available and returns the new parent for future detected nodes. |
protected AbstractExecutionNode<?> |
SymbolicExecutionTreeBuilder.addNodeToTreeAndUpdateParent(Node node,
AbstractExecutionNode<?> parentToAddTo,
AbstractExecutionNode<?> executionNode)
Adds the new created
AbstractExecutionNode to the symbolic execution tree
if available and returns the new parent for future detected nodes. |
protected AbstractExecutionNode<?> |
SymbolicExecutionTreeBuilder.analyzeNode(Node node,
AbstractExecutionNode<?> parentToAddTo,
SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions completions)
Analyzes the given
Proof and his contained proof tree by
filling the start node SymbolicExecutionTreeBuilder.getStartNode()
with IExecutionNode s which are instantiated if a Node
in KeY's proof tree applies a rule of symbolic execution. |
protected AbstractExecutionNode<?> |
SymbolicExecutionTreeBuilder.createExecutionTreeModelRepresentation(AbstractExecutionNode<?> parent,
Node node,
SourceElement statement)
Creates a new execution tree model representation (
IExecutionNode )
if possible for the given Node in KeY's proof tree. |
protected AbstractExecutionMethodReturn<?> |
SymbolicExecutionTreeBuilder.createMehtodReturn(AbstractExecutionNode<?> parent,
Node node,
SourceElement statement,
SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions completions)
Creates an method return node.
|
Modifier and Type | Method and Description |
---|---|
AbstractExecutionNode<?>[] |
AbstractExecutionNode.getChildren()
Returns the available children.
|
AbstractExecutionNode<?> |
AbstractExecutionNode.getParent()
Returns the parent
IExecutionNode or null if the
current node is the root. |
Modifier and Type | Method and Description |
---|---|
void |
AbstractExecutionNode.addChild(AbstractExecutionNode<?> child)
Adds a new child
AbstractExecutionNode . |
void |
AbstractExecutionNode.setParent(AbstractExecutionNode<?> parent)
Sets the parent
AbstractExecutionNode . |
Copyright © 2003-2019 The KeY-Project.