proguard.analysis.cpa.defaults

Class SimpleCpa<StateT extends AbstractState<StateT>>

java.lang.Object

proguard.analysis.cpa.defaults.SimpleCpa<StateT>

Type Parameters:

StateT - The type of the analyzed states.

All Implemented Interfaces:

ConfigurableProgramAnalysis<StateT>

Direct Known Subclasses:

CpaWithBamOperators, JvmMemoryLocationCpa, JvmTaintCpa

public class SimpleCpa<StateT extends AbstractState<StateT>>
extends java.lang.Object
implements ConfigurableProgramAnalysis<StateT>

The SimpleCpa is a ConfigurableProgramAnalysis wrapping its components.

Constructor Summary

Constructors

Constructor and Description
SimpleCpa(TransferRelation<StateT> transferRelation, MergeOperator<StateT> mergeOperator, StopOperator<StateT> stopOperator) Create a simple CPA with a static precision adjustment.
SimpleCpa(TransferRelation<StateT> transferRelation, MergeOperator<StateT> mergeOperator, StopOperator<StateT> stopOperator, PrecisionAdjustment precisionAdjustment, AbortOperator abortOperator) Create a simple CPA from ConfigurableProgramAnalysis components.

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.

Methods inherited from class java.lang.Object

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

Constructor Detail

SimpleCpa

public SimpleCpa(TransferRelation<StateT> transferRelation,
                 MergeOperator<StateT> mergeOperator,
                 StopOperator<StateT> 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(TransferRelation<StateT> transferRelation,
                 MergeOperator<StateT> mergeOperator,
                 StopOperator<StateT> stopOperator,
                 PrecisionAdjustment precisionAdjustment,
                 AbortOperator abortOperator)

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

abortOperator - an operator used to terminate the analysis prematurely.

Method Detail

getTransferRelation

@NotNull
public @NotNull TransferRelation<StateT> getTransferRelation()

Description copied from interface: ConfigurableProgramAnalysis

Returns the transfer relation of this CPA.

Specified by:

getTransferRelation in interface ConfigurableProgramAnalysis<StateT extends AbstractState<StateT>>

getMergeOperator

@NotNull
public @NotNull MergeOperator<StateT> getMergeOperator()

Description copied from interface: ConfigurableProgramAnalysis

Returns the merge operator of this CPA.

Specified by:

getMergeOperator in interface ConfigurableProgramAnalysis<StateT extends AbstractState<StateT>>

getStopOperator

@NotNull
public @NotNull StopOperator<StateT> getStopOperator()

Description copied from interface: ConfigurableProgramAnalysis

Returns the stop operator of this CPA.

Specified by:

getStopOperator in interface ConfigurableProgramAnalysis<StateT extends AbstractState<StateT>>

getPrecisionAdjustment

@NotNull
public @NotNull PrecisionAdjustment getPrecisionAdjustment()

Description copied from interface: ConfigurableProgramAnalysis

Returns the precision adjustment of this CPA.

Specified by:

getPrecisionAdjustment in interface ConfigurableProgramAnalysis<StateT extends AbstractState<StateT>>

getAbortOperator

@NotNull
public @NotNull AbortOperator getAbortOperator()

Specified by:

getAbortOperator in interface ConfigurableProgramAnalysis<StateT extends AbstractState<StateT>>