| Interface | Description |
|---|---|
| MapAbstractState<KeyT,AbstractSpaceT extends AbstractState<AbstractSpaceT>> |
| Class | Description |
|---|---|
| AbstractWaitlist<StateT extends AbstractState<StateT>> |
This is a base class for
Waitlists parametrized by the carrier CollectionT. |
| BreadthFirstWaitlist<StateT extends AbstractState<StateT>> | |
| Cfa<CfaNodeT extends CfaNode<CfaEdgeT,SignatureT>,CfaEdgeT extends CfaEdge<CfaNodeT>,SignatureT extends Signature> | |
| ControllableAbortOperator |
This
AbortOperator allows changing its behavior by setting the boolean field ControllableAbortOperator.abort to the desired output. |
| DefaultReachedSet<StateT extends AbstractState<StateT>> |
This is a
LinkedHashSet-based implementation of the ReachedSet. |
| DepthFirstWaitlist<StateT extends AbstractState<StateT>> | |
| HashMapAbstractState<KeyT,AbstractSpaceT extends AbstractState<AbstractSpaceT>> |
This
HashMapAbstractState represents a map to AbstractStates with the semilattice
operators lifted to the map. |
| ListAbstractState<AbstractSpaceT extends AbstractState<AbstractSpaceT>> |
This
ListAbstractState represents a list of AbstractStates with the semilattice operators lifted to the
list. |
| MergeJoinOperator<StateT extends AbstractState<StateT>> |
This
MergeOperator applies the join operator to its arguments. |
| MergeSepOperator<StateT extends AbstractState<StateT>> |
This
MergeOperator does not weaken the input AbstractState. |
| NeverAbortOperator |
This
AbortOperator never terminates the analysis prematurely. |
| PrecisionAdjustmentResult<StateT extends AbstractState<StateT>> | |
| ProgramLocationDependentReachedSet<StateT extends AbstractState<StateT> & ProgramLocationDependent> | |
| SetAbstractState<T> |
This
SetAbstractState represents a set with the subset ordering. |
| SimpleCpa<StateT extends AbstractState<StateT>> |
The
SimpleCpa is a ConfigurableProgramAnalysis wrapping its components. |
| StackAbstractState<AbstractSpaceT extends AbstractState<AbstractSpaceT>> |
This
StackAbstractState represents a stack of AbstractStates with the semilattice
operators lifted to the stack. |
| StaticPrecisionAdjustment |
This
PrecisionAdjustment keeps the Precision the same. |
| StopAlwaysOperator<StateT extends AbstractState<StateT>> |
This
StopOperator always returns true, i.e., it can be used for a single pass of the
analysis. |
| StopContainedOperator<StateT extends AbstractState<StateT>> |
This
StopOperator returns true if the reached set contains the input AbstractState. |
| StopJoinOperator<StateT extends AbstractState<StateT>> |
This
StopOperator returns true if the input state is less or equal than join over the
reached set. |
| StopNeverOperator<StateT extends AbstractState<StateT>> |
This
StopOperator always returns false, i.e., it can be used for analyses running until
the Waitlist becomes empty. |
| StopSepOperator<StateT extends AbstractState<StateT>> |
This
StopOperator returns true if there is a state in the reached set covering the input
AbstractState. |