接口 ConfigurableProgramAnalysis<StateT extends AbstractState<StateT>>
- 类型参数:
StateT- The type of the analyzed states.
- 所有已知实现类:
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.
-
方法概要
修饰符和类型方法说明@NotNull AbortOperator@NotNull MergeOperator<StateT>Returns the merge operator of this CPA.@NotNull PrecisionAdjustmentReturns the precision adjustment of this CPA.@NotNull StopOperator<StateT>Returns the stop operator of this CPA.@NotNull TransferRelation<StateT>Returns the transfer relation of this CPA.
-
方法详细资料
-
getTransferRelation
Returns the transfer relation of this CPA. -
getMergeOperator
Returns the merge operator of this CPA. -
getStopOperator
Returns the stop operator of this CPA. -
getPrecisionAdjustment
Returns the precision adjustment of this CPA. -
getAbortOperator
-