| Interface | Description |
|---|---|
| AbortOperator |
The
AbortOperator defines whether the analysis should terminate upon encountering a
specific abstract state. |
| AbstractState<StateT extends AbstractState<StateT>> |
An
AbstractState contains information about the program state. |
| CallEdge |
This interface must be implemented by edges representing a procedure call.
|
| CfaEdge<CfaNodeT extends CfaNode> |
An edge for
Cfa parametrized by its nodes CfaNodeT. |
| CfaNode<CfaEdgeT extends CfaEdge,SignatureT extends Signature> |
A node for
Cfa parametrized by its edges CfaEdgeT. |
| ConfigurableProgramAnalysis<StateT extends AbstractState<StateT>> |
ConfigurableProgramAnalysis consists of a TransferRelation, MergeOperator, StopOperator, and PrecisionAdjustment. |
| MergeOperator<StateT extends AbstractState<StateT>> |
The
MergeOperator defines how (and whether) the older AbstractState should be
updated with the newly discovered AbstractState. |
| Precision |
Precision parametrizes the analysis accuracy of the CpaAlgorithm. |
| PrecisionAdjustment |
PrecisionAdjustment allows adjusting the CpaAlgorithm Precision based of the reached abstract
states. |
| ProgramLocationDependent |
If an
AbstractState is program location-specific (i.e., is associated to a specific node
from the Cfa), it should implement ProgramLocationDependent. |
| ProgramLocationDependentBackwardTransferRelation<ContentT extends AbstractState<ContentT>> |
An interface for
TransferRelations that depend on the Cfa location for which the successor can be defined for the
entering edges of the current location. |
| ProgramLocationDependentForwardTransferRelation<ContentT extends AbstractState<ContentT>> |
An interface for
TransferRelations that depend on the Cfa location for which the successor can be defined for the
leaving edges of the current location. |
| ProgramLocationDependentTransferRelation<ContentT extends AbstractState<ContentT>> |
An interface for
TransferRelations that depend on the Cfa location for which the successor can be defined for the edges
of the current location. |
| ReachedSet<StateT extends AbstractState<StateT>> | |
| StopOperator<StateT extends AbstractState<StateT>> |
The
StopOperator decides if CpaAlgorithm should
stop. |
| TransferRelation<StateT extends AbstractState<StateT>> | |
| Waitlist<StateT extends AbstractState<StateT>> |