Package proguard.analysis.cpa.interfaces

Interface Summary

Interface	Description
AbortOperator	The AbortOperator defines whether the analysis should terminate upon encountering a specific abstract state.
AbstractDomain	The AbstractDomain defines a semilattice over AbstractStates.
AbstractState	An AbstractState contains information about the program state.
Algorithm	This interface wraps the main CPA algorithm parametrized by the ReachedSet, the Waitlist, and the AbortOperator.
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	ConfigurableProgramAnalysis consists of AbstractDomain, TransferRelation, MergeOperator, StopOperator, and PrecisionAdjustment.
MergeOperator	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 Algorithm.
PrecisionAdjustment	PrecisionAdjustment allows adjusting the Algorithm Precision based of the reached abstract states.
ProgramLocationDependent<CfaNodeT extends CfaNode<CfaEdgeT,SignatureT>,CfaEdgeT extends CfaEdge<CfaNodeT>,SignatureT extends Signature>	If an AbstractState is program location-specific, it should implement ProgramLocationDependent.
ProgramLocationDependentBackwardTransferRelation<CfaNodeT extends CfaNode<CfaEdgeT,SignatureT>,CfaEdgeT extends CfaEdge<CfaNodeT>,SignatureT extends Signature>	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<CfaNodeT extends CfaNode<CfaEdgeT,SignatureT>,CfaEdgeT extends CfaEdge<CfaNodeT>,SignatureT extends Signature>	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<CfaNodeT extends CfaNode<CfaEdgeT,SignatureT>,CfaEdgeT extends CfaEdge<CfaNodeT>,SignatureT extends Signature>	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	The ReachedSet stores reached States discovered by the Algorithm.
StopOperator	The StopOperator decides if Algorithm should stop.
TransferRelation	The TransferRelation computes the successor AbstractStates for the Algorithm.
Waitlist	The Waitlist stores the AbstractStates the Algorithm needs to process.
WrapperTransferRelation	This TransferRelation wraps other TransferRelations.