public interface IExecutionLoopStatement extends IExecutionBlockStartNode<LoopStatement>
A node in the symbolic execution tree which represents a loop.
e.g. while(x >= 0)
. The loop condition (x >= 0
) itself
is represented as IExecutionLoopCondition
instance.
The default implementation is ExecutionLoopStatement
which
is instantiated via a SymbolicExecutionTreeBuilder
instance.
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
getBlockCompletions, isBlockOpened
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
Copyright © 2003-2019 The KeY-Project.