Class | Description |
---|---|
AbstractCallStackBasedStopCondition |
Provides the basic functionality for
StopCondition s 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 . |