Package | Description |
---|---|
de.uka.ilkd.key.symbolic_execution | |
de.uka.ilkd.key.symbolic_execution.model | |
de.uka.ilkd.key.symbolic_execution.model.impl |
Modifier and Type | Class and Description |
---|---|
static class |
ExecutionNodeReader.AbstractKeYlessExecutionBlockStartNode<S extends SourceElement>
An abstract implementation of
IExecutionBlockStartNode which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessBranchStatement
An implementation of
IExecutionBranchStatement which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessLoopCondition
An implementation of
IExecutionLoopCondition which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessLoopStatement
An implementation of
IExecutionLoopStatement which is independent
from KeY and provides such only children and default attributes. |
Modifier and Type | Method and Description |
---|---|
ImmutableList<IExecutionBlockStartNode<?>> |
ExecutionNodeReader.AbstractKeYlessExecutionNode.getCompletedBlocks()
Returns all code blocks completed by this
IExecutionBlockStartNode . |
Modifier and Type | Method and Description |
---|---|
void |
ExecutionNodeReader.AbstractKeYlessExecutionNode.addCompletedBlock(IExecutionBlockStartNode<?> completedBlock,
java.lang.String formatedCondition)
Adds the given completed block.
|
protected void |
ExecutionNodeWriter.appendBlockCompletions(int level,
IExecutionBlockStartNode<?> node,
java.lang.StringBuffer sb)
Appends the block completion entries to the given
StringBuffer . |
Term |
ExecutionNodeReader.AbstractKeYlessExecutionNode.getBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode)
Returns the condition under which this node completes the code block of the given
IExecutionBlockStartNode . |
java.lang.String |
ExecutionNodeReader.AbstractKeYlessExecutionNode.getFormatedBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode)
Returns the human readable condition under which this node completes the code block of the given
IExecutionBlockStartNode . |
Modifier and Type | Interface and Description |
---|---|
interface |
IExecutionBranchStatement
A node in the symbolic execution tree which represents a node which
creates multiple child branches defined by branch conditions (
ISEDBranchCondition ),
e.g. |
interface |
IExecutionLoopCondition
A node in the symbolic execution tree which represents a loop condition,
e.g.
|
interface |
IExecutionLoopStatement
A node in the symbolic execution tree which represents a loop.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<IExecutionBlockStartNode<?>> |
IExecutionNode.getCompletedBlocks()
Returns all code blocks completed by this
IExecutionBlockStartNode . |
Modifier and Type | Method and Description |
---|---|
Term |
IExecutionNode.getBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode)
Returns the condition under which this node completes the code block of the given
IExecutionBlockStartNode . |
java.lang.String |
IExecutionNode.getFormatedBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode)
Returns the human readable condition under which this node completes the code block of the given
IExecutionBlockStartNode . |
Modifier and Type | Class and Description |
---|---|
class |
AbstractExecutionBlockStartNode<S extends SourceElement>
Provides a basic implementation of
IExecutionBlockStartNode . |
class |
ExecutionBranchStatement
The default implementation of
IExecutionBranchStatement . |
class |
ExecutionLoopCondition
The default implementation of
IExecutionLoopCondition . |
class |
ExecutionLoopStatement
The default implementation of
IExecutionLoopStatement . |
Modifier and Type | Method and Description |
---|---|
ImmutableList<IExecutionBlockStartNode<?>> |
AbstractExecutionNode.getCompletedBlocks()
Returns all code blocks completed by this
IExecutionBlockStartNode . |
Modifier and Type | Method and Description |
---|---|
void |
AbstractExecutionNode.addCompletedBlock(IExecutionBlockStartNode<?> completedBlock)
Registers the given
IExecutionBlockStartNode . |
Term |
AbstractExecutionNode.getBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode)
Returns the condition under which this node completes the code block of the given
IExecutionBlockStartNode . |
java.lang.String |
AbstractExecutionNode.getFormatedBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode)
Returns the human readable condition under which this node completes the code block of the given
IExecutionBlockStartNode . |
protected java.lang.Object |
AbstractExecutionNode.lazyComputeBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode,
boolean returnFormatedCondition)
Computes the condition lazily when
#getBlockCompletionCondition(IExecutionNode)
or #getFormatedBlockCompletionCondition(IExecutionNode) is called the first time. |
void |
AbstractExecutionNode.removeCompletedBlock(IExecutionBlockStartNode<?> completedBlock)
Removes the given
IExecutionBlockStartNode from registration. |
Copyright © 2003-2019 The KeY-Project.