public interface IExecutionBranchCondition extends IExecutionNode<SourceElement>
A node in the symbolic execution tree which represents a branch condition,
e.g. x < 0
.
The default implementation is ExecutionBranchCondition
which
is instantiated via a SymbolicExecutionTreeBuilder
instance.
SymbolicExecutionTreeBuilder
,
ExecutionBranchCondition
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Modifier and Type | Method and Description |
---|---|
java.lang.String |
getAdditionalBranchLabel()
Returns the optional additional branch label.
|
Term |
getBranchCondition()
Returns the branch condition as
Term . |
java.lang.String |
getFormatedBranchCondition()
Returns the human readable branch condition as string.
|
Term[] |
getMergedBranchCondtions()
Returns the branch condition
Term s. |
Node[] |
getMergedProofNodes()
Returns the branch condition nodes in KeY's proof tree
which are merged into this
IExecutionBranchCondition . |
boolean |
isBranchConditionComputed()
Checks if the value of
getBranchCondition() is already computed. |
boolean |
isMergedBranchCondition()
Checks if this branch condition is a merged one.
|
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
java.lang.String getAdditionalBranchLabel()
null
if not available.boolean isBranchConditionComputed()
getBranchCondition()
is already computed.true
value of getBranchCondition()
is already computed, false
value of getBranchCondition()
needs to be computed.Term getBranchCondition() throws ProofInputException
Returns the branch condition as Term
.
If this branch conditions merged proof nodes this Term
is the overall branch condition.
Term
.ProofInputException
java.lang.String getFormatedBranchCondition() throws ProofInputException
ProofInputException
boolean isMergedBranchCondition()
true
is merged branch condition, false
is normal branch condition.Node[] getMergedProofNodes()
Returns the branch condition nodes in KeY's proof tree
which are merged into this IExecutionBranchCondition
.
It includes also IExecutionElement.getProofNode()
.
Term[] getMergedBranchCondtions() throws ProofInputException
Term
s.Term
s.ProofInputException