public interface IExecutionBlockContract extends IExecutionNode<SourceElement>
A node in the symbolic execution tree which represents a use block contract application.
The default implementation is ExecutionBlockContract
which
is instantiated via a SymbolicExecutionTreeBuilder
instance.
SymbolicExecutionTreeBuilder
,
ExecutionBlockContract
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Modifier and Type | Method and Description |
---|---|
StatementBlock |
getBlock()
Returns the
StatementBlock at which the BlockContract is applied. |
BlockContract |
getContract()
Returns the applied
BlockContract . |
boolean |
isPreconditionComplied()
Checks if the precondition is complied.
|
getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged
getAppliedRuleApp, getElementType, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
BlockContract getContract()
BlockContract
.BlockContract
.StatementBlock getBlock()
StatementBlock
at which the BlockContract
is applied.StatementBlock
at which the BlockContract
is applied.boolean isPreconditionComplied()
true
precondition complied, false
precondition not complied.