public class ExecutionExceptionalMethodReturn extends AbstractExecutionMethodReturn<Throw> implements IExecutionExceptionalMethodReturn
IExecutionExceptionalMethodReturn
.INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Constructor and Description |
---|
ExecutionExceptionalMethodReturn(ITreeSettings settings,
Node proofNode,
ExecutionMethodCall methodCall)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
java.lang.String |
getElementType()
Returns a human readable element type name.
|
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 |
lazyComputeSignature()
Computes the signature lazily when
AbstractExecutionMethodReturn.getSignature() 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
public ExecutionExceptionalMethodReturn(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()
AbstractExecutionElement.getName()
is called the first time.lazyComputeName
in class AbstractExecutionElement
IExecutionNode
.protected IExecutionConstraint[] lazyComputeConstraints()
AbstractExecutionNode.getConstraints()
is
called the first time.lazyComputeConstraints
in class AbstractExecutionNode<Throw>
IExecutionConstraint
s of the current state.protected java.lang.String lazyComputeSignature() throws ProofInputException
AbstractExecutionMethodReturn.getSignature()
is called the first time.lazyComputeSignature
in class AbstractExecutionMethodReturn<Throw>
ProofInputException
public java.lang.String getElementType()
getElementType
in interface IExecutionElement