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 String |
nameIncludingReturnValue
The name including the return value.
|
private boolean |
returnValueComputed
Defines if the return value is computed or not.
|
private List<IExecutionMethodReturnValue> |
returnValues
The possible return values.
|
private String |
signatureIncludingReturnValue
The signature including the return value.
|
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Constructor and Description |
---|
ExecutionNodeReader.KeYlessMethodReturn(IExecutionNode<?> parent,
String name,
String formatedPathCondition,
boolean pathConditionChanged,
String nameIncludingReturnValue,
String signature,
String signatureIncludingReturnValue,
boolean returnValueComputed,
String formatedMethodReturn)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
void |
addReturnValue(IExecutionMethodReturnValue returnValue)
Adds the given
IExecutionMethodReturnValue . |
String |
getElementType()
Returns a human readable element type name.
|
String |
getNameIncludingReturnValue()
Returns the human readable node name including the return value (
IExecutionMethodReturn.getReturnValues() ). |
IExecutionMethodReturnValue[] |
getReturnValues()
Returns the possible return values.
|
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, 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
getCallStateVariables, getFormatedMethodReturnCondition, getMethodCall, getMethodReturnCondition, getSignature
getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged
getAppliedRuleApp, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
private final String nameIncludingReturnValue
private final String signatureIncludingReturnValue
private final boolean returnValueComputed
private final List<IExecutionMethodReturnValue> returnValues
public ExecutionNodeReader.KeYlessMethodReturn(IExecutionNode<?> parent, String name, String formatedPathCondition, boolean pathConditionChanged, String nameIncludingReturnValue, String signature, String signatureIncludingReturnValue, boolean returnValueComputed, 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 String getNameIncludingReturnValue() throws ProofInputException
IExecutionMethodReturn.getReturnValues()
).getNameIncludingReturnValue
in interface IExecutionMethodReturn
ProofInputException
- Occurred Exception.public String getSignatureIncludingReturnValue() throws ProofInputException
IExecutionMethodReturn.getReturnValues()
).getSignatureIncludingReturnValue
in interface IExecutionMethodReturn
ProofInputException
- Occurred Exception.public 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.