de.uka.ilkd.key.symbolic_execution

Class ExecutionNodeReader.KeYlessExceptionalMethodReturn

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

de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.KeYlessExceptionalMethodReturn

All Implemented Interfaces:

IExecutionBaseMethodReturn<Throw>, IExecutionElement, IExecutionExceptionalMethodReturn, IExecutionNode<Throw>

Enclosing class:

ExecutionNodeReader

public static class ExecutionNodeReader.KeYlessExceptionalMethodReturn
extends ExecutionNodeReader.AbstractKeYlessBaseExecutionNode<Throw>
implements IExecutionExceptionalMethodReturn

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

Author:

Martin Hentschel

Field Summary

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
KeYlessExceptionalMethodReturn(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
java.lang.String	getElementType() Returns a human readable element type name.

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

Constructor Detail

KeYlessExceptionalMethodReturn

public KeYlessExceptionalMethodReturn(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

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.