public class ExecutionMethodCall extends AbstractExecutionNode<MethodBodyStatement> implements IExecutionMethodCall
IExecutionMethodCall
.Modifier and Type | Field and Description |
---|---|
private ImmutableList<IExecutionBaseMethodReturn<?>> |
methodReturns
The up to know discovered
IExecutionBaseMethodReturn s. |
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Constructor and Description |
---|
ExecutionMethodCall(ITreeSettings settings,
Node proofNode)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
void |
addMethodReturn(IExecutionBaseMethodReturn<?> methodReturn)
Registers the given
IExecutionBaseMethodReturn . |
java.lang.String |
getElementType()
Returns a human readable element type name.
|
MethodReference |
getExplicitConstructorMethodReference()
Returns a copy of the
MethodReference which calls the
explicit constructor instead of the implicit constructor. |
IProgramMethod |
getExplicitConstructorProgramMethod()
Returns the explicit constructor.
|
protected java.lang.String |
getMethodCallText()
Computes the method call text.
|
MethodReference |
getMethodReference()
Returns the
MethodReference instance of the called method. |
ImmutableList<IExecutionBaseMethodReturn<?>> |
getMethodReturns()
Returns the up to now discovered
IExecutionBaseMethodReturn s. |
IProgramMethod |
getProgramMethod()
Returns the called
IProgramMethod . |
boolean |
isImplicitConstructor()
Checks if an implicit constructor is called.
|
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. |
void |
removeMethodReturn(IExecutionBaseMethodReturn<?> methodReturn)
Removes the given
IExecutionBaseMethodReturn . |
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
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 ImmutableList<IExecutionBaseMethodReturn<?>> methodReturns
IExecutionBaseMethodReturn
s.public ExecutionMethodCall(ITreeSettings settings, Node proofNode)
settings
- The ITreeSettings
to use.proofNode
- The Node
of KeY's proof tree which is represented by this IExecutionNode
.protected java.lang.String lazyComputeName()
AbstractExecutionElement.getName()
is called the first time.lazyComputeName
in class AbstractExecutionElement
IExecutionNode
.protected java.lang.String getMethodCallText()
public void removeMethodReturn(IExecutionBaseMethodReturn<?> methodReturn)
IExecutionBaseMethodReturn
.methodReturn
- The IExecutionBaseMethodReturn
to be deleted.public boolean isImplicitConstructor()
isImplicitConstructor
in interface IExecutionMethodCall
true
implicit constructor is called, false
method or explicit constructor is called.public MethodReference getExplicitConstructorMethodReference()
MethodReference
which calls the
explicit constructor instead of the implicit constructor.getExplicitConstructorMethodReference
in interface IExecutionMethodCall
MethodReference
to the explicit constructor or null
if no constructor is called.public IProgramMethod getExplicitConstructorProgramMethod()
getExplicitConstructorProgramMethod
in interface IExecutionMethodCall
null
if no constructor is called.public MethodReference getMethodReference()
MethodReference
instance of the called method.getMethodReference
in interface IExecutionMethodCall
MethodReference
of the called method.public IProgramMethod getProgramMethod()
IProgramMethod
.getProgramMethod
in interface IExecutionMethodCall
IProgramMethod
.public java.lang.String getElementType()
getElementType
in interface IExecutionElement
public ImmutableList<IExecutionBaseMethodReturn<?>> getMethodReturns()
IExecutionBaseMethodReturn
s.getMethodReturns
in interface IExecutionMethodCall
IExecutionBaseMethodReturn
s.public void addMethodReturn(IExecutionBaseMethodReturn<?> methodReturn)
IExecutionBaseMethodReturn
.methodReturn
- The IExecutionBaseMethodReturn
to register.protected IExecutionConstraint[] lazyComputeConstraints()
AbstractExecutionNode.getConstraints()
is
called the first time.lazyComputeConstraints
in class AbstractExecutionNode<MethodBodyStatement>
IExecutionConstraint
s of the current state.