de.uka.ilkd.key.symbolic_execution.model.impl

Class ExecutionMethodCall

java.lang.Object

de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionElement

de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionNode<MethodBodyStatement>

de.uka.ilkd.key.symbolic_execution.model.impl.ExecutionMethodCall

All Implemented Interfaces:

IExecutionElement, IExecutionMethodCall, IExecutionNode<MethodBodyStatement>

public class ExecutionMethodCall
extends AbstractExecutionNode<MethodBodyStatement>
implements IExecutionMethodCall

The default implementation of IExecutionMethodCall.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private ImmutableList<IExecutionBaseMethodReturn<?>>	methodReturns The up to know discovered IExecutionBaseMethodReturns.

Fields inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionNode

INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START

Constructor Summary

Constructors

Constructor and Description
ExecutionMethodCall(ITreeSettings settings, Node proofNode) Constructor.

Method Summary

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 IExecutionBaseMethodReturns.
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.

Methods inherited from class de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionNode

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

Methods inherited from class de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionElement

formatTerm, getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, isNameComputed, setName, toString

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionNode

getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged

Methods inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionElement

getAppliedRuleApp, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed

Field Detail

methodReturns

private ImmutableList<IExecutionBaseMethodReturn<?>> methodReturns

The up to know discovered IExecutionBaseMethodReturns.

Constructor Detail

ExecutionMethodCall

public ExecutionMethodCall(ITreeSettings settings,
                           Node proofNode)

Constructor.

Parameters:

settings - The ITreeSettings to use.

proofNode - The Node of KeY's proof tree which is represented by this IExecutionNode.

Method Detail

lazyComputeName

protected java.lang.String lazyComputeName()

Computes the name of this node lazily when AbstractExecutionElement.getName() is called the first time.

Specified by:

lazyComputeName in class AbstractExecutionElement

Returns:

The human readable name of this IExecutionNode.

getMethodCallText

protected java.lang.String getMethodCallText()

Computes the method call text.

Returns:

The method call text.

removeMethodReturn

public void removeMethodReturn(IExecutionBaseMethodReturn<?> methodReturn)

Removes the given IExecutionBaseMethodReturn.

Parameters:

methodReturn - The IExecutionBaseMethodReturn to be deleted.

isImplicitConstructor

public boolean isImplicitConstructor()

Checks if an implicit constructor is called.

Specified by:

isImplicitConstructor in interface IExecutionMethodCall

Returns:

true implicit constructor is called, false method or explicit constructor is called.

getExplicitConstructorMethodReference

public MethodReference getExplicitConstructorMethodReference()

Returns a copy of the MethodReference which calls the explicit constructor instead of the implicit constructor.

Specified by:

getExplicitConstructorMethodReference in interface IExecutionMethodCall

Returns:

The MethodReference to the explicit constructor or null if no constructor is called.

getExplicitConstructorProgramMethod

public IProgramMethod getExplicitConstructorProgramMethod()

Returns the explicit constructor.

Specified by:

getExplicitConstructorProgramMethod in interface IExecutionMethodCall

Returns:

The explicit constructor or null if no constructor is called.

getMethodReference

public MethodReference getMethodReference()

Returns the MethodReference instance of the called method.

Specified by:

getMethodReference in interface IExecutionMethodCall

Returns:

The MethodReference of the called method.

getProgramMethod

public IProgramMethod getProgramMethod()

Returns the called IProgramMethod.

Specified by:

getProgramMethod in interface IExecutionMethodCall

Returns:

The called IProgramMethod.

getElementType

public java.lang.String getElementType()

Returns a human readable element type name.

Specified by:

getElementType in interface IExecutionElement

Returns:

The human readable element type.

getMethodReturns

public ImmutableList<IExecutionBaseMethodReturn<?>> getMethodReturns()

Returns the up to now discovered IExecutionBaseMethodReturns.

Specified by:

getMethodReturns in interface IExecutionMethodCall

Returns:

The up to now discovered IExecutionBaseMethodReturns.

addMethodReturn

public void addMethodReturn(IExecutionBaseMethodReturn<?> methodReturn)

Registers the given IExecutionBaseMethodReturn.

Parameters:

methodReturn - The IExecutionBaseMethodReturn to register.

lazyComputeConstraints

protected IExecutionConstraint[] lazyComputeConstraints()

Computes the constraints lazily when AbstractExecutionNode.getConstraints() is called the first time.

Specified by:

lazyComputeConstraints in class AbstractExecutionNode<MethodBodyStatement>

Returns:

The IExecutionConstraints of the current state.