public class ExecutionMethodReturn extends AbstractExecutionMethodReturn<SourceElement> implements IExecutionMethodReturn
IExecutionMethodReturn
.Modifier and Type | Field and Description |
---|---|
private java.lang.String |
nameIncludingReturnValue
The node name including the return value.
|
private IExecutionMethodReturnValue[] |
returnValues
The possible return values.
|
private java.lang.String |
signatureIncludingReturnValue
The node name with signature including the return value.
|
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Constructor and Description |
---|
ExecutionMethodReturn(ITreeSettings settings,
Node proofNode,
ExecutionMethodCall methodCall)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
protected java.lang.String |
computeCalledMethodName()
Computes the name of the called method.
|
protected java.lang.String |
computeCalledMethodSignature()
Computes the signature of the called method.
|
static java.lang.String |
createMethodReturnName(java.lang.Object returnValue,
java.lang.String methodName)
Creates the human readable name which is shown in
IExecutionMethodReturn instances. |
protected Node |
findMethodReturnNode(Node node)
Searches from the given
Node the parent which applies
the rule "methodCallReturn" in the same modality. |
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. |
protected IExecutionConstraint[] |
lazyComputeConstraints()
Computes the constraints lazily when
AbstractExecutionNode.getConstraints() is
called the first time. |
protected java.lang.String |
lazyComputeName()
Computes the name of this node lazily when
AbstractExecutionElement.getName()
is called the first time. |
protected java.lang.String |
lazyComputeNameIncludingReturnValue()
Computes the name including the return value lazily when
getNameIncludingReturnValue() is called the first time. |
protected IExecutionMethodReturnValue[] |
lazyComputeReturnValues()
Computes the return value lazily when
#getReturnValue() is called the first time. |
protected java.lang.String |
lazyComputeSignature()
Computes the signature lazily when
AbstractExecutionMethodReturn.getSignature() is called the first time. |
protected java.lang.String |
lazyComputeSigntureIncludingReturnValue()
Computes the signature including the return value lazily when
getNameIncludingReturnValue() is called the first time. |
getCallStateVariables, getFormatedMethodReturnCondition, getMethodCall, getMethodReturnCondition, getSignature, lazyComputeCallStateVariables, lazyComputeMethodReturnCondition
addChild, addCompletedBlock, addIncomingLink, addOutgoingLink, getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutExtractor, getLayoutsCount, getLayoutsEquivalenceClasses, getModalityPIO, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged, lazyComputeBlockCompletionCondition, lazyComputeLayoutExtractor, lazyComputeModalityPIO, lazyComputeVariables, lazyComputeVariables, removeChild, removeCompletedBlock, removeIncomingLink, removeOutgoingLink, setCallStack, setParent
formatTerm, getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, isNameComputed, setName, 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 java.lang.String signatureIncludingReturnValue
private java.lang.String nameIncludingReturnValue
private IExecutionMethodReturnValue[] returnValues
public ExecutionMethodReturn(ITreeSettings settings, Node proofNode, ExecutionMethodCall methodCall)
settings
- The ITreeSettings
to use.proofNode
- The Node
of KeY's proof tree which is represented by this IExecutionNode
.methodCall
- The IExecutionMethodCall
which is now returned.protected java.lang.String lazyComputeName() throws ProofInputException
AbstractExecutionElement.getName()
is called the first time.lazyComputeName
in class AbstractExecutionElement
IExecutionNode
.ProofInputException
protected java.lang.String computeCalledMethodName()
protected java.lang.String lazyComputeSignature() throws ProofInputException
AbstractExecutionMethodReturn.getSignature()
is called the first time.lazyComputeSignature
in class AbstractExecutionMethodReturn<SourceElement>
ProofInputException
protected java.lang.String computeCalledMethodSignature() throws ProofInputException
ProofInputException
public java.lang.String getNameIncludingReturnValue() throws ProofInputException
IExecutionMethodReturn.getReturnValues()
).getNameIncludingReturnValue
in interface IExecutionMethodReturn
ProofInputException
- Occurred Exception.protected java.lang.String lazyComputeNameIncludingReturnValue() throws ProofInputException
getNameIncludingReturnValue()
is called the first time.Occurred
- Exception.ProofInputException
public java.lang.String getSignatureIncludingReturnValue() throws ProofInputException
IExecutionMethodReturn.getReturnValues()
).getSignatureIncludingReturnValue
in interface IExecutionMethodReturn
ProofInputException
- Occurred Exception.protected java.lang.String lazyComputeSigntureIncludingReturnValue() throws ProofInputException
getNameIncludingReturnValue()
is called the first time.Occurred
- Exception.ProofInputException
public IExecutionMethodReturnValue[] getReturnValues() throws ProofInputException
getReturnValues
in interface IExecutionMethodReturn
ProofInputException
- Occurred Exception.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.protected IExecutionMethodReturnValue[] lazyComputeReturnValues() throws ProofInputException
#getReturnValue()
is called the first time.ProofInputException
- Occurred Exception.protected Node findMethodReturnNode(Node node)
Node
the parent which applies
the rule "methodCallReturn" in the same modality.public static java.lang.String createMethodReturnName(java.lang.Object returnValue, java.lang.String methodName)
IExecutionMethodReturn
instances.returnValue
- The return value.methodName
- The name of the method that is completely executed.protected IExecutionConstraint[] lazyComputeConstraints()
AbstractExecutionNode.getConstraints()
is
called the first time.lazyComputeConstraints
in class AbstractExecutionNode<SourceElement>
IExecutionConstraint
s of the current state.public java.lang.String getElementType()
getElementType
in interface IExecutionElement