de.uka.ilkd.key.symbolic_execution.model

Interface IExecutionStatement

All Superinterfaces:

IExecutionElement, IExecutionNode<SourceElement>

All Known Implementing Classes:

ExecutionNodeReader.KeYlessStatement, ExecutionStatement

public interface IExecutionStatement
extends IExecutionNode<SourceElement>

A node in the symbolic execution tree which represents a single statement, e.g. int x = 1 + 2;.

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

Author:

Martin Hentschel

See Also:

SymbolicExecutionTreeBuilder, ExecutionStatement

Field Summary

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

INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START

Method Summary

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