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.
SymbolicExecutionTreeBuilder
,
ExecutionTermination
Modifier and Type | Interface and Description |
---|---|
static class |
IExecutionTermination.TerminationKind
Defines the possible termination kinds.
|
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 . |
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
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.
|
getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged
getAppliedRuleApp, getElementType, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
static final java.lang.String NORMAL_TERMINATION_NODE_NAME
IExecutionTermination.TerminationKind.NORMAL
.static final java.lang.String LOOP_BODY_TERMINATION_NODE_NAME
IExecutionTermination.TerminationKind.LOOP_BODY
.IProgramVariable getExceptionVariable()
IProgramVariable
which is used in the Sequent
of Proof.root()
to check if a normal or exceptional termination
occurred.IProgramVariable
which is used to caught global exceptions.Sort getExceptionSort()
Sort
of the caught exception.Sort
of the caught exception.IExecutionTermination.TerminationKind getTerminationKind()
IExecutionTermination.TerminationKind
.IExecutionTermination.TerminationKind
.boolean isBranchVerified()
true
verified/closed, false
not verified/still open