接口 ConfigurableProgramAnalysis<StateT extends AbstractState<StateT>>
-
- 类型参数:
StateT- The type of the analyzed states.
- 所有已知实现类:
BamCpa,CpaWithBamOperators,JvmMemoryLocationCpa,JvmTaintCpa,SimpleCpa
public interface ConfigurableProgramAnalysis<StateT extends AbstractState<StateT>>ConfigurableProgramAnalysisconsists of aTransferRelation,MergeOperator,StopOperator, andPrecisionAdjustment.The
TransferRelationspecifies how successor states are computed in theCpaAlgorithm.The
MergeOperatordefines how (and whether) the olderAbstractStateshould be updated with the newly discoveredAbstractState.The
StopOperatordecides whether the successor state should be added to theReachedSetbased on the content of the latter.The
PrecisionAdjustmentselects thePrecisionfor the currently processedAbstractStateconsidering theReachedSetcontent.All CPA components should be side effect free, i.e., not modify their arguments.
-
-
方法概要
所有方法 实例方法 抽象方法 修饰符和类型 方法 说明 @NotNull AbortOperatorgetAbortOperator()@NotNull MergeOperator<StateT>getMergeOperator()Returns the merge operator of this CPA.@NotNull PrecisionAdjustmentgetPrecisionAdjustment()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.
-
-
-
方法详细资料
-
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()
-
-