IExecutionNode (KeY API Documentation)

All Superinterfaces:

IExecutionElement

All Known Subinterfaces:

IExecutionAuxiliaryContract, IExecutionBaseMethodReturn<S>, IExecutionBlockStartNode<S>, IExecutionBranchCondition, IExecutionBranchStatement, IExecutionExceptionalMethodReturn, IExecutionJoin, IExecutionLoopCondition, IExecutionLoopInvariant, IExecutionLoopStatement, IExecutionMethodCall, IExecutionMethodReturn, IExecutionOperationContract, IExecutionStart, IExecutionStatement, IExecutionTermination

All Known Implementing Classes:

AbstractExecutionBlockStartNode, AbstractExecutionMethodReturn, AbstractExecutionNode, ExecutionAuxiliaryContract, ExecutionBranchCondition, ExecutionBranchStatement, ExecutionExceptionalMethodReturn, ExecutionJoin, ExecutionLoopCondition, ExecutionLoopInvariant, ExecutionLoopStatement, ExecutionMethodCall, ExecutionMethodReturn, ExecutionNodeReader.AbstractKeYlessBaseExecutionNode, ExecutionNodeReader.AbstractKeYlessExecutionBlockStartNode, ExecutionNodeReader.AbstractKeYlessExecutionNode, ExecutionNodeReader.KeYlessBlockContract, ExecutionNodeReader.KeYlessBranchCondition, ExecutionNodeReader.KeYlessBranchStatement, ExecutionNodeReader.KeYlessExceptionalMethodReturn, ExecutionNodeReader.KeYlessJoin, ExecutionNodeReader.KeYlessLoopCondition, ExecutionNodeReader.KeYlessLoopInvariant, ExecutionNodeReader.KeYlessLoopStatement, ExecutionNodeReader.KeYlessMethodCall, ExecutionNodeReader.KeYlessMethodReturn, ExecutionNodeReader.KeYlessOperationContract, ExecutionNodeReader.KeYlessStart, ExecutionNodeReader.KeYlessStatement, ExecutionNodeReader.KeYlessTermination, ExecutionOperationContract, ExecutionStart, ExecutionStatement, ExecutionTermination
```
public interface IExecutionNode<S extends SourceElement>
extends IExecutionElement
```
Provides the basic methods each node in a symbolic execution tree should have and allows to access the children. A symbolic execution tree always starts with an IExecutionStart and is created via a SymbolicExecutionTreeBuilder instance.

The following concrete nodes are available
- IExecutionStart (root node)
- IExecutionStatement (single statement, e.g. int x = 1 + 2;)
- IExecutionBranchStatement (branch statement, e.g. if(x >= 0))
- IExecutionBranchCondition (branch condition, e.g. x < 0)
- IExecutionMethodCall (method call, e.g. foo())
- IExecutionMethodReturn (method return, e.g. return 42)
- IExecutionTermination (termination, e.g. <end> or <uncaught java.lang.NullPointerException>)
Author:

Martin Hentschel

Field Summary

Fields
Modifier and Type	Field and Description
`static java.lang.String`	`INTERNAL_NODE_NAME_END` Suffix that is used in `IExecutionNode`s which represents an internal state in KeY which is not part of the source code.
`static java.lang.String`	`INTERNAL_NODE_NAME_START` Prefix that is used in `IExecutionNode`s which represents an internal state in KeY which is not part of the source code.

Method Summary

