public abstract static class ExecutionNodeReader.AbstractKeYlessExecutionNode<S extends SourceElement> extends ExecutionNodeReader.AbstractKeYlessExecutionElement implements IExecutionNode<S>
IExecutionNode
which is independent
from KeY and provides such only children and default attributes.Modifier and Type | Field and Description |
---|---|
private java.util.List<IExecutionNode<?>> |
callStack
The call stack.
|
private java.util.List<IExecutionNode<?>> |
children
The children.
|
private ImmutableList<IExecutionBlockStartNode<?>> |
completedBlocks
The completed blocks.
|
private java.util.List<IExecutionConstraint> |
constraints
The contained constraints.
|
private java.util.Map<IExecutionBlockStartNode<?>,java.lang.String> |
formatedCompletedBlockConditions
The formated conditions under which a block is completed.
|
private java.lang.String |
formatedPathCondition
The formated path condition.
|
private ImmutableList<IExecutionLink> |
incomingLinks
The contained incoming links.
|
private ImmutableList<IExecutionLink> |
outgoingLinks
The contained outgoing links.
|
private IExecutionNode<?> |
parent
The parent
IExecutionNode . |
private boolean |
pathConditionChanged
Is the path condition changed compared to parent?
|
private java.util.List<IExecutionVariable> |
variables
The contained variables.
|
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Constructor and Description |
---|
AbstractKeYlessExecutionNode(IExecutionNode<?> parent,
java.lang.String name,
java.lang.String formatedPathCondition,
boolean pathConditionChanged)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
void |
addCallStackEntry(IExecutionNode<?> entry)
Adds the given entry to the call stack.
|
void |
addChild(IExecutionNode<?> child)
Adds the given child.
|
void |
addCompletedBlock(IExecutionBlockStartNode<?> completedBlock,
java.lang.String formatedCondition)
Adds the given completed block.
|
void |
addConstraint(IExecutionConstraint constraint)
Adds the given
IExecutionConstraint . |
void |
addIncomingLink(IExecutionLink link)
Adds the incoming
IExecutionLink . |
void |
addOutgoingLink(IExecutionLink link)
Adds the outgoing
IExecutionLink . |
void |
addVariable(IExecutionVariable variable)
Adds the given
IExecutionVariable . |
PositionInfo |
getActivePositionInfo()
Returns the
PositionInfo of IExecutionNode.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 configurationIndex)
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 configurationIndex)
Returns the initial memory layout before the method was executed.
|
int |
getLayoutsCount()
Returns the number of memory layouts.
|
ImmutableList<ISymbolicEquivalenceClass> |
getLayoutsEquivalenceClasses(int configurationIndex)
Returns the equivalence classes of the memory layout with the given index.
|
PosInOccurrence |
getModalityPIO()
Returns the
PosInOccurrence of the modality of interest including updates. |
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, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, toString
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getAppliedRuleApp, getElementType, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
private final IExecutionNode<?> parent
IExecutionNode
.private final java.util.List<IExecutionNode<?>> children
private final java.lang.String formatedPathCondition
private final boolean pathConditionChanged
private final java.util.List<IExecutionNode<?>> callStack
private final java.util.List<IExecutionConstraint> constraints
private final java.util.List<IExecutionVariable> variables
private ImmutableList<IExecutionBlockStartNode<?>> completedBlocks
private final java.util.Map<IExecutionBlockStartNode<?>,java.lang.String> formatedCompletedBlockConditions
private ImmutableList<IExecutionLink> outgoingLinks
private ImmutableList<IExecutionLink> incomingLinks
public AbstractKeYlessExecutionNode(IExecutionNode<?> parent, java.lang.String name, java.lang.String formatedPathCondition, boolean pathConditionChanged)
parent
- The parent IExecutionNode
.name
- The name of this node.formatedPathCondition
- The formated path condition.pathConditionChanged
- Is the path condition changed compared to parent?public IExecutionNode<?> getParent()
IExecutionNode
or null
if the
current node is the root.getParent
in interface IExecutionNode<S extends SourceElement>
IExecutionNode
or null
on root.public void addChild(IExecutionNode<?> child)
child
- The child to add.public IExecutionNode<?>[] getChildren()
getChildren
in interface IExecutionNode<S extends SourceElement>
public Term getPathCondition() throws ProofInputException
Term
.getPathCondition
in interface IExecutionNode<S extends SourceElement>
Term
.ProofInputException
public java.lang.String getFormatedPathCondition() throws ProofInputException
getFormatedPathCondition
in interface IExecutionNode<S extends SourceElement>
ProofInputException
public boolean isPathConditionChanged()
isPathConditionChanged
in interface IExecutionNode<S extends SourceElement>
true
has different path condition compared to its parent, false
has same path condition as parent.public void addCallStackEntry(IExecutionNode<?> entry)
entry
- The entry to add to the call stack.public IExecutionNode<?>[] getCallStack()
getCallStack
in interface IExecutionNode<S extends SourceElement>
public void addConstraint(IExecutionConstraint constraint)
IExecutionConstraint
.constraint
- The IExecutionConstraint
to add.public IExecutionConstraint[] getConstraints()
IExecutionConstraint
s.getConstraints
in interface IExecutionNode<S extends SourceElement>
IExecutionConstraint
s.public void addVariable(IExecutionVariable variable)
IExecutionVariable
.variable
- The IExecutionVariable
to add.public S getActiveStatement()
getActiveStatement
in interface IExecutionNode<S extends SourceElement>
public PositionInfo getActivePositionInfo()
PositionInfo
of IExecutionNode.getActiveStatement()
.getActivePositionInfo
in interface IExecutionNode<S extends SourceElement>
PositionInfo
of IExecutionNode.getActiveStatement()
.public IExecutionVariable[] getVariables()
getVariables
in interface IExecutionNode<S extends SourceElement>
public IExecutionVariable[] getVariables(Term condition)
getVariables
in interface IExecutionNode<S extends SourceElement>
condition
- A Term
specifying some additional constraints to consider.public int getLayoutsCount() throws ProofInputException
getLayoutsCount
in interface IExecutionNode<S extends SourceElement>
ProofInputException
- Occurred Exception.public ISymbolicLayout getInitialLayout(int configurationIndex) throws ProofInputException
getInitialLayout
in interface IExecutionNode<S extends SourceElement>
configurationIndex
- The index of the memory layout.ProofInputException
- Occurred Exception.public ISymbolicLayout getCurrentLayout(int configurationIndex) throws ProofInputException
getCurrentLayout
in interface IExecutionNode<S extends SourceElement>
configurationIndex
- The index of the memory layout.ProofInputException
- Occurred Exception.public ImmutableList<ISymbolicEquivalenceClass> getLayoutsEquivalenceClasses(int configurationIndex) throws ProofInputException
getLayoutsEquivalenceClasses
in interface IExecutionNode<S extends SourceElement>
configurationIndex
- The index of the memory layout.ProofInputException
- Occurred Exception.public PosInOccurrence getModalityPIO()
PosInOccurrence
of the modality of interest including updates.getModalityPIO
in interface IExecutionElement
PosInOccurrence
of the modality of interest including updates.public ImmutableList<IExecutionBlockStartNode<?>> getCompletedBlocks()
IExecutionBlockStartNode
.getCompletedBlocks
in interface IExecutionNode<S extends SourceElement>
IExecutionBlockStartNode
.public Term getBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode) throws ProofInputException
IExecutionBlockStartNode
.getBlockCompletionCondition
in interface IExecutionNode<S extends SourceElement>
completedNode
- The completed IExecutionBlockStartNode
for which the condition is requested.IExecutionBlockStartNode
.ProofInputException
public java.lang.String getFormatedBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode) throws ProofInputException
IExecutionBlockStartNode
.getFormatedBlockCompletionCondition
in interface IExecutionNode<S extends SourceElement>
completedNode
- The completed IExecutionBlockStartNode
for which the condition is requested.IExecutionBlockStartNode
.ProofInputException
public void addCompletedBlock(IExecutionBlockStartNode<?> completedBlock, java.lang.String formatedCondition)
completedBlock
- The completed block.formatedCondition
- The formated condition under which the block is completed.public IExecutionLink getOutgoingLink(IExecutionNode<?> target)
IExecutionLink
.getOutgoingLink
in interface IExecutionNode<S extends SourceElement>
target
- The target IExecutionNode
.IExecutionLink
or null
if such a link is not available.public void addOutgoingLink(IExecutionLink link)
IExecutionLink
.link
- The outgoing IExecutionLink
to add.public ImmutableList<IExecutionLink> getOutgoingLinks()
getOutgoingLinks
in interface IExecutionNode<S extends SourceElement>
public void addIncomingLink(IExecutionLink link)
IExecutionLink
.link
- The incoming IExecutionLink
to add.public IExecutionLink getIncomingLink(IExecutionNode<?> source)
IExecutionLink
.getIncomingLink
in interface IExecutionNode<S extends SourceElement>
source
- The source IExecutionNode
.IExecutionLink
or null
if such a link is not available.public ImmutableList<IExecutionLink> getIncomingLinks()
getIncomingLinks
in interface IExecutionNode<S extends SourceElement>