public abstract static class ExecutionNodeReader.AbstractKeYlessBaseExecutionNode<S extends SourceElement> extends ExecutionNodeReader.AbstractKeYlessExecutionNode<S> implements IExecutionBaseMethodReturn<S>
IExecutionBaseMethodReturn
which is independent
from KeY and provides such only children and default attributes.Modifier and Type | Field and Description |
---|---|
private java.util.List<IExecutionVariable> |
callStateVariables
The contained call state variables.
|
private java.lang.String |
formatedMethodReturn
The formated method return condition.
|
private java.lang.String |
signature
The signature.
|
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Constructor and Description |
---|
AbstractKeYlessBaseExecutionNode(IExecutionNode<?> parent,
java.lang.String name,
java.lang.String formatedPathCondition,
boolean pathConditionChanged,
java.lang.String signature,
java.lang.String formatedMethodReturn)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
void |
addCallStateVariable(IExecutionVariable variable)
Adds the given
IExecutionVariable . |
IExecutionVariable[] |
getCallStateVariables()
Returns the variable value pairs of the state when the method has been called.
|
java.lang.String |
getFormatedMethodReturnCondition()
Returns the human readable condition under which this method return is reached from
the calling
IExecutionMethodCall . |
IExecutionMethodCall |
getMethodCall()
A reference to the
IExecutionMethodCall which is now returned. |
Term |
getMethodReturnCondition()
Returns the condition under which this method return is reached from
the calling
IExecutionMethodCall . |
java.lang.String |
getSignature()
Returns a human readable signature which describes this element.
|
addCallStackEntry, addChild, addCompletedBlock, addConstraint, addIncomingLink, addOutgoingLink, addVariable, getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getModalityPIO, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged
getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, toString
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged
getAppliedRuleApp, getElementType, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
private final java.util.List<IExecutionVariable> callStateVariables
private final java.lang.String signature
private final java.lang.String formatedMethodReturn
public AbstractKeYlessBaseExecutionNode(IExecutionNode<?> parent, java.lang.String name, java.lang.String formatedPathCondition, boolean pathConditionChanged, java.lang.String signature, java.lang.String formatedMethodReturn)
parent
- The parent IExecutionNode
.name
- The name of this node.formatedPathCondition
- The formated path condition.pathConditionChanged
- Is the path condition changed compared to parent?signature
- The signature.formatedMethodReturn
- The formated method return condition.public IExecutionVariable[] getCallStateVariables()
getCallStateVariables
in interface IExecutionBaseMethodReturn<S extends SourceElement>
public void addCallStateVariable(IExecutionVariable variable)
IExecutionVariable
.variable
- The IExecutionVariable
to add.public IExecutionMethodCall getMethodCall()
IExecutionMethodCall
which is now returned.getMethodCall
in interface IExecutionBaseMethodReturn<S extends SourceElement>
public java.lang.String getSignature() throws ProofInputException
getSignature
in interface IExecutionBaseMethodReturn<S extends SourceElement>
ProofInputException
- Occurred Exception.public Term getMethodReturnCondition() throws ProofInputException
IExecutionMethodCall
.getMethodReturnCondition
in interface IExecutionBaseMethodReturn<S extends SourceElement>
IExecutionMethodCall
as Term
.ProofInputException
public java.lang.String getFormatedMethodReturnCondition() throws ProofInputException
IExecutionMethodCall
.getFormatedMethodReturnCondition
in interface IExecutionBaseMethodReturn<S extends SourceElement>
IExecutionMethodCall
.ProofInputException