org.checkerframework.checker.nullness

Class NullnessAnalysis

java.lang.Object

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

org.checkerframework.framework.flow.CFAbstractAnalysis<NullnessValue,NullnessStore,NullnessTransfer>

org.checkerframework.checker.nullness.NullnessAnalysis

public class NullnessAnalysis
extends CFAbstractAnalysis<NullnessValue,NullnessStore,NullnessTransfer>

The analysis class for the non-null type system (serves as factory for the transfer function, stores and abstract values.

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
NullnessAnalysis(BaseTypeChecker checker, NullnessAnnotatedTypeFactory factory, java.util.List<Pair<javax.lang.model.element.VariableElement,NullnessValue>> fieldValues)

Method Summary

Modifier and Type	Method and Description
NullnessValue	createAbstractValue(java.util.Set<javax.lang.model.element.AnnotationMirror> annotations, javax.lang.model.type.TypeMirror underlyingType)
NullnessStore	createCopiedStore(NullnessStore s)
NullnessStore	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

NullnessAnalysis

public NullnessAnalysis(BaseTypeChecker checker,
                        NullnessAnnotatedTypeFactory factory,
                        java.util.List<Pair<javax.lang.model.element.VariableElement,NullnessValue>> fieldValues)

Method Detail

createEmptyStore

public NullnessStore createEmptyStore(boolean sequentialSemantics)

Specified by:

createEmptyStore in class CFAbstractAnalysis<NullnessValue,NullnessStore,NullnessTransfer>

Returns:

an empty store of the appropriate type

createCopiedStore

public NullnessStore createCopiedStore(NullnessStore s)

Specified by:

createCopiedStore in class CFAbstractAnalysis<NullnessValue,NullnessStore,NullnessTransfer>

Returns:

an identical copy of the store s.

createAbstractValue

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

Specified by:

createAbstractValue in class CFAbstractAnalysis<NullnessValue,NullnessStore,NullnessTransfer>

Returns:

an abstract value containing the given annotations and underlyingType.