public interface IExecutionAuxiliaryContract extends IExecutionNode<SourceElement>
A node in the symbolic execution tree which represents a use block/loop contract application.
The default implementation is ExecutionAuxiliaryContract
which
is instantiated via a SymbolicExecutionTreeBuilder
instance.
SymbolicExecutionTreeBuilder
,
ExecutionAuxiliaryContract
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. |
AuxiliaryContract |
getContract()
Returns the applied
AuxiliaryContract . |
boolean |
isPreconditionComplied()
Checks if the precondition is complied.
|
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
AuxiliaryContract getContract()
AuxiliaryContract
.AuxiliaryContract
.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.