Class and Description |
---|
AbstractUpdateExtractor
Provides the basic functionality to extract values from updates.
|
AbstractUpdateExtractor.ExecutionVariableValuePair
Represents a location (value or association of a given object/state)
in a concrete memory layout of the initial or current state.
|
AbstractUpdateExtractor.ExtractLocationParameter
Instances of this class provides the
Term which are required
to compute a location (value or association of a given object/state). |
AbstractUpdateExtractor.NodeGoal
Utility class used by
AbstractUpdateExtractor#computeValueConditions(Set, Map) . |
AbstractWriter
Provides the basic functionality for classes like
ExecutionNodeWriter
and SymbolicLayoutWriter which encodes an object structure as XML. |
ExecutionNodeReader.AbstractKeYlessBaseExecutionNode
An implementation of
IExecutionBaseMethodReturn which is independent
from KeY and provides such only children and default attributes. |
ExecutionNodeReader.AbstractKeYlessExecutionBlockStartNode
An abstract implementation of
IExecutionBlockStartNode which is independent
from KeY and provides such only children and default attributes. |
ExecutionNodeReader.AbstractKeYlessExecutionElement
An abstract implementation of
IExecutionElement which is independent
from KeY and provides such only children and default attributes. |
ExecutionNodeReader.AbstractKeYlessExecutionNode
An abstract implementation of
IExecutionNode which is independent
from KeY and provides such only children and default attributes. |
ExecutionNodeReader.KeYlessMethodReturnValue
An implementation of
IExecutionMethodReturn which is independent
from KeY and provides such only children and default attributes. |
ExecutionNodeReader.KeYlessValue
An implementation of
IExecutionValue which is independent
from KeY and provides such only children and default attributes. |
ExecutionNodeReader.KeYlessVariable
An implementation of
IExecutionVariable which is independent
from KeY and provides such only children and default attributes. |
ExecutionVariableExtractor.ExtractedExecutionValue
The
IExecutionValue instantiated by the ExecutionVariableExtractor . |
ExecutionVariableExtractor.ExtractedExecutionVariable
The
IExecutionVariable instantiated by the ExecutionVariableExtractor . |
SymbolicExecutionTreeBuilder.JavaPair
Utility class to group a call stack size with an
ImmutableList of SourceElement with the elements of interest. |
SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions
Instances of this class are returned by
SymbolicExecutionTreeBuilder.analyse()
to inform about newly completed blocks and returned methods. |
SymbolicLayoutExtractor
Instances of this class can be used to compute memory layouts
(objects with values and associations to other objects on the heap together
with objects and associations to objects on the current state of the stack)
which a given
Node of KeY's proof tree can have based on
equivalence classes (aliasing) of objects. |
SymbolicLayoutReader.AbstractKeYlessAssociationValueContainer
An implementation of
ISymbolicAssociationValueContainer which is independent
from KeY and provides such only children and default attributes. |
SymbolicLayoutReader.AbstractKeYlessElement
An implementation of
ISymbolicElement which is independent
from KeY and provides such only children and default attributes. |
TruthValueTracingUtil.BranchResult |
TruthValueTracingUtil.MultiEvaluationResult
Instances of this unmodifyable class are used to store the found
evaluation results.
|
TruthValueTracingUtil.TruthValue
Represents the possible truth values.
|
TruthValueTracingUtil.TruthValueTracingResult
Represents the final predicate evaluation result returned by
{@link TruthValueEvaluationUtil#evaluate(Node, Name, boolean, boolean).
|
Class and Description |
---|
ExecutionNodeSymbolicLayoutExtractor
Special
SymbolicLayoutExtractor for IExecutionNode s. |
Class and Description |
---|
SymbolicExecutionTreeBuilder
Instances of this class are used to extract the symbolic execution tree
from a normal KeY's proof tree.
|
Class and Description |
---|
SymbolicExecutionTreeBuilder
Instances of this class are used to extract the symbolic execution tree
from a normal KeY's proof tree.
|
Copyright © 2003-2019 The KeY-Project.