| Class | Description |
|---|---|
| AbstractCallStackBasedStopCondition |
Provides the basic functionality for
StopConditions which stops
the auto mode when the call stack size of the starting set node has
a special difference to the call stack size of the current set node, e.g. |
| AbstractCallStackBasedStopCondition.NodeStartEntry |
Instances of this class are used in
AbstractCallStackBasedStopCondition.startingCallStackSizePerGoal
to represent the initial Node of Goal on which
the auto mode was started together with its call stack size. |
| BreakpointStopCondition |
An
IBreakpointStopCondition which can be used during proof. |
| CompoundStopCondition |
This
StopCondition contains other StopCondition as
children and stops the auto mode if at least on of its children force it. |
| CutHeapObjectsFeature |
This
BinaryFeature checks if a cut with an equality for
an alias check should be done or not. |
| CutHeapObjectsTermGenerator |
This
TermGenerator is used by the SymbolicExecutionStrategy
to add early alias checks of used objects as target of store operations
on heaps. |
| ExecutedSymbolicExecutionTreeNodesStopCondition |
This
StopCondition stops the auto mode (ApplyStrategy) if
a given number (ExecutedSymbolicExecutionTreeNodesStopCondition.getMaximalNumberOfSetNodesToExecutePerGoal()) of maximal
executed symbolic execution tree nodes is reached in a goal. |
| SimplifyTermStrategy | |
| SimplifyTermStrategy.Factory |
The
StrategyFactory to create instances of SimplifyTermStrategy. |
| StepOverSymbolicExecutionTreeNodesStopCondition |
This
StopCondition stops the auto mode when a "step over" is completed. |
| StepReturnSymbolicExecutionTreeNodesStopCondition |
This
StopCondition stops the auto mode when a "step over" is completed. |
| SymbolicExecutionBreakpointStopCondition |
An
IBreakpointStopCondition which can be used during symbolic execution. |
| SymbolicExecutionGoalChooser |
This
GoalChooser is a special implementation of the default
DepthFirstGoalChooser. |
| SymbolicExecutionGoalChooserBuilder |
This
GoalChooserBuilder creates a special GoalChooser
for symbolic execution. |
| SymbolicExecutionStrategy |
Strategy to use for symbolic execution. |
| SymbolicExecutionStrategy.Factory |
The
StrategyFactory to create instances of SymbolicExecutionStrategy. |