proguard.analysis.cpa.defaults

Class SimpleCpa

java.lang.Object

proguard.analysis.cpa.defaults.SimpleCpa

All Implemented Interfaces:

ConfigurableProgramAnalysis

Direct Known Subclasses:

CpaWithBamOperators, JvmMemoryLocationCpa, JvmTaintCpa

public class SimpleCpa
extends java.lang.Object
implements ConfigurableProgramAnalysis

The SimpleCpa is a ConfigurableProgramAnalysis wrapping its components.

Constructor Summary

Constructors

Constructor and Description
SimpleCpa(AbstractDomain abstractDomain, TransferRelation transferRelation, MergeOperator mergeOperator, StopOperator stopOperator) Create a simple CPA with a static precision adjustment.
SimpleCpa(AbstractDomain abstractDomain, TransferRelation transferRelation, MergeOperator mergeOperator, StopOperator stopOperator, PrecisionAdjustment precisionAdjustment) Create a simple CPA from ConfigurableProgramAnalysis components.

Method Summary

Modifier and Type	Method and Description
AbstractDomain	getAbstractDomain() Returns the abstract domain of this CPA.
MergeOperator	getMergeOperator() Returns the merge operator of this CPA.
PrecisionAdjustment	getPrecisionAdjustment() Returns the precision adjustment of this CPA.
StopOperator	getStopOperator() Returns the stop operator of this CPA.
TransferRelation	getTransferRelation() Returns the transfer relation of this CPA.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

SimpleCpa

public SimpleCpa(AbstractDomain abstractDomain,
                 TransferRelation transferRelation,
                 MergeOperator mergeOperator,
                 StopOperator stopOperator)

Create a simple CPA with a static precision adjustment.

Parameters:

abstractDomain - a join-semilattice of AbstractStates defining the abstraction level of the analysis

transferRelation - a transfer relation specifying how successor states are computed

mergeOperator - a merge operator defining how (and whether) the older AbstractState should be updated with the newly discovered AbstractState

stopOperator - a stop operator deciding whether the successor state should be added to the ReachedSet based on the content of the latter

SimpleCpa

public SimpleCpa(AbstractDomain abstractDomain,
                 TransferRelation transferRelation,
                 MergeOperator mergeOperator,
                 StopOperator stopOperator,
                 PrecisionAdjustment precisionAdjustment)

Create a simple CPA from ConfigurableProgramAnalysis components.

Parameters:

abstractDomain - a join-semilattice of AbstractStates defining the abstraction level of the analysis

transferRelation - a transfer relation specifying how successor states are computed

mergeOperator - a merge operator defining how (and whether) the older AbstractState should be updated with the newly discovered AbstractState

stopOperator - a stop operator deciding whether the successor state should be added to the ReachedSet based on the content of the latter

precisionAdjustment - a precision adjustment selecting the Precision for the currently processed AbstractState considering the ReachedSet content

Method Detail

getAbstractDomain

public AbstractDomain getAbstractDomain()

Description copied from interface: ConfigurableProgramAnalysis

Returns the abstract domain of this CPA.

Specified by:

getAbstractDomain in interface ConfigurableProgramAnalysis

getTransferRelation

public TransferRelation getTransferRelation()

Description copied from interface: ConfigurableProgramAnalysis

Returns the transfer relation of this CPA.

Specified by:

getTransferRelation in interface ConfigurableProgramAnalysis

getMergeOperator

public MergeOperator getMergeOperator()

Description copied from interface: ConfigurableProgramAnalysis

Returns the merge operator of this CPA.

Specified by:

getMergeOperator in interface ConfigurableProgramAnalysis

getStopOperator

public StopOperator getStopOperator()

Description copied from interface: ConfigurableProgramAnalysis

Returns the stop operator of this CPA.

Specified by:

getStopOperator in interface ConfigurableProgramAnalysis

getPrecisionAdjustment

public PrecisionAdjustment getPrecisionAdjustment()

Description copied from interface: ConfigurableProgramAnalysis

Returns the precision adjustment of this CPA.

Specified by:

getPrecisionAdjustment in interface ConfigurableProgramAnalysis