public static class ExecutionNodeReader.KeYlessMethodReturn extends ExecutionNodeReader.AbstractKeYlessBaseExecutionNode<SourceElement> implements IExecutionMethodReturn
IExecutionMethodReturn
which is independent
from KeY and provides such only children and default attributes.Modifier and Type | Field and Description |
---|---|
private java.lang.String |
nameIncludingReturnValue
The name including the return value.
|
private boolean |
returnValueComputed
Defines if the return value is computed or not.
|
private java.util.List<IExecutionMethodReturnValue> |
returnValues
The possible return values.
|
private java.lang.String |
signatureIncludingReturnValue
The signature including the return value.
|
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Constructor and Description |
---|
KeYlessMethodReturn(IExecutionNode<?> parent,
java.lang.String name,
java.lang.String formatedPathCondition,
boolean pathConditionChanged,
java.lang.String nameIncludingReturnValue,
java.lang.String signature,
java.lang.String signatureIncludingReturnValue,
boolean returnValueComputed,
java.lang.String formatedMethodReturn)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
void |
addReturnValue(IExecutionMethodReturnValue returnValue)
Adds the given
IExecutionMethodReturnValue . |
java.lang.String |
getElementType()
Returns a human readable element type name.
|
java.lang.String |
getNameIncludingReturnValue()
Returns the human readable node name including the return value (
IExecutionMethodReturn.getReturnValues() ). |
IExecutionMethodReturnValue[] |
getReturnValues()
Returns the possible return values.
|
java.lang.String |
getSignatureIncludingReturnValue()
Returns the human readable signature including the return value (
IExecutionMethodReturn.getReturnValues() ). |
boolean |
isReturnValuesComputed()
Checks if the values of
IExecutionMethodReturn.getReturnValues() are already computed. |
addCallStateVariable, getCallStateVariables, getFormatedMethodReturnCondition, getMethodCall, getMethodReturnCondition, getSignature
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
getCallStateVariables, getFormatedMethodReturnCondition, getMethodCall, getMethodReturnCondition, getSignature
getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged
getAppliedRuleApp, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
private final java.lang.String nameIncludingReturnValue
private final java.lang.String signatureIncludingReturnValue
private final boolean returnValueComputed
private final java.util.List<IExecutionMethodReturnValue> returnValues
public KeYlessMethodReturn(IExecutionNode<?> parent, java.lang.String name, java.lang.String formatedPathCondition, boolean pathConditionChanged, java.lang.String nameIncludingReturnValue, java.lang.String signature, java.lang.String signatureIncludingReturnValue, boolean returnValueComputed, 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?nameIncludingReturnValue
- The name including the return value.signature
- The signature.signatureIncludingReturnValue
- The signature including return value.returnValueComputed
- Is the return value computed?formatedMethodReturn
- The formated method return condition.public java.lang.String getNameIncludingReturnValue() throws ProofInputException
IExecutionMethodReturn.getReturnValues()
).getNameIncludingReturnValue
in interface IExecutionMethodReturn
ProofInputException
- Occurred Exception.public java.lang.String getSignatureIncludingReturnValue() throws ProofInputException
IExecutionMethodReturn.getReturnValues()
).getSignatureIncludingReturnValue
in interface IExecutionMethodReturn
ProofInputException
- Occurred Exception.public java.lang.String getElementType()
getElementType
in interface IExecutionElement
public boolean isReturnValuesComputed()
IExecutionMethodReturn.getReturnValues()
are already computed.isReturnValuesComputed
in interface IExecutionMethodReturn
true
value of IExecutionMethodReturn.getReturnValues()
are already computed, false
values of IExecutionMethodReturn.getReturnValues()
needs to be computed.public IExecutionMethodReturnValue[] getReturnValues() throws ProofInputException
getReturnValues
in interface IExecutionMethodReturn
ProofInputException
- Occurred Exception.public void addReturnValue(IExecutionMethodReturnValue returnValue)
IExecutionMethodReturnValue
.returnValue
- The IExecutionMethodReturnValue
to add.