|Constructor and Description|
Create an algorithm to run the specified CPA.
Create a CPA algorithm from CPA components.
|Modifier and Type||Method and Description|
Algorithm from the paper is parametrized with the reached set and the waitlist.
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
public CpaAlgorithm(ConfigurableProgramAnalysis cpa)
cpa- a CPA instance wrapping the transfer relation, the merge, and the stop operator, and the precision adjustment
public CpaAlgorithm(TransferRelation transferRelation, MergeOperator mergeOperator, StopOperator stopOperator, PrecisionAdjustment precisionAdjustment)
transferRelation- a transfer relation specifying how successor states are computed
mergeOperator- a merge operator defining how (and whether) the older
AbstractStateshould be updated with the newly discovered
stopOperator- a stop operator deciding whether the successor state should be added to the
ReachedSetbased on the content of the latter
precisionAdjustment- a precision adjustment selecting the
Precisionfor the currently processed
public void run(ReachedSet reachedSet, Waitlist waitlist, AbortOperator abortOperator)
abortOperatordetermines whether the analysis should end prematurely.