de.uka.ilkd.key.symbolic_execution

Class ExecutionNodeReader.KeYlessMethodReturn

java.lang.Object

de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.AbstractKeYlessExecutionElement

de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.AbstractKeYlessExecutionNode<S>

de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.AbstractKeYlessBaseExecutionNode<SourceElement>

de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.KeYlessMethodReturn

All Implemented Interfaces:

IExecutionBaseMethodReturn<SourceElement>, IExecutionElement, IExecutionMethodReturn, IExecutionNode<SourceElement>

Enclosing class:

ExecutionNodeReader

public static class ExecutionNodeReader.KeYlessMethodReturn
extends ExecutionNodeReader.AbstractKeYlessBaseExecutionNode<SourceElement>
implements IExecutionMethodReturn

An implementation of IExecutionMethodReturn which is independent from KeY and provides such only children and default attributes.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private java.lang.String	nameIncludingReturnValue The name including the return value.
private boolean	returnValueComputed Defines if the return value is computed or not.
private java.util.List<IExecutionMethodReturnValue>	returnValues The possible return values.
private java.lang.String	signatureIncludingReturnValue The signature including the return value.

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

Method Summary

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.

Methods inherited from class de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.AbstractKeYlessBaseExecutionNode

addCallStateVariable, getCallStateVariables, getFormatedMethodReturnCondition, getMethodCall, getMethodReturnCondition, getSignature

Methods inherited from class de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.AbstractKeYlessExecutionNode

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

Methods inherited from class de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.AbstractKeYlessExecutionElement

getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, 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.IExecutionBaseMethodReturn

getCallStateVariables, getFormatedMethodReturnCondition, getMethodCall, getMethodReturnCondition, getSignature

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

nameIncludingReturnValue

private final java.lang.String nameIncludingReturnValue

The name including the return value.

signatureIncludingReturnValue

private final java.lang.String signatureIncludingReturnValue

The signature including the return value.

returnValueComputed

private final boolean returnValueComputed

Defines if the return value is computed or not.

returnValues

private final java.util.List<IExecutionMethodReturnValue> returnValues

The possible return values.

Constructor Detail

KeYlessMethodReturn

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)

Constructor.

Parameters:

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.

Method Detail

getNameIncludingReturnValue

public java.lang.String getNameIncludingReturnValue()
                                             throws ProofInputException

Returns the human readable node name including the return value (IExecutionMethodReturn.getReturnValues()).

Specified by:

getNameIncludingReturnValue in interface IExecutionMethodReturn

Returns:

The human readable node name including the return value.

Throws:

ProofInputException - Occurred Exception.

getSignatureIncludingReturnValue

public java.lang.String getSignatureIncludingReturnValue()
                                                  throws ProofInputException

Returns the human readable signature including the return value (IExecutionMethodReturn.getReturnValues()).

Specified by:

getSignatureIncludingReturnValue in interface IExecutionMethodReturn

Returns:

The human readable signature including the return value.

Throws:

ProofInputException - Occurred Exception.

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.

isReturnValuesComputed

public boolean isReturnValuesComputed()

Checks if the values of IExecutionMethodReturn.getReturnValues() are already computed.

Specified by:

isReturnValuesComputed in interface IExecutionMethodReturn

Returns:

true value of IExecutionMethodReturn.getReturnValues() are already computed, false values of IExecutionMethodReturn.getReturnValues() needs to be computed.

getReturnValues

public IExecutionMethodReturnValue[] getReturnValues()
                                              throws ProofInputException

Returns the possible return values.

Specified by:

getReturnValues in interface IExecutionMethodReturn

Returns:

The possible return values.

Throws:

ProofInputException - Occurred Exception.

addReturnValue

public void addReturnValue(IExecutionMethodReturnValue returnValue)

Adds the given IExecutionMethodReturnValue.

Parameters:

returnValue - The IExecutionMethodReturnValue to add.