public abstract class JvmBamCpaRun<CpaT extends ConfigurableProgramAnalysis,AbstractStateT extends LatticeAbstractState<AbstractStateT>,OuterAbstractStateT extends AbstractState> extends BamCpaRun<CpaT,OuterAbstractStateT,JvmCfaNode,JvmCfaEdge,MethodSignature>
BamCpaRun
uses a reached set optimized for program location-dependent
analysis.Modifier and Type | Class and Description |
---|---|
static class |
JvmBamCpaRun.Builder
A builder for
JvmBamCpaRun . |
Modifier and Type | Field and Description |
---|---|
protected JvmCfa |
cfa |
HeapModel |
heapModel |
reduceHeap
abortOperator, cpa
Modifier | Constructor and Description |
---|---|
protected |
JvmBamCpaRun(JvmCfa cfa,
int maxCallStackDepth)
Create a JVM BAM CPA run.
|
protected |
JvmBamCpaRun(JvmCfa cfa,
int maxCallStackDepth,
HeapModel heapModel,
AbortOperator abortOperator,
boolean reduceHeap)
Create a JVM BAM CPA run.
|
Modifier and Type | Method and Description |
---|---|
protected ReachedSet |
createReachedSet()
Returns an empty
ReachedSet . |
ReduceOperator<JvmCfaNode,JvmCfaEdge,MethodSignature> |
createReduceOperator()
Returns the reduce operator.
|
JvmCfa |
getCfa()
Returns the CFA.
|
createCache, createExpandOperator, createIntraproceduralCPA, createRebuildOperator, getAnalyzedMethods, getCpa, getMainSignature, getMaxCallStackDepth
createWaitlist, execute, getAbortOperator, getInitialStates
protected JvmBamCpaRun(JvmCfa cfa, int maxCallStackDepth)
cfa
- a CFAmaxCallStackDepth
- the maximum depth of the call stack analyzed interprocedurally 0 means
intraprocedural analysis < 0 means no maximum depthprotected JvmBamCpaRun(JvmCfa cfa, int maxCallStackDepth, HeapModel heapModel, AbortOperator abortOperator, boolean reduceHeap)
cfa
- a CFAmaxCallStackDepth
- the maximum depth of the call stack analyzed interprocedurally 0 means
intraprocedural analysis < 0 means no maximum depthabortOperator
- an abort operatorreduceHeap
- whether reduction/expansion of the heap state is performed at call/return
sitespublic JvmCfa getCfa()
BamCpaRun
getCfa
in class BamCpaRun<CpaT extends ConfigurableProgramAnalysis,OuterAbstractStateT extends AbstractState,JvmCfaNode,JvmCfaEdge,MethodSignature>
public ReduceOperator<JvmCfaNode,JvmCfaEdge,MethodSignature> createReduceOperator()
BamCpaRun
createReduceOperator
in class BamCpaRun<CpaT extends ConfigurableProgramAnalysis,OuterAbstractStateT extends AbstractState,JvmCfaNode,JvmCfaEdge,MethodSignature>
protected ReachedSet createReachedSet()
CpaRun
ReachedSet
.createReachedSet
in class CpaRun<BamCpa<JvmCfaNode,JvmCfaEdge,MethodSignature>,OuterAbstractStateT extends AbstractState>