proguard.analysis.cpa.interfaces

Interface ConfigurableProgramAnalysis<StateT extends AbstractState<StateT>>

Type Parameters:

StateT - The type of the analyzed states.

All Known Implementing Classes:

BamCpa, CpaWithBamOperators, JvmMemoryLocationCpa, JvmTaintCpa, SimpleCpa

public interface ConfigurableProgramAnalysis<StateT extends AbstractState<StateT>>

ConfigurableProgramAnalysis consists of a TransferRelation, MergeOperator, StopOperator, and PrecisionAdjustment.

The TransferRelation specifies how successor states are computed in the CpaAlgorithm.

The MergeOperator defines how (and whether) the older AbstractState should be updated with the newly discovered AbstractState.

The StopOperator decides whether the successor state should be added to the ReachedSet based on the content of the latter.

The PrecisionAdjustment selects the Precision for the currently processed AbstractState considering the ReachedSet content.

All CPA components should be side effect free, i.e., not modify their arguments.

Method Summary

Modifier and Type	Method and Description
@NotNull AbortOperator	getAbortOperator()
@NotNull MergeOperator<StateT>	getMergeOperator() Returns the merge operator of this CPA.
@NotNull PrecisionAdjustment	getPrecisionAdjustment() Returns the precision adjustment of this CPA.
@NotNull StopOperator<StateT>	getStopOperator() Returns the stop operator of this CPA.
@NotNull TransferRelation<StateT>	getTransferRelation() Returns the transfer relation of this CPA.

Method Detail

getTransferRelation

@NotNull
@NotNull TransferRelation<StateT> getTransferRelation()

Returns the transfer relation of this CPA.

getMergeOperator

@NotNull
@NotNull MergeOperator<StateT> getMergeOperator()

Returns the merge operator of this CPA.

getStopOperator

@NotNull
@NotNull StopOperator<StateT> getStopOperator()

Returns the stop operator of this CPA.

getPrecisionAdjustment

@NotNull
@NotNull PrecisionAdjustment getPrecisionAdjustment()

Returns the precision adjustment of this CPA.

getAbortOperator

@NotNull
@NotNull AbortOperator getAbortOperator()