de.uka.ilkd.key.symbolic_execution

Class ExecutionNodeReader.AbstractKeYlessBaseExecutionNode<S extends SourceElement>

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

All Implemented Interfaces:

IExecutionBaseMethodReturn<S>, IExecutionElement, IExecutionNode<S>

Direct Known Subclasses:

ExecutionNodeReader.KeYlessExceptionalMethodReturn, ExecutionNodeReader.KeYlessMethodReturn

Enclosing class:

ExecutionNodeReader

public abstract static class ExecutionNodeReader.AbstractKeYlessBaseExecutionNode<S extends SourceElement>
extends ExecutionNodeReader.AbstractKeYlessExecutionNode<S>
implements IExecutionBaseMethodReturn<S>

An implementation of IExecutionBaseMethodReturn 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.util.List<IExecutionVariable>	callStateVariables The contained call state variables.
private java.lang.String	formatedMethodReturn The formated method return condition.
private java.lang.String	signature The signature.

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
AbstractKeYlessBaseExecutionNode(IExecutionNode<?> parent, java.lang.String name, java.lang.String formatedPathCondition, boolean pathConditionChanged, java.lang.String signature, java.lang.String formatedMethodReturn) Constructor.

Method Summary

Modifier and Type	Method and Description
void	addCallStateVariable(IExecutionVariable variable) Adds the given IExecutionVariable.
IExecutionVariable[]	getCallStateVariables() Returns the variable value pairs of the state when the method has been called.
java.lang.String	getFormatedMethodReturnCondition() Returns the human readable condition under which this method return is reached from the calling IExecutionMethodCall.
IExecutionMethodCall	getMethodCall() A reference to the IExecutionMethodCall which is now returned.
Term	getMethodReturnCondition() Returns the condition under which this method return is reached from the calling IExecutionMethodCall.
java.lang.String	getSignature() Returns a human readable signature which describes this element.

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

Field Detail

callStateVariables

private final java.util.List<IExecutionVariable> callStateVariables

The contained call state variables.

signature

private final java.lang.String signature

The signature.

formatedMethodReturn

private final java.lang.String formatedMethodReturn

The formated method return condition.

Constructor Detail

AbstractKeYlessBaseExecutionNode

public AbstractKeYlessBaseExecutionNode(IExecutionNode<?> parent,
                                        java.lang.String name,
                                        java.lang.String formatedPathCondition,
                                        boolean pathConditionChanged,
                                        java.lang.String signature,
                                        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?

signature - The signature.

formatedMethodReturn - The formated method return condition.

Method Detail

getCallStateVariables

public IExecutionVariable[] getCallStateVariables()

Returns the variable value pairs of the state when the method has been called.

Specified by:

getCallStateVariables in interface IExecutionBaseMethodReturn<S extends SourceElement>

Returns:

The variable value pairs.

addCallStateVariable

public void addCallStateVariable(IExecutionVariable variable)

Adds the given IExecutionVariable.

Parameters:

variable - The IExecutionVariable to add.

getMethodCall

public IExecutionMethodCall getMethodCall()

A reference to the IExecutionMethodCall which is now returned.

Specified by:

getMethodCall in interface IExecutionBaseMethodReturn<S extends SourceElement>

Returns:

The call of the now returned method.

getSignature

public java.lang.String getSignature()
                              throws ProofInputException

Returns a human readable signature which describes this element.

Specified by:

getSignature in interface IExecutionBaseMethodReturn<S extends SourceElement>

Returns:

The human readable signature which describes this element.

Throws:

ProofInputException - Occurred Exception.

getMethodReturnCondition

public Term getMethodReturnCondition()
                              throws ProofInputException

Returns the condition under which this method return is reached from the calling IExecutionMethodCall.

Specified by:

getMethodReturnCondition in interface IExecutionBaseMethodReturn<S extends SourceElement>

Returns:

The method return condition to reach this node from its IExecutionMethodCall as Term.

Throws:

ProofInputException

getFormatedMethodReturnCondition

public java.lang.String getFormatedMethodReturnCondition()
                                                  throws ProofInputException

Returns the human readable condition under which this method return is reached from the calling IExecutionMethodCall.

Specified by:

getFormatedMethodReturnCondition in interface IExecutionBaseMethodReturn<S extends SourceElement>

Returns:

The human readable method return condition to reach this node from its IExecutionMethodCall.

Throws:

ProofInputException