All Methods Instance Methods Abstract Methods
Modifier and Type	Method and Description
`PositionInfo`	`getActivePositionInfo()` Returns the `PositionInfo` of `getActiveStatement()`.
`S`	`getActiveStatement()` Returns the active statement which is executed in the code.
`Term`	`getBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode)` Returns the condition under which this node completes the code block of the given `IExecutionBlockStartNode`.
`IExecutionNode<?>[]`	`getCallStack()` Returns the method call stack.
`IExecutionNode<?>[]`	`getChildren()` Returns the available children.
`ImmutableList<IExecutionBlockStartNode<?>>`	`getCompletedBlocks()` Returns all code blocks completed by this `IExecutionBlockStartNode`.
`IExecutionConstraint[]`	`getConstraints()` Returns all available `IExecutionConstraint`s.
`ISymbolicLayout`	`getCurrentLayout(int layoutIndex)` Returns the current memory layout which shows the memory structure before the current node in the symbolic execution tree is executed.
`java.lang.String`	`getFormatedBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode)` Returns the human readable condition under which this node completes the code block of the given `IExecutionBlockStartNode`.
`java.lang.String`	`getFormatedPathCondition()` Returns the human readable path condition to reach this node as string.
`IExecutionLink`	`getIncomingLink(IExecutionNode<?> source)` Returns the incoming `IExecutionLink`.
`ImmutableList<IExecutionLink>`	`getIncomingLinks()` Returns all available incoming links.
`ISymbolicLayout`	`getInitialLayout(int layoutIndex)` Returns the initial memory layout before the method was executed.
`int`	`getLayoutsCount()` Returns the number of memory layouts.
`ImmutableList<ISymbolicEquivalenceClass>`	`getLayoutsEquivalenceClasses(int layoutIndex)` Returns the equivalence classes of the memory layout with the given index.
`IExecutionLink`	`getOutgoingLink(IExecutionNode<?> target)` Returns the outgoing `IExecutionLink`.
`ImmutableList<IExecutionLink>`	`getOutgoingLinks()` Returns all available outgoing links.
`IExecutionNode<?>`	`getParent()` Returns the parent `IExecutionNode` or `null` if the current node is the root.
`Term`	`getPathCondition()` Returns the path condition to reach this node as `Term`.
`IExecutionVariable[]`	`getVariables()` Returns the variable value pairs of the current state.
`IExecutionVariable[]`	`getVariables(Term condition)` Returns the variable value pairs of the current state under the given condition.
`boolean`	`isPathConditionChanged()` Checks if this node has changed the path condition of the parent.

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
  - INTERNAL_NODE_NAME_START
```
static final java.lang.String INTERNAL_NODE_NAME_START
```
    Prefix that is used in IExecutionNodes which represents an internal state in KeY which is not part of the source code.
    
    See Also:
    
    Constant Field Values
  - INTERNAL_NODE_NAME_END
```
static final java.lang.String INTERNAL_NODE_NAME_END
```
    Suffix that is used in IExecutionNodes which represents an internal state in KeY which is not part of the source code.
    
    See Also:
    
    Constant Field Values
- Method Detail
  - getParent
```
IExecutionNode<?> getParent()
```
    Returns the parent IExecutionNode or null if the current node is the root.
    
    Returns:
    
    The parent IExecutionNode or null on root.
  - getChildren
```
IExecutionNode<?>[] getChildren()
```
    Returns the available children.
    
    Returns:
    
    The available children.
  - isPathConditionChanged
```
boolean isPathConditionChanged()
```
    Checks if this node has changed the path condition of the parent.
    
    Returns:
    
    true has different path condition compared to its parent, false has same path condition as parent.
  - getPathCondition
```
Term getPathCondition()
               throws ProofInputException
```
    Returns the path condition to reach this node as Term.
    
    Returns:
    
    The path condition to reach this node as Term.
    
    Throws:
    
    ProofInputException
  - getFormatedPathCondition
```
java.lang.String getFormatedPathCondition()
                                   throws ProofInputException
```
    Returns the human readable path condition to reach this node as string.
    
    Returns:
    
    The human readable path condition as string.
    
    Throws:
    
    ProofInputException
  - getCallStack
```
IExecutionNode<?>[] getCallStack()
```
    Returns the method call stack.
    
    Returns:
    
    The method call stack.
  - getConstraints
```
IExecutionConstraint[] getConstraints()
```
    Returns all available IExecutionConstraints.
    
    Returns:
    
    The available IExecutionConstraints.
  - getActiveStatement
```
S getActiveStatement()
```
    Returns the active statement which is executed in the code.
    
    Returns:
    
    The active statement which is executed in the code.
  - getActivePositionInfo
```
PositionInfo getActivePositionInfo()
```
    Returns the PositionInfo of getActiveStatement().
    
    Returns:
    
    The PositionInfo of getActiveStatement().
  - getVariables
```
IExecutionVariable[] getVariables()
                           throws ProofInputException
```
    Returns the variable value pairs of the current state.
    
    Returns:
    
    The variable value pairs.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - getVariables
