AbstractSingleWrapperState |
|
AbstractWaitlist<CollectionT extends java.util.Collection<AbstractState>> |
This is a base class for Waitlist s parametrized by the carrier CollectionT .
|
AbstractWrapperState |
|
BamCpaRun<CpaT extends ConfigurableProgramAnalysis,AbstractStateT extends AbstractState,CfaNodeT extends CfaNode<CfaEdgeT,SignatureT>,CfaEdgeT extends CfaEdge<CfaNodeT>,SignatureT extends Signature> |
|
BamCpaRun.Builder |
|
BreadthFirstWaitlist |
This Waitlist pops the first element, i.e., performs a breadth first traversal over the
Cfa .
|
Cfa<CfaNodeT extends CfaNode<CfaEdgeT,SignatureT>,CfaEdgeT extends CfaEdge<CfaNodeT>,SignatureT extends Signature> |
A Cfa is a control flow automaton with nodes <CfaNodeT> and edges
<CfaEdgeT> .
|
ControllableAbortOperator |
|
CpaRun<CpaT extends ConfigurableProgramAnalysis,AbstractStateT extends AbstractState> |
|
DefaultReachedSet |
This is a LinkedHashSet -based implementation of the ReachedSet .
|
DelegateAbstractDomain<LatticeAbstractStateT extends LatticeAbstractState> |
|
DepthFirstWaitlist |
This Waitlist pops the last element, i.e., performs a depth first traversal over the
Cfa .
|
DifferentialMap<K,V> |
A differential representation of maps.
|
DifferentialMapAbstractState<KeyT,AbstractSpaceT extends LatticeAbstractState<AbstractSpaceT>> |
|
HashMapAbstractState<KeyT,AbstractSpaceT extends LatticeAbstractState<AbstractSpaceT>> |
|
LimitedHashMap<K,V> |
This LimitedHashMap is a HashMap which limits its content based on the function
removeElement .
|
LimitedHashMapAbstractState<KeyT,AbstractSpaceT extends LatticeAbstractState<AbstractSpaceT>> |
|
ListAbstractState<AbstractSpaceT extends LatticeAbstractState<AbstractSpaceT>> |
|
MergeJoinOperator |
|
MergeSepOperator |
|
NeverAbortOperator |
|
PrecisionAdjustmentResult |
|
ProgramLocationDependentReachedSet<CfaNodeT extends CfaNode<CfaEdgeT,SignatureT>,CfaEdgeT extends CfaEdge<CfaNodeT>,AbstractStateT extends AbstractState & ProgramLocationDependent<CfaNodeT,CfaEdgeT,SignatureT>,SignatureT extends Signature> |
|
SequentialCpaRun<CpaT extends ConfigurableProgramAnalysis,AbstractStateT extends AbstractState,InputCpaRunT extends CpaRun> |
This CpaRun wraps another InputCpaRunT and allows a following CpaT to be
constructed using the output of the former run.
|
SetAbstractState<T> |
|
SimpleCpa |
|
SingleWrapperTransferRelation |
|
StackAbstractState<AbstractSpaceT extends LatticeAbstractState<AbstractSpaceT>> |
|
StaticPrecisionAdjustment |
|
StopAlwaysOperator |
This StopOperator always returns true, i.e., it can be used for a single pass of the
analysis.
|
StopContainedOperator |
|
StopJoinOperator |
This StopOperator returns true if the input state is less or equal than join over the
reached set.
|
StopNeverOperator |
This StopOperator always returns false, i.e., it can be used for analyses running until
the Waitlist becomes empty.
|
StopSepOperator |
|