de.uka.ilkd.key.symbolic_execution.model

Interface IExecutionStart

All Superinterfaces:

IExecutionElement, IExecutionNode<SourceElement>

All Known Implementing Classes:

ExecutionNodeReader.KeYlessStart, ExecutionStart

public interface IExecutionStart
extends IExecutionNode<SourceElement>

The start node of a symbolic execution tree.

The default implementation is ExecutionStart which is instantiated via a SymbolicExecutionTreeBuilder instance.

Author:

Martin Hentschel

See Also:

SymbolicExecutionTreeBuilder, ExecutionStart

Field Summary

Fields

Modifier and Type	Field and Description
static java.lang.String	DEFAULT_START_NODE_NAME The default name of an IExecutionStart.

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<IExecutionTermination>	getTerminations() Returns the up to now discovered IExecutionTerminations.

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

Field Detail

DEFAULT_START_NODE_NAME

static final java.lang.String DEFAULT_START_NODE_NAME

The default name of an IExecutionStart.

See Also:

Constant Field Values

Method Detail

getTerminations

ImmutableList<IExecutionTermination> getTerminations()

Returns the up to now discovered IExecutionTerminations.

Returns:

The up to now discovered IExecutionTerminations.