public static class ExecutionNodeReader.KeYlessTermination extends ExecutionNodeReader.AbstractKeYlessExecutionNode<SourceElement> implements IExecutionTermination
IExecutionTermination
which is independent
from KeY and provides such only children and default attributes.IExecutionTermination.TerminationKind
Modifier and Type | Field and Description |
---|---|
private boolean |
branchVerified
The branch verified flag.
|
private IExecutionTermination.TerminationKind |
terminationKind
|
LOOP_BODY_TERMINATION_NODE_NAME, NORMAL_TERMINATION_NODE_NAME
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Constructor and Description |
---|
KeYlessTermination(IExecutionNode<?> parent,
java.lang.String name,
java.lang.String formatedPathCondition,
boolean pathConditionChanged,
IExecutionTermination.TerminationKind terminationKind,
boolean branchVerified)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
java.lang.String |
getElementType()
Returns a human readable element type name.
|
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.
|
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
getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, toString
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged
getAppliedRuleApp, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
private final IExecutionTermination.TerminationKind terminationKind
private final boolean branchVerified
public KeYlessTermination(IExecutionNode<?> parent, java.lang.String name, java.lang.String formatedPathCondition, boolean pathConditionChanged, IExecutionTermination.TerminationKind terminationKind, boolean branchVerified)
parent
- The parent IExecutionNode
.name
- The name of this node.formatedPathCondition
- The formated path condition.pathConditionChanged
- Is the path condition changed compared to parent?exceptionalTermination
- Exceptional termination?branchVerified
- The branch verified flag.public IProgramVariable getExceptionVariable()
IProgramVariable
which is used in the Sequent
of Proof.root()
to check if a normal or exceptional termination
occurred.getExceptionVariable
in interface IExecutionTermination
IProgramVariable
which is used to caught global exceptions.public Sort getExceptionSort()
Sort
of the caught exception.getExceptionSort
in interface IExecutionTermination
Sort
of the caught exception.public java.lang.String getElementType()
getElementType
in interface IExecutionElement
public IExecutionTermination.TerminationKind getTerminationKind()
IExecutionTermination.TerminationKind
.getTerminationKind
in interface IExecutionTermination
IExecutionTermination.TerminationKind
.public boolean isBranchVerified()
isBranchVerified
in interface IExecutionTermination
true
verified/closed, false
not verified/still open