org.checkerframework.framework.flow

Class CFAnalysis

java.lang.Object

org.checkerframework.dataflow.analysis.Analysis<V,S,T>

org.checkerframework.framework.flow.CFAbstractAnalysis<CFValue,CFStore,CFTransfer>

org.checkerframework.framework.flow.CFAnalysis

public class CFAnalysis
extends CFAbstractAnalysis<CFValue,CFStore,CFTransfer>

The default org.checkerframework.dataflow analysis used in the Checker Framework.

Author:

Stefan Heule

Nested Class Summary

Nested classes/interfaces inherited from class org.checkerframework.dataflow.analysis.Analysis

Analysis.Worklist

Field Summary

Fields inherited from class org.checkerframework.framework.flow.CFAbstractAnalysis

atypeFactory, checker, fieldValues, qualifierHierarchy, typeHierarchy

Fields inherited from class org.checkerframework.dataflow.analysis.Analysis

blockCount, cfg, currentInput, currentNode, currentTree, elseStores, env, finalLocalValues, inputs, isRunning, maxCountBeforeWidening, nodeValues, storesAtReturnStatements, thenStores, transferFunction, types, worklist

Constructor Summary

Constructors

Constructor and Description
CFAnalysis(BaseTypeChecker checker, GenericAnnotatedTypeFactory<CFValue,CFStore,CFTransfer,CFAnalysis> factory, java.util.List<Pair<javax.lang.model.element.VariableElement,CFValue>> fieldValues)

Method Summary

Modifier and Type	Method and Description
CFValue	createAbstractValue(java.util.Set<javax.lang.model.element.AnnotationMirror> annotations, javax.lang.model.type.TypeMirror underlyingType)
CFStore	createCopiedStore(CFStore s)
CFStore	createEmptyStore(boolean sequentialSemantics)

Methods inherited from class org.checkerframework.framework.flow.CFAbstractAnalysis

createAbstractValue, createSingleAnnotationValue, createTransferFunction, defaultCreateAbstractValue, getFieldValues, getTypeFactory, getTypeFactoryOfSubchecker, getTypeHierarchy, visualizeCFG

Methods inherited from class org.checkerframework.dataflow.analysis.Analysis

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, updateNodeValues

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

CFAnalysis

public CFAnalysis(BaseTypeChecker checker,
                  GenericAnnotatedTypeFactory<CFValue,CFStore,CFTransfer,CFAnalysis> factory,
                  java.util.List<Pair<javax.lang.model.element.VariableElement,CFValue>> fieldValues)

Method Detail

createEmptyStore

public CFStore createEmptyStore(boolean sequentialSemantics)

Specified by:

createEmptyStore in class CFAbstractAnalysis<CFValue,CFStore,CFTransfer>

Returns:

an empty store of the appropriate type

createCopiedStore

public CFStore createCopiedStore(CFStore s)

Specified by:

createCopiedStore in class CFAbstractAnalysis<CFValue,CFStore,CFTransfer>

Returns:

an identical copy of the store s.

createAbstractValue

public CFValue createAbstractValue(java.util.Set<javax.lang.model.element.AnnotationMirror> annotations,
                                   javax.lang.model.type.TypeMirror underlyingType)

Specified by:

createAbstractValue in class CFAbstractAnalysis<CFValue,CFStore,CFTransfer>

Returns:

an abstract value containing the given annotations and underlyingType.