de.uka.ilkd.key.symbolic_execution.model

Interface IExecutionTermination

All Superinterfaces:

IExecutionElement, IExecutionNode<SourceElement>

All Known Implementing Classes:

ExecutionNodeReader.KeYlessTermination, ExecutionTermination

public interface IExecutionTermination
extends IExecutionNode<SourceElement>

A node in the symbolic execution tree which represents the normal termination of a branch, e.g. <end> in case of normal termination or <uncaught java.lang.NullPointerException> in case of exceptional termination.

The default implementation is ExecutionTermination which is instantiated via a SymbolicExecutionTreeBuilder instance.

Author:

Martin Hentschel

See Also:

SymbolicExecutionTreeBuilder, ExecutionTermination

Nested Class Summary

Nested Classes

Modifier and Type	Interface and Description
static class	IExecutionTermination.TerminationKind Defines the possible termination kinds.

Field Summary

Fields

Modifier and Type	Field and Description
static java.lang.String	LOOP_BODY_TERMINATION_NODE_NAME The default name of a termination node with IExecutionTermination.TerminationKind.LOOP_BODY.
static java.lang.String	NORMAL_TERMINATION_NODE_NAME The default name of a termination node with IExecutionTermination.TerminationKind.NORMAL.

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

INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START

Method Summary

Modifier and Type	Method and Description
Sort	getExceptionSort() Returns the Sort of the caught exception.
IProgramVariable	getExceptionVariable() Returns the IProgramVariable which is used in the Sequent of Proof.root() to check if a normal or exceptional termination occurred.
IExecutionTermination.TerminationKind	getTerminationKind() Returns the IExecutionTermination.TerminationKind.
boolean	isBranchVerified() Checks if this branch would be closed without the uninterpreted predicate and thus be treated as valid/closed in a regular proof.

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

NORMAL_TERMINATION_NODE_NAME

static final java.lang.String NORMAL_TERMINATION_NODE_NAME

The default name of a termination node with IExecutionTermination.TerminationKind.NORMAL.

See Also:

Constant Field Values

LOOP_BODY_TERMINATION_NODE_NAME

static final java.lang.String LOOP_BODY_TERMINATION_NODE_NAME

The default name of a termination node with IExecutionTermination.TerminationKind.LOOP_BODY.

See Also:

Constant Field Values

Method Detail

getExceptionVariable

IProgramVariable getExceptionVariable()

Returns the IProgramVariable which is used in the Sequent of Proof.root() to check if a normal or exceptional termination occurred.

Returns:

The IProgramVariable which is used to caught global exceptions.

getExceptionSort

Sort getExceptionSort()

Returns the Sort of the caught exception.

Returns:

The Sort of the caught exception.

getTerminationKind

IExecutionTermination.TerminationKind getTerminationKind()

Returns the IExecutionTermination.TerminationKind.

Returns:

The IExecutionTermination.TerminationKind.

isBranchVerified

boolean isBranchVerified()

Checks if this branch would be closed without the uninterpreted predicate and thus be treated as valid/closed in a regular proof.

Returns:

true verified/closed, false not verified/still open