proguard.analysis.cpa.defaults

Class SequentialCpaRun<CpaT extends ConfigurableProgramAnalysis,AbstractStateT extends AbstractState,InputCpaRunT extends CpaRun>

java.lang.Object

proguard.analysis.cpa.defaults.CpaRun<CpaT,AbstractStateT>

proguard.analysis.cpa.defaults.SequentialCpaRun<CpaT,AbstractStateT,InputCpaRunT>

Direct Known Subclasses:

JvmMemoryLocationBamCpaRun

public abstract class SequentialCpaRun<CpaT extends ConfigurableProgramAnalysis,AbstractStateT extends AbstractState,InputCpaRunT extends CpaRun>
extends CpaRun<CpaT,AbstractStateT>

This CpaRun wraps another InputCpaRunT and allows a following CpaT to be constructed using the output of the former run.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static interface	SequentialCpaRun.PreviousRunDurationReceiver Interface that can be implemented by the abort operator of the second CPA.

Field Summary

Fields

Modifier and Type	Field and Description
protected InputCpaRunT	inputCpaRun
protected ReachedSet	inputReachedSet
protected ReachedSet	outputReachedSet

Fields inherited from class proguard.analysis.cpa.defaults.CpaRun

abortOperator, cpa

Constructor Summary

Constructors

Constructor and Description
SequentialCpaRun(InputCpaRunT inputCpaRun) Create a CPA run which accepts the reached set of another CPA run.

Method Summary

Modifier and Type	Method and Description
ReachedSet	execute() Sets up the CpaAlgorithm, runs it, and returns the ReachedSet with the result of the analysis.
InputCpaRunT	getInputCpaRun()
ReachedSet	getOutputReachedSet()

Methods inherited from class proguard.analysis.cpa.defaults.CpaRun

createReachedSet, createWaitlist, getAbortOperator, getCpa, getInitialStates

Methods inherited from class java.lang.Object

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

Field Detail

inputCpaRun

protected final InputCpaRunT extends CpaRun inputCpaRun

inputReachedSet

protected ReachedSet inputReachedSet

outputReachedSet

protected ReachedSet outputReachedSet

Constructor Detail

SequentialCpaRun

public SequentialCpaRun(InputCpaRunT inputCpaRun)

Create a CPA run which accepts the reached set of another CPA run.

Parameters:

inputCpaRun - the inner CPA run

Method Detail

execute

public ReachedSet execute()

Description copied from class: CpaRun

Sets up the CpaAlgorithm, runs it, and returns the ReachedSet with the result of the analysis.

Overrides:

execute in class CpaRun<CpaT extends ConfigurableProgramAnalysis,AbstractStateT extends AbstractState>

getOutputReachedSet

public ReachedSet getOutputReachedSet()

getInputCpaRun

public InputCpaRunT getInputCpaRun()