```
IExecutionVariable[] getVariables(Term condition)
                           throws ProofInputException
```
    Returns the variable value pairs of the current state under the given condition.
    
    Parameters:
    
    condition - A Term specifying some additional constraints to consider.
    
    Returns:
    
    The variable value pairs.
    
    Throws:
    
    ProofInputException
  - getLayoutsCount
```
int getLayoutsCount()
             throws ProofInputException
```
    Returns the number of memory layouts.
    
    Returns:
    
    The number of memory layouts.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - getLayoutsEquivalenceClasses
```
ImmutableList<ISymbolicEquivalenceClass> getLayoutsEquivalenceClasses(int layoutIndex)
                                                               throws ProofInputException
```
    Returns the equivalence classes of the memory layout with the given index.
    
    Parameters:
    
    layoutIndex - The index of the memory layout.
    
    Returns:
    
    The equivalence classes of the memory layout at the given index.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - getInitialLayout
```
ISymbolicLayout getInitialLayout(int layoutIndex)
                          throws ProofInputException
```
    Returns the initial memory layout before the method was executed.
    
    Parameters:
    
    layoutIndex - The index of the memory layout.
    
    Returns:
    
    The initial memory layout at the given index.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - getCurrentLayout
```
ISymbolicLayout getCurrentLayout(int layoutIndex)
                          throws ProofInputException
```
    Returns the current memory layout which shows the memory structure before the current node in the symbolic execution tree is executed.
    
    Parameters:
    
    layoutIndex - The index of the memory layout.
    
    Returns:
    
    The current memory layout at the given index.
    
    Throws:
    
    ProofInputException - Occurred Exception.
  - getCompletedBlocks
```
ImmutableList<IExecutionBlockStartNode<?>> getCompletedBlocks()
```
    Returns all code blocks completed by this IExecutionBlockStartNode.
    
    Returns:
    
    All code blocks completed by this IExecutionBlockStartNode.
  - getBlockCompletionCondition
```
Term getBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode)
                          throws ProofInputException
```
    Returns the condition under which this node completes the code block of the given IExecutionBlockStartNode.
    
    Parameters:
    
    completedNode - The completed IExecutionBlockStartNode for which the condition is requested.
    
    Returns:
    
    The condition under which this node completes the code block of the given IExecutionBlockStartNode.
    
    Throws:
    
    ProofInputException
  - getFormatedBlockCompletionCondition
```
java.lang.String getFormatedBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode)
                                              throws ProofInputException
```
    Returns the human readable condition under which this node completes the code block of the given IExecutionBlockStartNode.
    
    Parameters:
    
    completedNode - The completed IExecutionBlockStartNode for which the condition is requested.
    
    Returns:
    
    The human readable condition under which this node completes the code block of the given IExecutionBlockStartNode.
    
    Throws:
    
    ProofInputException
  - getOutgoingLink
```
IExecutionLink getOutgoingLink(IExecutionNode<?> target)
```
    Returns the outgoing IExecutionLink.
    
    Parameters:
    
    target - The target IExecutionNode.
    
    Returns:
    
    The found IExecutionLink or null if such a link is not available.
  - getOutgoingLinks
```
ImmutableList<IExecutionLink> getOutgoingLinks()
```
    Returns all available outgoing links.
    
    Returns:
    
    The available outgoing links.
  - getIncomingLink
```
IExecutionLink getIncomingLink(IExecutionNode<?> source)
```
    Returns the incoming IExecutionLink.
    
    Parameters:
    
    source - The source IExecutionNode.
    
    Returns:
    
    The found IExecutionLink or null if such a link is not available.
  - getIncomingLinks
```
ImmutableList<IExecutionLink> getIncomingLinks()
```
    Returns all available incoming links.
    
    Returns:
    
    The available incoming links.

Interface IExecutionNode<S extends SourceElement>

Field Summary

Method Summary

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

Field Detail

INTERNAL_NODE_NAME_START

INTERNAL_NODE_NAME_END

Method Detail

getParent

getChildren

isPathConditionChanged

getPathCondition

getFormatedPathCondition

getCallStack

getConstraints

getActiveStatement

getActivePositionInfo

getVariables

getVariables

getLayoutsCount

getLayoutsEquivalenceClasses

getInitialLayout

getCurrentLayout

getCompletedBlocks

getBlockCompletionCondition

getFormatedBlockCompletionCondition

getOutgoingLink

getOutgoingLinks

getIncomingLink

getIncomingLinks