public class CpaWithBamOperators<CfaNodeT extends CfaNode<CfaEdgeT,SignatureT>,CfaEdgeT extends CfaEdge<CfaNodeT>,SignatureT extends Signature> extends SimpleCpa
BamCpa
to be extended
inter-procedurally.
Compared to a standard ConfigurableProgramAnalysis
, this is extended with three
operators:
- The reduce operator discards from the entry abstract state of a procedure the unnecessary information (e.g. local variables of the caller).
- The expand operator restores the removed information.
- The rebuild operator avoids collision of program identifiers while returning from a procedure call (e.g. renaming variables).
Constructor and Description |
---|
CpaWithBamOperators(AbstractDomain abstractDomain,
ProgramLocationDependentTransferRelation<CfaNodeT,CfaEdgeT,SignatureT> transferRelation,
MergeOperator merge,
StopOperator stop,
PrecisionAdjustment precisionAdjustment,
ReduceOperator<CfaNodeT,CfaEdgeT,SignatureT> reduce,
ExpandOperator<CfaNodeT,CfaEdgeT,SignatureT> expand,
RebuildOperator rebuild)
Create a CPA with BAM operators from the abstract domain and the operators.
|
CpaWithBamOperators(ConfigurableProgramAnalysis intraproceduralCpa,
ReduceOperator<CfaNodeT,CfaEdgeT,SignatureT> reduce,
ExpandOperator<CfaNodeT,CfaEdgeT,SignatureT> expand,
RebuildOperator rebuild)
Create a CPA with BAM operators from the intra-procedural
ConfigurableProgramAnalysis
and the additional BAM operators. |
Modifier and Type | Method and Description |
---|---|
ExpandOperator<CfaNodeT,CfaEdgeT,SignatureT> |
getExpandOperator()
Returns the
ExpandOperator . |
RebuildOperator |
getRebuildOperator()
Returns the
RebuildOperator . |
ReduceOperator<CfaNodeT,CfaEdgeT,SignatureT> |
getReduceOperator()
Returns the
ReduceOperator . |
getAbstractDomain, getMergeOperator, getPrecisionAdjustment, getStopOperator, getTransferRelation
public CpaWithBamOperators(AbstractDomain abstractDomain, ProgramLocationDependentTransferRelation<CfaNodeT,CfaEdgeT,SignatureT> transferRelation, MergeOperator merge, StopOperator stop, PrecisionAdjustment precisionAdjustment, ReduceOperator<CfaNodeT,CfaEdgeT,SignatureT> reduce, ExpandOperator<CfaNodeT,CfaEdgeT,SignatureT> expand, RebuildOperator rebuild)
abstractDomain
- a join-semilattice of AbstractState
s defining the abstraction
level of the analysistransferRelation
- a transfer relation specifying how successor states are computedmerge
- a merge operator defining how (and whether) the older AbstractState
should
be updated with the newly discovered AbstractState
stop
- a stop operator deciding whether the successor state should be added to the ReachedSet
based on the content of the latterprecisionAdjustment
- a precision adjustment selecting the Precision
for the
currently processed AbstractState
considering the ReachedSet
contentreduce
- a reduce operator discarding from the entry abstract state of procedures the
unnecessary informationexpand
- an expand operator restoring the information removed during reductionrebuild
- a rebuild operator avoiding identifiers collision while returning from a
procedure callpublic CpaWithBamOperators(ConfigurableProgramAnalysis intraproceduralCpa, ReduceOperator<CfaNodeT,CfaEdgeT,SignatureT> reduce, ExpandOperator<CfaNodeT,CfaEdgeT,SignatureT> expand, RebuildOperator rebuild)
ConfigurableProgramAnalysis
and the additional BAM operators.intraproceduralCpa
- an intra-procedural ConfigurableProgramAnalysis
reduce
- a reduce operator discarding from the entry abstract state of procedures the
unnecessary informationexpand
- an expand operator restoring the information removed during reductionrebuild
- a rebuild operator avoiding identifiers collision while returning from a
procedure callpublic ReduceOperator<CfaNodeT,CfaEdgeT,SignatureT> getReduceOperator()
ReduceOperator
.public ExpandOperator<CfaNodeT,CfaEdgeT,SignatureT> getExpandOperator()
ExpandOperator
.public RebuildOperator getRebuildOperator()
RebuildOperator
.