public abstract class CFAbstractAnalysis<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>,T extends CFAbstractTransfer<V,S,T>> extends Analysis<V,S,T>
CFAbstractAnalysis is an extensible org.checkerframework.dataflow analysis for the
Checker Framework that tracks the annotations using a flow-sensitive analysis. It uses an AnnotatedTypeFactory to provide checker-specific logic how to combine types (e.g., what is the
type of a string concatenation, given the types of the two operands) and as an abstraction
function (e.g., determine the annotations on literals).
The purpose of this class is twofold: Firstly, it serves as factory for abstract values,
stores and the transfer function. Furthermore, it makes it easy for the transfer function and the
stores to access the AnnotatedTypeFactory, the qualifier hierarchy, etc.
Analysis.Worklist| Modifier and Type | Field and Description |
|---|---|
protected GenericAnnotatedTypeFactory<V,S,T,? extends CFAbstractAnalysis<V,S,T>> |
atypeFactory
A type factory that can provide static type annotations for AST Trees.
|
protected SourceChecker |
checker
A checker used to do error reporting.
|
protected List<Pair<VariableElement,V>> |
fieldValues
Initial abstract types for fields.
|
protected QualifierHierarchy |
qualifierHierarchy
The qualifier hierarchy for which to track annotations.
|
protected TypeHierarchy |
typeHierarchy
The type hierarchy.
|
blockCount, cfg, currentInput, currentNode, currentTree, elseStores, env, finalLocalValues, inputs, isRunning, maxCountBeforeWidening, nodeValues, storesAtReturnStatements, thenStores, transferFunction, types, worklist| Constructor and Description |
|---|
CFAbstractAnalysis(BaseTypeChecker checker,
GenericAnnotatedTypeFactory<V,S,T,? extends CFAbstractAnalysis<V,S,T>> factory,
List<Pair<VariableElement,V>> fieldValues) |
CFAbstractAnalysis(BaseTypeChecker checker,
GenericAnnotatedTypeFactory<V,S,T,? extends CFAbstractAnalysis<V,S,T>> factory,
List<Pair<VariableElement,V>> fieldValues,
int maxCountBeforeWidening) |
| Modifier and Type | Method and Description |
|---|---|
V |
createAbstractValue(AnnotatedTypeMirror type)
Creates an abstract value from the annotated type mirror.
|
abstract V |
createAbstractValue(Set<AnnotationMirror> annotations,
TypeMirror underlyingType) |
abstract S |
createCopiedStore(S s) |
abstract S |
createEmptyStore(boolean sequentialSemantics) |
V |
createSingleAnnotationValue(AnnotationMirror anno,
TypeMirror underlyingType)
Returns an abstract value containing an annotated type with the annotation
anno, and
'top' for all other hierarchies. |
T |
createTransferFunction() |
CFValue |
defaultCreateAbstractValue(CFAbstractAnalysis<CFValue,?,?> analysis,
Set<AnnotationMirror> annotations,
TypeMirror underlyingType)
Default implementation for
createAbstractValue(Set, TypeMirror) |
List<Pair<VariableElement,V>> |
getFieldValues() |
GenericAnnotatedTypeFactory<V,S,T,? extends CFAbstractAnalysis<V,S,T>> |
getTypeFactory() |
<W extends GenericAnnotatedTypeFactory<?,?,?,?>,U extends BaseTypeChecker> |
getTypeFactoryOfSubchecker(Class<U> checkerClass) |
TypeHierarchy |
getTypeHierarchy() |
void |
visualizeCFG()
Perform a visualization of the CFG and analysis info for inspection.
|
addStoreBefore, addToWorklist, callTransferFunction, getContainingClass, getContainingMethod, getCurrentTree, getEnv, getExceptionalExitStore, getInput, getInputBefore, getNodeForTree, getRegularExitStore, getResult, getReturnStatementStores, getStoreBefore, getTransferFunction, getTypes, getValue, getValue, init, isRunning, performAnalysis, propagateStoresTo, readFromStore, setCurrentTree, setTransferFunction, updateNodeValuesprotected final QualifierHierarchy qualifierHierarchy
protected final TypeHierarchy typeHierarchy
protected final GenericAnnotatedTypeFactory<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>,T extends CFAbstractTransfer<V,S,T>,? extends CFAbstractAnalysis<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>,T extends CFAbstractTransfer<V,S,T>>> atypeFactory
protected final SourceChecker checker
protected final List<Pair<VariableElement,V extends CFAbstractValue<V>>> fieldValues
public CFAbstractAnalysis(BaseTypeChecker checker, GenericAnnotatedTypeFactory<V,S,T,? extends CFAbstractAnalysis<V,S,T>> factory, List<Pair<VariableElement,V>> fieldValues, int maxCountBeforeWidening)
public CFAbstractAnalysis(BaseTypeChecker checker, GenericAnnotatedTypeFactory<V,S,T,? extends CFAbstractAnalysis<V,S,T>> factory, List<Pair<VariableElement,V>> fieldValues)
public List<Pair<VariableElement,V>> getFieldValues()
public T createTransferFunction()
public abstract S createEmptyStore(boolean sequentialSemantics)
public abstract S createCopiedStore(S s)
s.public V createAbstractValue(AnnotatedTypeMirror type)
CFAbstractValue for an explanation.type.public abstract V createAbstractValue(Set<AnnotationMirror> annotations, TypeMirror underlyingType)
annotations and underlyingType.public CFValue defaultCreateAbstractValue(CFAbstractAnalysis<CFValue,?,?> analysis, Set<AnnotationMirror> annotations, TypeMirror underlyingType)
createAbstractValue(Set, TypeMirror)public TypeHierarchy getTypeHierarchy()
public GenericAnnotatedTypeFactory<V,S,T,? extends CFAbstractAnalysis<V,S,T>> getTypeFactory()
public void visualizeCFG()
public V createSingleAnnotationValue(AnnotationMirror anno, TypeMirror underlyingType)
anno, and
'top' for all other hierarchies. The underlying type is Object.public <W extends GenericAnnotatedTypeFactory<?,?,?,?>,U extends BaseTypeChecker> W getTypeFactoryOfSubchecker(Class<U> checkerClass)