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 List<IExecutionVariable> |
callStateVariables
The contained call state variables.
|
private String |
formatedMethodReturn
The formated method return condition.
|
private String |
signature
The signature.
|
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Constructor and Description |
---|
AbstractKeYlessBaseExecutionNode(IExecutionNode<?> parent,
String name,
String formatedPathCondition,
boolean pathConditionChanged,
String signature,
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.
|
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 . |
String |
getSignature()
Returns a human readable signature which describes this element.
|
addCallStackEntry, addChild, addCompletedBlock, addConstraint, addVariable, getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getModalityPIO, 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, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged
getAppliedRuleApp, getElementType, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
private final List<IExecutionVariable> callStateVariables
private final String signature
private final String formatedMethodReturn
public AbstractKeYlessBaseExecutionNode(IExecutionNode<?> parent, String name, String formatedPathCondition, boolean pathConditionChanged, String signature, 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 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 String getFormatedMethodReturnCondition() throws ProofInputException
IExecutionMethodCall
.getFormatedMethodReturnCondition
in interface IExecutionBaseMethodReturn<S extends SourceElement>
IExecutionMethodCall
.ProofInputException