public interface IExecutionNode<S extends SourceElement> extends IExecutionElement
Provides the basic methods each node in a symbolic execution tree
should have and allows to access the children. A symbolic execution tree
always starts with an IExecutionStart
and is created via
a SymbolicExecutionTreeBuilder
instance.
The following concrete nodes are available
IExecutionStart
(root node)IExecutionStatement
(single statement, e.g. int x = 1 + 2;
)IExecutionBranchStatement
(branch statement, e.g. if(x >= 0)
)IExecutionBranchCondition
(branch condition, e.g. x < 0
)IExecutionMethodCall
(method call, e.g. foo()
)IExecutionMethodReturn
(method return, e.g. return 42
)IExecutionTermination
(termination, e.g. <end>
or <uncaught java.lang.NullPointerException>
)Modifier and Type | Field and Description |
---|---|
static java.lang.String |
INTERNAL_NODE_NAME_END
Suffix that is used in
IExecutionNode s which represents an internal state in KeY which is not part of the source code. |
static java.lang.String |
INTERNAL_NODE_NAME_START
Prefix that is used in
IExecutionNode s which represents an internal state in KeY which is not part of the source code. |
Modifier and Type | Method and Description |
---|---|
PositionInfo |
getActivePositionInfo()
Returns the
PositionInfo of getActiveStatement() . |
S |
getActiveStatement()
Returns the active statement which is executed in the code.
|
Term |
getBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode)
Returns the condition under which this node completes the code block of the given
IExecutionBlockStartNode . |
IExecutionNode<?>[] |
getCallStack()
Returns the method call stack.
|
IExecutionNode<?>[] |
getChildren()
Returns the available children.
|
ImmutableList<IExecutionBlockStartNode<?>> |
getCompletedBlocks()
Returns all code blocks completed by this
IExecutionBlockStartNode . |
IExecutionConstraint[] |
getConstraints()
Returns all available
IExecutionConstraint s. |
ISymbolicLayout |
getCurrentLayout(int layoutIndex)
Returns the current memory layout which shows the memory
structure before the current node in the symbolic execution tree is executed.
|
java.lang.String |
getFormatedBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode)
Returns the human readable condition under which this node completes the code block of the given
IExecutionBlockStartNode . |
java.lang.String |
getFormatedPathCondition()
Returns the human readable path condition to reach this node as string.
|
IExecutionLink |
getIncomingLink(IExecutionNode<?> source)
Returns the incoming
IExecutionLink . |
ImmutableList<IExecutionLink> |
getIncomingLinks()
Returns all available incoming links.
|
ISymbolicLayout |
getInitialLayout(int layoutIndex)
Returns the initial memory layout before the method was executed.
|
int |
getLayoutsCount()
Returns the number of memory layouts.
|
ImmutableList<ISymbolicEquivalenceClass> |
getLayoutsEquivalenceClasses(int layoutIndex)
Returns the equivalence classes of the memory layout with the given index.
|
IExecutionLink |
getOutgoingLink(IExecutionNode<?> target)
Returns the outgoing
IExecutionLink . |
ImmutableList<IExecutionLink> |
getOutgoingLinks()
Returns all available outgoing links.
|
IExecutionNode<?> |
getParent()
Returns the parent
IExecutionNode or null if the
current node is the root. |
Term |
getPathCondition()
Returns the path condition to reach this node as
Term . |
IExecutionVariable[] |
getVariables()
Returns the variable value pairs of the current state.
|
IExecutionVariable[] |
getVariables(Term condition)
Returns the variable value pairs of the current state under the given condition.
|
boolean |
isPathConditionChanged()
Checks if this node has changed the path condition of the parent.
|
getAppliedRuleApp, getElementType, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
static final java.lang.String INTERNAL_NODE_NAME_START
IExecutionNode
s which represents an internal state in KeY which is not part of the source code.static final java.lang.String INTERNAL_NODE_NAME_END
IExecutionNode
s which represents an internal state in KeY which is not part of the source code.IExecutionNode<?> getParent()
IExecutionNode
or null
if the
current node is the root.IExecutionNode
or null
on root.IExecutionNode<?>[] getChildren()
boolean isPathConditionChanged()
true
has different path condition compared to its parent, false
has same path condition as parent.Term getPathCondition() throws ProofInputException
Term
.Term
.ProofInputException
java.lang.String getFormatedPathCondition() throws ProofInputException
ProofInputException
IExecutionNode<?>[] getCallStack()
IExecutionConstraint[] getConstraints()
IExecutionConstraint
s.IExecutionConstraint
s.S getActiveStatement()
PositionInfo getActivePositionInfo()
PositionInfo
of getActiveStatement()
.PositionInfo
of getActiveStatement()
.IExecutionVariable[] getVariables() throws ProofInputException
ProofInputException
- Occurred Exception.IExecutionVariable[] getVariables(Term condition) throws ProofInputException
condition
- A Term
specifying some additional constraints to consider.ProofInputException
int getLayoutsCount() throws ProofInputException
ProofInputException
- Occurred Exception.ImmutableList<ISymbolicEquivalenceClass> getLayoutsEquivalenceClasses(int layoutIndex) throws ProofInputException
layoutIndex
- The index of the memory layout.ProofInputException
- Occurred Exception.ISymbolicLayout getInitialLayout(int layoutIndex) throws ProofInputException
layoutIndex
- The index of the memory layout.ProofInputException
- Occurred Exception.ISymbolicLayout getCurrentLayout(int layoutIndex) throws ProofInputException
layoutIndex
- The index of the memory layout.ProofInputException
- Occurred Exception.ImmutableList<IExecutionBlockStartNode<?>> getCompletedBlocks()
IExecutionBlockStartNode
.IExecutionBlockStartNode
.Term getBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode) throws ProofInputException
IExecutionBlockStartNode
.completedNode
- The completed IExecutionBlockStartNode
for which the condition is requested.IExecutionBlockStartNode
.ProofInputException
java.lang.String getFormatedBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode) throws ProofInputException
IExecutionBlockStartNode
.completedNode
- The completed IExecutionBlockStartNode
for which the condition is requested.IExecutionBlockStartNode
.ProofInputException
IExecutionLink getOutgoingLink(IExecutionNode<?> target)
IExecutionLink
.target
- The target IExecutionNode
.IExecutionLink
or null
if such a link is not available.ImmutableList<IExecutionLink> getOutgoingLinks()
IExecutionLink getIncomingLink(IExecutionNode<?> source)
IExecutionLink
.source
- The source IExecutionNode
.IExecutionLink
or null
if such a link is not available.ImmutableList<IExecutionLink> getIncomingLinks()