| Class | 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.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. |
| ExecutionNodePreorderIterator |
Iterates preorder over the whole sub tree of a given
IExecutionNode. |
| ExecutionNodeReader |
Allows to read XML files which contains an symbolic execution tree
written via an
ExecutionNodeWriter. |
| ExecutionNodeReader.AbstractKeYlessBaseExecutionNode<S extends SourceElement> |
An implementation of
IExecutionBaseMethodReturn which is independent
from KeY and provides such only children and default attributes. |
| ExecutionNodeReader.AbstractKeYlessExecutionBlockStartNode<S extends SourceElement> |
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<S extends SourceElement> |
An abstract implementation of
IExecutionNode which is independent
from KeY and provides such only children and default attributes. |
| ExecutionNodeReader.KeYlessBlockContract |
An implementation of
IExecutionAuxiliaryContract which is independent
from KeY and provides such only children and default attributes. |
| ExecutionNodeReader.KeYlessBranchCondition |
An implementation of
IExecutionLoopCondition which is independent
from KeY and provides such only children and default attributes. |
| ExecutionNodeReader.KeYlessBranchStatement |
An implementation of
IExecutionBranchStatement which is independent
from KeY and provides such only children and default attributes. |
| ExecutionNodeReader.KeYlessConstraint |
An implementation of
IExecutionConstraint which is independent
from KeY and provides such only children and default attributes. |
| ExecutionNodeReader.KeYlessExceptionalMethodReturn |
An implementation of
IExecutionExceptionalMethodReturn which is independent
from KeY and provides such only children and default attributes. |
| ExecutionNodeReader.KeYlessJoin |
An implementation of
IExecutionJoin which is independent
from KeY and provides such only children and default attributes. |
| ExecutionNodeReader.KeYLessLink |
An implementation of
IExecutionLink which is independent
from KeY and provides such only children and default attributes. |
| ExecutionNodeReader.KeYlessLoopCondition |
An implementation of
IExecutionLoopCondition which is independent
from KeY and provides such only children and default attributes. |
| ExecutionNodeReader.KeYlessLoopInvariant |
An implementation of
IExecutionLoopInvariant which is independent
from KeY and provides such only children and default attributes. |
| ExecutionNodeReader.KeYlessLoopStatement |
An implementation of
IExecutionLoopStatement which is independent
from KeY and provides such only children and default attributes. |
| ExecutionNodeReader.KeYlessMethodCall |
An implementation of
IExecutionMethodCall which is independent
from KeY and provides such only children and default attributes. |
| ExecutionNodeReader.KeYlessMethodReturn |
An implementation of
IExecutionMethodReturn 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.KeYlessOperationContract |
An implementation of
IExecutionOperationContract which is independent
from KeY and provides such only children and default attributes. |
| ExecutionNodeReader.KeYlessStart |
An implementation of
IExecutionStart which is independent
from KeY and provides such only children and default attributes. |
| ExecutionNodeReader.KeYlessStatement |
An implementation of
IExecutionStatement which is independent
from KeY and provides such only children and default attributes. |
| ExecutionNodeReader.KeYlessTermination |
An implementation of
IExecutionTermination 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. |
| ExecutionNodeSymbolicLayoutExtractor |
Special
SymbolicLayoutExtractor for IExecutionNodes. |
| ExecutionNodeWriter |
Allows to persistent selected properties of
IExecutionNodes
as XML file. |
| ExecutionVariableExtractor |
Extracts the current state and represents it as
IExecutionVariables. |
| ExecutionVariableExtractor.ExtractedExecutionValue |
The
IExecutionValue instantiated by the ExecutionVariableExtractor. |
| ExecutionVariableExtractor.ExtractedExecutionVariable |
The
IExecutionVariable instantiated by the ExecutionVariableExtractor. |
| ExecutionVariableExtractor.LocationDefinition |
Utility class representing a location.
|
| ExecutionVariableExtractor.ParentDefinition |
Utility class representing a parent definition.
|
| SymbolicExecutionTreeBuilder |
Instances of this class are used to extract the symbolic execution tree
from a normal KeY's proof tree.
|
| SymbolicExecutionTreeBuilder.JavaPair |
Utility class to group a call stack size with an
ImmutableList of SourceElement with the elements of interest. |
| SymbolicExecutionTreeBuilder.MethodFrameCounterJavaASTVisitor |
Utility class used in
SymbolicExecutionTreeBuilder.initNewLoopBodyMethodCallStack(Node)
to compute the number of available MethodFrames. |
| 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 |
Allows to read XML files which contains an object model
written via an
SymbolicLayoutWriter. |
| 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. |
| SymbolicLayoutReader.KeYlessAssociation |
An implementation of
ISymbolicAssociation which is independent
from KeY and provides such only children and default attributes. |
| SymbolicLayoutReader.KeYlessEquivalenceClass |
An implementation of
ISymbolicEquivalenceClass which is independent
from KeY and provides such only children and default attributes. |
| SymbolicLayoutReader.KeYlessLayout |
An implementation of
ISymbolicLayout which is independent
from KeY and provides such only children and default attributes. |
| SymbolicLayoutReader.KeYlessObject |
An implementation of
ISymbolicObject which is independent
from KeY and provides such only children and default attributes. |
| SymbolicLayoutReader.KeYlessState |
An implementation of
ISymbolicState which is independent
from KeY and provides such only children and default attributes. |
| SymbolicLayoutReader.KeYlessValue |
An implementation of
ISymbolicValue which is independent
from KeY and provides such only children and default attributes. |
| SymbolicLayoutWriter |
Allows to persistent selected properties of
ISymbolicLayouts
as XML file. |
| TruthValueTracingUtil |
Provides functionality to evaluate the truth value of labeled formulas
(predicates and junctors).
|
| TruthValueTracingUtil.BranchResult | |
| TruthValueTracingUtil.LabelOccurrence |
Utility class which specifies the occurrence of a
FormulaTermLabel. |
| TruthValueTracingUtil.MultiEvaluationResult |
Instances of this unmodifyable class are used to store the found
evaluation results.
|
| TruthValueTracingUtil.TruthValueTracingResult |
Represents the final predicate evaluation result returned by
{@link TruthValueEvaluationUtil#evaluate(Node, Name, boolean, boolean).
|
| Enum | Description |
|---|---|
| TruthValueTracingUtil.TruthValue |
Represents the possible truth values.
|