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.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
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.Copyright © 2003-2019 The KeY-Project.