de.uka.ilkd.key.symbolic_execution.model

Interface IExecutionBlockStartNode<S extends SourceElement>

All Superinterfaces:

IExecutionElement, IExecutionNode<S>

All Known Subinterfaces:

IExecutionBranchStatement, IExecutionLoopCondition, IExecutionLoopStatement

All Known Implementing Classes:

AbstractExecutionBlockStartNode, ExecutionBranchStatement, ExecutionLoopCondition, ExecutionLoopStatement, ExecutionNodeReader.AbstractKeYlessExecutionBlockStartNode, ExecutionNodeReader.KeYlessBranchStatement, ExecutionNodeReader.KeYlessLoopCondition, ExecutionNodeReader.KeYlessLoopStatement

public interface IExecutionBlockStartNode<S extends SourceElement>
extends IExecutionNode<S>

An extended IExecutionNode which groups several child nodes.

Author:

Martin Hentschel

Field Summary

Fields inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionNode

INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START

Method Summary

Modifier and Type	Method and Description
ImmutableList<IExecutionNode<?>>	getBlockCompletions() Returns the up to now discovered IExecutionNodes.
boolean	isBlockOpened() Checks if a block might be opened.

Methods inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionNode

getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged

Methods inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionElement

getAppliedRuleApp, getElementType, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed

Method Detail

isBlockOpened

boolean isBlockOpened()

Checks if a block might be opened.

Returns:

false block is definitively not opened, true block is or might be opened.

getBlockCompletions

ImmutableList<IExecutionNode<?>> getBlockCompletions()

Returns the up to now discovered IExecutionNodes.

Returns:

The up to now discovered IExecutionNodes.