Modifier and Type | Class and Description |
---|---|
static class |
ExecutionNodeReader.AbstractKeYlessBaseExecutionNode<S extends SourceElement>
An implementation of
IExecutionBaseMethodReturn which is independent
from KeY and provides such only children and default attributes. |
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.AbstractKeYlessExecutionElement
An abstract implementation of
IExecutionElement which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.AbstractKeYlessExecutionNode<S extends SourceElement>
An abstract implementation of
IExecutionNode which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessBlockContract
An implementation of
IExecutionAuxiliaryContract which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessBranchCondition
An implementation of
IExecutionLoopCondition 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.KeYlessConstraint
An implementation of
IExecutionConstraint which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessExceptionalMethodReturn
An implementation of
IExecutionExceptionalMethodReturn which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessJoin
An implementation of
IExecutionJoin 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.KeYlessLoopInvariant
An implementation of
IExecutionLoopInvariant 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. |
static class |
ExecutionNodeReader.KeYlessMethodCall
An implementation of
IExecutionMethodCall which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessMethodReturn
An implementation of
IExecutionMethodReturn which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessMethodReturnValue
An implementation of
IExecutionMethodReturn which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessOperationContract
An implementation of
IExecutionOperationContract which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessStart
An implementation of
IExecutionStart which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessStatement
An implementation of
IExecutionStatement which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessTermination
An implementation of
IExecutionTermination which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessValue
An implementation of
IExecutionValue which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessVariable
An implementation of
IExecutionVariable which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionVariableExtractor.ExtractedExecutionValue
The
IExecutionValue instantiated by the ExecutionVariableExtractor . |
static class |
ExecutionVariableExtractor.ExtractedExecutionVariable
The
IExecutionVariable instantiated by the ExecutionVariableExtractor . |
Modifier and Type | Interface and Description |
---|---|
interface |
IExecutionAuxiliaryContract
A node in the symbolic execution tree which represents a use block/loop contract application.
|
interface |
IExecutionBaseMethodReturn<S extends SourceElement>
Defines the common interface of
IExecutionMethodReturn
and IExecutionExceptionalMethodReturn . |
interface |
IExecutionBlockStartNode<S extends SourceElement>
An extended
IExecutionNode which groups several child nodes. |
interface |
IExecutionBranchCondition
A node in the symbolic execution tree which represents a branch condition,
e.g.
|
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 |
IExecutionConstraint
A constrained considered during symbolic execution.
|
interface |
IExecutionExceptionalMethodReturn
A node in the symbolic execution tree which represents a exceptional method return.
|
interface |
IExecutionJoin
A node in the symbolic execution tree which represents a join.
|
interface |
IExecutionLoopCondition
A node in the symbolic execution tree which represents a loop condition,
e.g.
|
interface |
IExecutionLoopInvariant
A node in the symbolic execution tree which represents a loop invariant application.
|
interface |
IExecutionLoopStatement
A node in the symbolic execution tree which represents a loop.
|
interface |
IExecutionMethodCall
A node in the symbolic execution tree which represents a method call,
e.g.
|
interface |
IExecutionMethodReturn
A node in the symbolic execution tree which represents a method return,
e.g.
|
interface |
IExecutionMethodReturnValue
A return value of an
IExecutionMethodReturn . |
interface |
IExecutionNode<S extends SourceElement>
Provides the basic methods each node in a symbolic execution tree
should have and allows to access the children.
|
interface |
IExecutionOperationContract
A node in the symbolic execution tree which represents a use operation contract application.
|
interface |
IExecutionStart
The start node of a symbolic execution tree.
|
interface |
IExecutionStatement
A node in the symbolic execution tree which represents a single statement,
e.g.
|
interface |
IExecutionTermination
A node in the symbolic execution tree which represents the normal termination of a branch,
e.g.
|
interface |
IExecutionValue
A value of an
IExecutionVariable , e.g. |
interface |
IExecutionVariable
A variable value pair contained in an
IExecutionNode , e.g. |
Modifier and Type | Method and Description |
---|---|
static ImmutableList<Goal> |
SymbolicExecutionUtil.collectGoalsInSubtree(IExecutionElement executionElement)
Collects all
Goal s in the subtree of the given IExecutionElement . |
static NotationInfo |
SymbolicExecutionUtil.createNotationInfo(IExecutionElement element)
Creates the
NotationInfo for the given IExecutionElement . |
Copyright © 2003-2019 The KeY-Project.