public abstract class BamCpaRun<CpaT extends ConfigurableProgramAnalysis,AbstractStateT extends AbstractState,CfaNodeT extends CfaNode<CfaEdgeT,SignatureT>,CfaEdgeT extends CfaEdge<CfaNodeT>,SignatureT extends Signature> extends CpaRun<BamCpa<CfaNodeT,CfaEdgeT,SignatureT>,AbstractStateT>
CpaWithBamOperators
based on the intraprocedural
ConfigurableProgramAnalysis
, runs it, and returns the ReachedSet
.Modifier and Type | Class and Description |
---|---|
static class |
BamCpaRun.Builder
A builder for
BamCpaRun . |
Modifier and Type | Field and Description |
---|---|
protected boolean |
reduceHeap |
abortOperator, cpa
Modifier | Constructor and Description |
---|---|
protected |
BamCpaRun(AbortOperator abortOperator,
int maxCallStackDepth)
Create a BAM CPA run.
|
protected |
BamCpaRun(AbortOperator abortOperator,
int maxCallStackDepth,
boolean reduceHeap)
Create a BAM CPA run.
|
Modifier and Type | Method and Description |
---|---|
BamCache<SignatureT> |
createCache()
Returns a fresh BAM cache.
|
abstract ExpandOperator<CfaNodeT,CfaEdgeT,SignatureT> |
createExpandOperator()
Returns the expand operator.
|
abstract CpaT |
createIntraproceduralCPA()
Returns the intraprocedural CPA.
|
RebuildOperator |
createRebuildOperator()
Returns the rebuild operator.
|
abstract ReduceOperator<CfaNodeT,CfaEdgeT,SignatureT> |
createReduceOperator()
Returns the reduce operator.
|
java.util.Set<SignatureT> |
getAnalyzedMethods() |
abstract Cfa<CfaNodeT,CfaEdgeT,SignatureT> |
getCfa()
Returns the CFA.
|
BamCpa<CfaNodeT,CfaEdgeT,SignatureT> |
getCpa()
Returns the CPA.
|
abstract SignatureT |
getMainSignature()
Returns the signature of the main procedure.
|
int |
getMaxCallStackDepth()
Returns the maximal call stack depth.
|
createReachedSet, createWaitlist, execute, getAbortOperator, getInitialStates
protected BamCpaRun(AbortOperator abortOperator, int maxCallStackDepth)
abortOperator
- an abort operatormaxCallStackDepth
- the maximum depth of the call stack analyzed interprocedurally 0 means
intraprocedural analysis < 0 means no maximum depthprotected BamCpaRun(AbortOperator abortOperator, int maxCallStackDepth, boolean reduceHeap)
abortOperator
- an abort operatormaxCallStackDepth
- the maximum depth of the call stack analyzed interprocedurally 0 means
intraprocedural analysis < 0 means no maximum depthreduceHeap
- whether reduction/expansion of the heap state is performed at call/return
sitespublic BamCpa<CfaNodeT,CfaEdgeT,SignatureT> getCpa()
CpaRun
getCpa
in class CpaRun<BamCpa<CfaNodeT extends CfaNode<CfaEdgeT,SignatureT>,CfaEdgeT extends CfaEdge<CfaNodeT>,SignatureT extends Signature>,AbstractStateT extends AbstractState>
public abstract CpaT createIntraproceduralCPA()
public abstract ReduceOperator<CfaNodeT,CfaEdgeT,SignatureT> createReduceOperator()
public abstract ExpandOperator<CfaNodeT,CfaEdgeT,SignatureT> createExpandOperator()
public RebuildOperator createRebuildOperator()
public BamCache<SignatureT> createCache()
public abstract Cfa<CfaNodeT,CfaEdgeT,SignatureT> getCfa()
public abstract SignatureT getMainSignature()
public int getMaxCallStackDepth()
public java.util.Set<SignatureT> getAnalyzedMethods()