Package org.checkerframework.checker.nullness

Class NullnessAnnotatedTypeFactory

java.lang.Object

org.checkerframework.framework.type.AnnotatedTypeFactory

org.checkerframework.framework.type.GenericAnnotatedTypeFactory<Value,Store,Transfer,Flow>

org.checkerframework.checker.initialization.InitializationAnnotatedTypeFactory<NullnessValue,NullnessStore,NullnessTransfer,NullnessAnalysis>

org.checkerframework.checker.nullness.NullnessAnnotatedTypeFactory

All Implemented Interfaces:

AnnotationProvider

public class NullnessAnnotatedTypeFactory
extends InitializationAnnotatedTypeFactory<NullnessValue,NullnessStore,NullnessTransfer,NullnessAnalysis>

The annotated type factory for the nullness type-system.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
protected static class	NullnessAnnotatedTypeFactory.NullnessPropagationTreeAnnotator	Nullness doesn't call propagation on binary and unary because the result is always @Initialized (the default qualifier).
protected class	NullnessAnnotatedTypeFactory.NullnessQualifierHierarchy	NullnessQualifierHierarchy.
protected class	NullnessAnnotatedTypeFactory.NullnessTreeAnnotator
protected class	NullnessAnnotatedTypeFactory.NullnessTypeAnnotator

Nested classes/interfaces inherited from class org.checkerframework.checker.initialization.InitializationAnnotatedTypeFactory

InitializationAnnotatedTypeFactory.CommitmentTreeAnnotator, InitializationAnnotatedTypeFactory.CommitmentTypeAnnotator, InitializationAnnotatedTypeFactory.InitializationQualifierHierarchy

Nested classes/interfaces inherited from class org.checkerframework.framework.type.GenericAnnotatedTypeFactory

GenericAnnotatedTypeFactory.ScanState

Nested classes/interfaces inherited from class org.checkerframework.framework.type.AnnotatedTypeFactory

AnnotatedTypeFactory.CapturedTypeVarSubstitutor, AnnotatedTypeFactory.ParameterizedExecutableType

Field Summary

Fields

Modifier and Type	Field	Description
protected final ExecutableElement	classGetCanonicalName	The Class.getCanonicalName() method.
protected final CollectionToArrayHeuristics	collectionToArrayHeuristics	Determines the nullness type of calls to Collection.toArray().
protected final AnnotationMirror	MONOTONIC_NONNULL	The @MonotonicNonNull annotation.
protected final AnnotationMirror	NONNULL	The @NonNull annotation.
protected final AnnotationMirror	NULLABLE	The @Nullable annotation.
protected final Set<Class<? extends Annotation>>	nullnessAnnos	Cache for the nullness annotations.
protected final AnnotationMirror	POLYNULL	The @PolyNull annotation.
protected final SystemGetPropertyHandler	systemGetPropertyHandler	Handles invocations of System.getProperty(String).

Fields inherited from class org.checkerframework.checker.initialization.InitializationAnnotatedTypeFactory

FBCBOTTOM, initAnnoNames, initAnnos, INITIALIZED, NOT_ONLY_INITIALIZED, objectTypeMirror, UNDER_INITALIZATION, underInitializationValueElement, UNKNOWN_INITIALIZATION, unknownInitializationValueElement, unusedWhenElement

Fields inherited from class org.checkerframework.framework.type.GenericAnnotatedTypeFactory

analysis, arraysAreRelevant, cfgVisualizer, contractsUtils, defaults, dependentTypesHelper, emptyStore, exceptionalExitStores, flowByDefault, flowResult, flowResultAnalysisCaches, formalParameterPattern, hasOrIsSubchecker, initializationStaticStore, initializationStore, methodInvocationStores, poly, regularExitStores, relevantJavaTypes, returnStatementStores, scannedClasses, shouldClearSubcheckerSharedCFGs, sideEffectsUnrefineAliases, subcheckerSharedCFG, transfer, treeAnnotator, typeAnnotator

Fields inherited from class org.checkerframework.framework.type.AnnotatedTypeFactory

ajavaTypes, annotatedForValueElement, artificialTreeToEnclosingElementMap, capturedTypeVarSubstitutor, checker, currentFileAjavaTypes, elements, ensuresQualifierExpressionElement, ensuresQualifierIfExpressionElement, ensuresQualifierIfListTM, ensuresQualifierIfListValueElement, ensuresQualifierIfResultElement, ensuresQualifierIfTM, ensuresQualifierListTM, ensuresQualifierListValueElement, ensuresQualifierTM, fieldInvariantFieldElement, fieldInvariantQualifierElement, fromExpressionTreeCache, fromMemberTreeCache, fromTypeTreeCache, hasQualifierParameterValueElement, ignoreRawTypeArguments, loader, methodValClassNameElement, methodValMethodNameElement, methodValParamsElement, noQualifierParameterValueElement, objectGetClass, processingEnv, qualHierarchy, qualifierUpperBounds, reflectionResolver, requiresQualifierExpressionElement, requiresQualifierListTM, requiresQualifierListValueElement, requiresQualifierTM, root, shouldCache, stubTypes, trees, typeArgumentInference, typeFormatter, typeHierarchy, types, typeVarSubstitutor, uid, wpiOutputFormat

Constructor Summary

Constructors

Constructor	Description
NullnessAnnotatedTypeFactory(BaseTypeChecker checker)	Creates a NullnessAnnotatedTypeFactory.

Method Summary

Modifier and Type	Method	Description
void	adaptGetClassReturnTypeToReceiver(AnnotatedTypeMirror.AnnotatedExecutableType getClassType, AnnotatedTypeMirror receiverType, ExpressionTree tree)	Java special-cases the return type of getClass().
protected void	addAnnotationsFromDefaultForType(@Nullable Element element, AnnotatedTypeMirror type)	Adds default qualifiers based on the underlying type of type to type.
protected boolean	containsNullnessAnnotation(@Nullable List<? extends AnnotationTree> annoTrees, Tree typeTree)	Returns true if some annotation on the given type, or in the given list, is a nullness annotation such as @NonNull, @Nullable, @MonotonicNonNull, etc.
protected boolean	containsNullnessAnnotation(List<? extends AnnotationTree> annoTrees)	Returns true if some annotation in the given list is a nullness annotation such as @NonNull, @Nullable, @MonotonicNonNull, etc.
protected AnnotatedTypeFormatter	createAnnotatedTypeFormatter()	Returns an AnnotatedTypeFormatter that does not print the qualifiers on null literals.
protected DefaultForTypeAnnotator	createDefaultForTypeAnnotator()	Creates an DefaultForTypeAnnotator.
protected NullnessAnalysis	createFlowAnalysis()	Returns the appropriate flow analysis class that is used for the org.checkerframework.dataflow analysis.
NullnessTransfer	createFlowTransferFunction(CFAbstractAnalysis<NullnessValue,NullnessStore,NullnessTransfer> analysis)	Returns the appropriate transfer function that is used for the given org.checkerframework.dataflow analysis.
protected QualifierHierarchy	createQualifierHierarchy()	Returns the QualifierHierarchy to be used by this checker.
protected @Nullable AnnotationMirror	createRequiresOrEnsuresQualifier(String expression, AnnotationMirror qualifier, AnnotatedTypeMirror declaredType, Analysis.BeforeOrAfter preOrPost, @Nullable List<AnnotationMirror> preconds)	Creates a RequiresQualifier("...") or EnsuresQualifier("...") annotation for the given expression.
protected Set<Class<? extends Annotation>>	createSupportedTypeQualifiers()	Returns a mutable set of annotation classes that are supported by a checker.
protected TreeAnnotator	createTreeAnnotator()	Returns a TreeAnnotator that adds annotations to a type based on the contents of a tree.
protected TypeAnnotator	createTypeAnnotator()	Returns a DefaultForTypeAnnotator that adds annotations to a type based on the content of the type itself.
AnnotatedTypeMirror	getDefaultValueAnnotatedType(TypeMirror typeMirror)	Return the type of the default value of the given type.
AnnotationMirror	getFieldInvariantAnnotation()	Returns the annotation that makes up the invariant of this commitment type system, such as @NonNull.
AnnotatedTypeMirror	getMethodReturnType(MethodTree m, ReturnTree r)	Returns the return type of the method m at the return statement r.
Set<Class<? extends Annotation>>	getNullnessAnnotations()	Returns the list of annotations of the non-null type system.
org.plumelib.util.IPair<List<VariableTree>,List<VariableTree>>	getUninitializedFields(NullnessStore store, TreePath path, boolean isStatic, Collection<? extends AnnotationMirror> receiverAnnotations)	Returns the fields that are not yet initialized in a given store.
protected boolean	hasFieldInvariantAnnotation(AnnotatedTypeMirror type, VariableElement fieldElement)	Returns whether or not type has the invariant annotation.
boolean	isImmutable(TypeMirror type)	A non-null reference to an object stays non-null under mutation.
boolean	isMapGet(Node node)	Returns true if node is an invocation of Map.get.
protected boolean	isNonNullOrAlias(AnnotationMirror am)	Returns true if the given annotation is @NonNull or an alias for it.
protected boolean	isNullableOrAlias(AnnotationMirror am)	Returns true if the given annotation is @Nullable or an alias for it.
protected boolean	isNullnessAnnotation(AnnotationMirror am)	Returns true if the given annotation is a nullness annotation such as @NonNull, @Nullable, @MonotonicNonNull, etc.
protected AnnotatedTypeFactory.ParameterizedExecutableType	methodFromUse(MethodInvocationTree tree, boolean inferTypeArgs)	The implementation of AnnotatedTypeFactory.methodFromUse(MethodInvocationTree) and AnnotatedTypeFactory.methodFromUseWithoutTypeArgInference(MethodInvocationTree).
protected void	replacePolyQualifier(AnnotatedTypeMirror lhsType, Tree context)	For types of left-hand side of an assignment, this method replaces PolyNull with Nullable (or with NonNull if the org.checkerframework.dataflow analysis has determined that this is allowed soundly.
void	wpiAdjustForUpdateField(Tree lhsTree, Element element, String fieldName, AnnotatedTypeMirror rhsATM)	Changes the type of rhsATM when being assigned to a field, for use by whole-program inference.
void	wpiAdjustForUpdateNonField(AnnotatedTypeMirror rhsATM)	Changes the type of rhsATM when being assigned to anything other than a field, for use by whole-program inference.
boolean	wpiShouldInferTypesForReceivers()	Returns whether whole-program inference should infer types for receiver expressions.

Methods inherited from class org.checkerframework.checker.initialization.InitializationAnnotatedTypeFactory

areAllFieldsInitializedOnly, createUnderInitializationAnnotation, createUnderInitializationAnnotation, createUnknownInitializationAnnotation, createUnknownInitializationAnnotation, getAnnotatedTypeLhs, getInitializationAnnotations, getInitializedInvariantFields, getInvalidConstructorReturnTypeAnnotations, getSelfType, getTypeFrameFromAnnotation, getUnderInitializationAnnotationOfSuperType, getUninitializedInvariantFields, hasFieldInvariantAnnotation, isFbcBottom, isFbcBottom, isInitializationAnnotation, isInitialized, isInitialized, isInitializedForFrame, isUnderInitialization, isUnderInitialization, isUnknownInitialization, isUnknownInitialization, methodFromUse, postAsMemberOf, setSelfTypeInInitializationCode

Methods inherited from class org.checkerframework.framework.type.GenericAnnotatedTypeFactory

addCheckedCodeDefaults, addCheckedStandardDefaults, addComputedTypeAnnotations, addComputedTypeAnnotations, addComputedTypeAnnotations, addComputedTypeAnnotationsForWarnRedundant, addDefaultAnnotations, addSharedCFGForTree, addUncheckedStandardDefaults, analyze, annotationsForIrrelevantJavaType, applyInferredAnnotations, applyQualifierParameterDefaults, applyQualifierParameterDefaults, checkAndPerformFlowAnalysis, checkForDefaultQualifierInHierarchy, constructorFromUse, constructorFromUsePreSubstitution, createAndInitQualifierDefaults, createCFGVisualizer, createContractsFromMethod, createDefaultForUseTypeAnnotator, createDependentTypesHelper, createQualifierDefaults, createQualifierPolymorphism, getAnnotatedTypeLhsNoTypeVarDefault, getAnnotatedTypeRhsUnaryAssign, getAnnotatedTypeVarargsArray, getAnnotationFromJavaExpression, getAnnotationFromJavaExpressionString, getAnnotationMirrorFromJavaExpressionString, getAnnotationsFromJavaExpression, getCFGVisualizer, getContractAnnotations, getContractAnnotations, getContractExpressions, getContractsFromMethod, getDefaultAnnotations, getDefaultAnnotationsForWarnRedundant, getDefaultForTypeAnnotator, getDependentTypesHelper, getEmptyStore, getEnsuresQualifierIfResult, getExceptionalExitStore, getExplicitNewClassAnnos, getExplicitNewClassClassTypeArgs, getExpressionAndOffsetFromJavaExpressionString, getFinalLocalValues, getFirstNodeOfKindForTree, getInferredValueFor, getMethodReturnType, getNodesForTree, getPostconditionAnnotations, getPostconditionAnnotations, getPostconditionAnnotations, getPreconditionAnnotations, getPreconditionAnnotations, getPreconditionAnnotations, getPreOrPostconditionAnnotations, getQualifierPolymorphism, getRegularExitStore, getReturnStatementStores, getSharedCFGForTree, getShouldDefaultTypeVarLocals, getSortedQualifierNames, getStoreAfter, getStoreAfter, getStoreAfter, getStoreBefore, getStoreBefore, getStoreBefore, getSupportedMonotonicTypeQualifiers, getTypeFactoryOfSubchecker, getTypeFactoryOfSubcheckerOrNull, handleCFGViz, irrelevantExtraMessage, isIgnoredExceptionType, isRelevant, isRelevant, isRelevantImpl, isUnreachable, methodFromUsePreSubstitution, parseJavaExpressionString, performFlowAnalysis, postAnalyze, postDirectSuperTypes, postInit, preProcessClassTree, setRoot, typeVariablesFromUse

Methods inherited from class org.checkerframework.framework.type.AnnotatedTypeFactory

addAliasedDeclAnnotation, addAliasedTypeAnnotation, addAliasedTypeAnnotation, addAliasedTypeAnnotation, addAliasedTypeAnnotation, addAnnotationFromFieldInvariant, addInheritedAnnotation, applyCaptureConversion, applyCaptureConversion, applyUnboxing, areSameByClass, binaryTreeArgTypes, binaryTreeArgTypes, canonicalAnnotation, checkInvalidOptionsInferSignatures, compoundAssignmentTreeArgTypes, constructorFromUse, constructorFromUseWithoutTypeArgInference, containsCapturedTypes, containsSameByClass, createAnnotationClassLoader, createAnnotationFormatter, createQualifierUpperBounds, createTypeArgumentInference, createTypeHierarchy, createTypeVariableSubstitutor, declarationFromElement, doesAnnotatedForApplyToThisChecker, fromElement, fromElement, fromElement, getAnnotatedNullType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedTypeFormatter, getAnnotatedTypeFromTypeTree, getAnnotationByClass, getAnnotationFormatter, getAnnotationMirror, getAnnotationWithMetaAnnotation, getBoxedType, getBundledTypeQualifiers, getCacheSize, getChecker, getCheckerNames, getContractExpressions, getContractListValues, getDeclAnnotation, getDeclAnnotationNoAliases, getDeclAnnotations, getDeclAnnotationWithMetaAnnotation, getDefaultTypeDeclarationBounds, getDummyAssignedTo, getElementUtils, getEnclosingClassOrMethod, getEnclosingElementForArtificialTree, getEnclosingSubType, getEnclosingType, getEnumConstructorQualifiers, getExpressionAndOffset, getFieldInvariantAnnotationTree, getFieldInvariantDeclarationAnnotations, getFieldInvariants, getFnInterfaceFromTree, getFunctionTypeFromTree, getFunctionTypeFromTree, getImplicitReceiverType, getIterableElementType, getIterableElementType, getNarrowedAnnotations, getNarrowedPrimitive, getPath, getProcessingEnv, getQualifierHierarchy, getQualifierParameterHierarchies, getQualifierParameterHierarchies, getQualifierUpperBounds, getReceiverType, getResultingTypeOfConstructorMemberReference, getStringType, getSupportedTypeQualifierNames, getSupportedTypeQualifiers, getTreeUtils, getTypeArgumentInference, getTypeDeclarationBounds, getTypeHierarchy, getTypeOfExtendsImplements, getTypeVarSubstitutor, getUnboxedType, getVisitorTreePath, getWholeProgramInference, getWidenedAnnotations, getWidenedType, getWidenedType, hasExplicitNoQualifierParameterInHierarchy, hasExplicitQualifierParameterInHierarchy, hasQualifierParameterInHierarchy, hasQualifierParameterInHierarchy, initializeAtm, initializeReflectionResolution, isDeterministic, isFromByteCode, isFromStubFile, isSideEffectFree, isSupportedQualifier, isSupportedQualifier, isSupportedQualifier, isTop, isWithinConstructor, logGat, makeConditionConsistentWithOtherMethod, mergeAnnotationFileAnnosIntoType, methodFromUse, methodFromUse, methodFromUseWithoutTypeArgInference, methodFromUseWithoutTypeArgInference, negateConstant, order, parseAnnotationFiles, postProcessClassTree, replaceAnnotations, replaceAnnotations, setEnclosingElementForArtificialTree, setVisitorTreePath, shouldWarnIfStubRedundantWithBytecode, toAnnotatedType, toString, type, wpiPrepareMethodForWriting, wpiPrepareMethodForWriting

Methods inherited from class java.lang.Object

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

Field Details

NONNULL

protected final AnnotationMirror NONNULL

The @NonNull annotation.

NULLABLE

protected final AnnotationMirror NULLABLE

The @Nullable annotation.

POLYNULL

protected final AnnotationMirror POLYNULL

The @PolyNull annotation.

MONOTONIC_NONNULL

protected final AnnotationMirror MONOTONIC_NONNULL

The @MonotonicNonNull annotation.

systemGetPropertyHandler

protected final SystemGetPropertyHandler systemGetPropertyHandler

Handles invocations of System.getProperty(String).

collectionToArrayHeuristics

protected final CollectionToArrayHeuristics collectionToArrayHeuristics

Determines the nullness type of calls to Collection.toArray().

classGetCanonicalName

protected final ExecutableElement classGetCanonicalName

The Class.getCanonicalName() method.

nullnessAnnos

protected final Set<Class<? extends Annotation>> nullnessAnnos

Cache for the nullness annotations.

Constructor Details

NullnessAnnotatedTypeFactory

public NullnessAnnotatedTypeFactory(BaseTypeChecker checker)

Creates a NullnessAnnotatedTypeFactory.

Parameters:

checker - the associated NullnessChecker

Method Details

createSupportedTypeQualifiers

protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers()

Description copied from class: AnnotatedTypeFactory

Returns a mutable set of annotation classes that are supported by a checker.

Subclasses may override this method to return a mutable set of their supported type qualifiers through one of the 5 approaches shown below.

Subclasses should not call this method; they should call AnnotatedTypeFactory.getSupportedTypeQualifiers() instead.

By default, a checker supports all annotations located in a subdirectory called qual that's located in the same directory as the checker. Note that only annotations defined with the @Target({ElementType.TYPE_USE}) meta-annotation (and optionally with the additional value of ElementType.TYPE_PARAMETER, but no other ElementType values) are automatically considered as supported annotations.

To support a different set of annotations than those in the qual subdirectory, or that have other ElementType values, see examples below.

In total, there are 5 ways to indicate annotations that are supported by a checker:

1. Only support annotations located in a checker's qual directory:

   This is the default behavior. Simply place those annotations within the qual directory.

2. Support annotations located in a checker's qual directory and a list of other annotations:

   Place those annotations within the qual directory, and override AnnotatedTypeFactory.createSupportedTypeQualifiers() by calling AnnotatedTypeFactory.getBundledTypeQualifiers(Class...) with a varargs parameter list of the other annotations. Code example:

    @Override protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers() {
         return getBundledTypeQualifiers(Regex.class, PartialRegex.class, RegexBottom.class, UnknownRegex.class);
     } 
    

3. Supporting only annotations that are explicitly listed: Override AnnotatedTypeFactory.createSupportedTypeQualifiers() and return a mutable set of the supported annotations. Code example:

    @Override protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers() {
         return new HashSet<Class<? extends Annotation>>(
                 Arrays.asList(A.class, B.class));
     } 
    

   The set of qualifiers returned by AnnotatedTypeFactory.createSupportedTypeQualifiers() must be a fresh, mutable set. The methods AnnotatedTypeFactory.getBundledTypeQualifiers(Class...) must return a fresh, mutable set

Overrides:

createSupportedTypeQualifiers in class AnnotatedTypeFactory

Returns:

the type qualifiers supported this processor, or an empty set if none

replacePolyQualifier

protected void replacePolyQualifier(AnnotatedTypeMirror lhsType,
 Tree context)

For types of left-hand side of an assignment, this method replaces PolyNull with Nullable (or with NonNull if the org.checkerframework.dataflow analysis has determined that this is allowed soundly. For example:

 @PolyNull String foo(@PolyNull String param) {
    if (param == null) {
        //  @PolyNull is really @Nullable, so change
        // the type of param to @Nullable.
        param = null;
    }
    return param;
 }
 

Parameters:

lhsType - type to replace whose polymorphic qualifier will be replaced

context - tree used to get dataflow value

getUninitializedFields

public org.plumelib.util.IPair<List<VariableTree>,List<VariableTree>> getUninitializedFields(NullnessStore store,
 TreePath path,
 boolean isStatic,
 Collection<? extends AnnotationMirror> receiverAnnotations)

Description copied from class: InitializationAnnotatedTypeFactory

Returns the fields that are not yet initialized in a given store. The result is a pair of lists:

• fields that are not yet initialized and have the invariant annotation
• fields that are not yet initialized and do not have the invariant annotation

Overrides:

getUninitializedFields in class InitializationAnnotatedTypeFactory<NullnessValue,NullnessStore,NullnessTransfer,NullnessAnalysis>

Parameters:

store - a store

path - the current path, used to determine the current class

isStatic - whether to report static fields or instance fields

receiverAnnotations - the annotations on the receiver

Returns:

the fields that are not yet initialized in a given store (a pair of lists)

createFlowAnalysis

protected NullnessAnalysis createFlowAnalysis()

Description copied from class: GenericAnnotatedTypeFactory

Returns the appropriate flow analysis class that is used for the org.checkerframework.dataflow analysis.

This implementation uses the checker naming convention to create the appropriate analysis. If no transfer function is found, it returns an instance of CFAnalysis.

Subclasses have to override this method to create the appropriate analysis if they do not follow the checker naming convention.

Overrides:

createFlowAnalysis in class GenericAnnotatedTypeFactory<NullnessValue,NullnessStore,NullnessTransfer,NullnessAnalysis>

Returns:

the appropriate flow analysis class that is used for the org.checkerframework.dataflow analysis

createFlowTransferFunction

public NullnessTransfer createFlowTransferFunction(CFAbstractAnalysis<NullnessValue,NullnessStore,NullnessTransfer> analysis)

Description copied from class: GenericAnnotatedTypeFactory

Returns the appropriate transfer function that is used for the given org.checkerframework.dataflow analysis.

This implementation uses the checker naming convention to create the appropriate transfer function. If no transfer function is found, it returns an instance of CFTransfer.

Subclasses have to override this method to create the appropriate transfer function if they do not follow the checker naming convention.

Overrides:

createFlowTransferFunction in class GenericAnnotatedTypeFactory<NullnessValue,NullnessStore,NullnessTransfer,NullnessAnalysis>

Parameters:

analysis - a dataflow analysis

Returns:

a new transfer function

createAnnotatedTypeFormatter

protected AnnotatedTypeFormatter createAnnotatedTypeFormatter()

Returns an AnnotatedTypeFormatter that does not print the qualifiers on null literals.

Overrides:

createAnnotatedTypeFormatter in class AnnotatedTypeFactory

Returns:

an AnnotatedTypeFormatter that does not print the qualifiers on null literals

methodFromUse

protected AnnotatedTypeFactory.ParameterizedExecutableType methodFromUse(MethodInvocationTree tree,
 boolean inferTypeArgs)

Description copied from class: AnnotatedTypeFactory

The implementation of AnnotatedTypeFactory.methodFromUse(MethodInvocationTree) and AnnotatedTypeFactory.methodFromUseWithoutTypeArgInference(MethodInvocationTree).

Overrides:

methodFromUse in class GenericAnnotatedTypeFactory<NullnessValue,NullnessStore,NullnessTransfer,NullnessAnalysis>

Parameters:

tree - a method invocation tree

inferTypeArgs - whether type arguments should be inferred

Returns:

the type of the invoked method, any explicit type arguments, and if inferTypeArgs is true, any inferred type arguments

adaptGetClassReturnTypeToReceiver

public void adaptGetClassReturnTypeToReceiver(AnnotatedTypeMirror.AnnotatedExecutableType getClassType,
 AnnotatedTypeMirror receiverType,
 ExpressionTree tree)

Description copied from class: AnnotatedTypeFactory

Java special-cases the return type of getClass(). Though the method has a return type of Class<?>, the compiler special cases this return-type and changes the bound of the type argument to the erasure of the receiver type. For example:

• x.getClass() has the type Class< ? extends erasure_of_x >
• someInteger.getClass() has the type Class< ? extends Integer >

Overrides:

adaptGetClassReturnTypeToReceiver in class AnnotatedTypeFactory

Parameters:

getClassType - this must be a type representing a call to Object.getClass otherwise a runtime exception will be thrown. It is modified by side effect.

receiverType - the receiver type of the method invocation (not the declared receiver type)

tree - getClass method invocation tree

getMethodReturnType

public AnnotatedTypeMirror getMethodReturnType(MethodTree m,
 ReturnTree r)

Description copied from class: AnnotatedTypeFactory

Returns the return type of the method m at the return statement r. This implementation just calls AnnotatedTypeFactory.getMethodReturnType(MethodTree), but subclasses may override this method to change the type based on the return statement.

Overrides:

getMethodReturnType in class AnnotatedTypeFactory

Parameters:

m - tree of a method declaration

r - a return statement within method m

Returns:

the return type of the method m at the return statement r

createDefaultForTypeAnnotator

protected DefaultForTypeAnnotator createDefaultForTypeAnnotator()

Description copied from class: GenericAnnotatedTypeFactory

Creates an DefaultForTypeAnnotator.

Overrides:

createDefaultForTypeAnnotator in class GenericAnnotatedTypeFactory<NullnessValue,NullnessStore,NullnessTransfer,NullnessAnalysis>

Returns:

a new DefaultForTypeAnnotator

addAnnotationsFromDefaultForType

protected void addAnnotationsFromDefaultForType(@Nullable Element element,
 AnnotatedTypeMirror type)

Description copied from class: GenericAnnotatedTypeFactory

Adds default qualifiers based on the underlying type of type to type. If element is a local variable, or if the type already has an annotation from the relevant type hierarchy, then the defaults are not added.

(This uses both the DefaultQualifierForUseTypeAnnotator and DefaultForTypeAnnotator.)

Overrides:

addAnnotationsFromDefaultForType in class GenericAnnotatedTypeFactory<NullnessValue,NullnessStore,NullnessTransfer,NullnessAnalysis>

Parameters:

element - possibly null element whose type is type

type - the type to which defaults are added

createTypeAnnotator

protected TypeAnnotator createTypeAnnotator()

Description copied from class: GenericAnnotatedTypeFactory

Returns a DefaultForTypeAnnotator that adds annotations to a type based on the content of the type itself.

Subclass may override this method. The default type annotator is a ListTypeAnnotator of the following:

1. IrrelevantTypeAnnotator: Adds top to types not listed in the @RelevantJavaTypes annotation on the checker.
2. PropagationTypeAnnotator: Propagates annotation onto wildcards.

Overrides:

createTypeAnnotator in class InitializationAnnotatedTypeFactory<NullnessValue,NullnessStore,NullnessTransfer,NullnessAnalysis>

Returns:

a type annotator

createTreeAnnotator

protected TreeAnnotator createTreeAnnotator()

Description copied from class: GenericAnnotatedTypeFactory

Returns a TreeAnnotator that adds annotations to a type based on the contents of a tree.

The default tree annotator is a ListTreeAnnotator of the following:

1. PropagationTreeAnnotator: Propagates annotations from subtrees
2. LiteralTreeAnnotator: Adds annotations based on QualifierForLiterals meta-annotations
3. DependentTypesTreeAnnotator: Adapts dependent annotations based on context

Subclasses may override this method to specify additional tree annotators, for example:

 new ListTreeAnnotator(super.createTreeAnnotator(), new KeyLookupTreeAnnotator(this));
 

Overrides:

createTreeAnnotator in class InitializationAnnotatedTypeFactory<NullnessValue,NullnessStore,NullnessTransfer,NullnessAnalysis>

Returns:

a tree annotator

getNullnessAnnotations

public Set<Class<? extends Annotation>> getNullnessAnnotations()

Returns the list of annotations of the non-null type system.

Returns:

the list of annotations of the non-null type system

getFieldInvariantAnnotation

public AnnotationMirror getFieldInvariantAnnotation()

Description copied from class: InitializationAnnotatedTypeFactory

Returns the annotation that makes up the invariant of this commitment type system, such as @NonNull.

Specified by:

getFieldInvariantAnnotation in class InitializationAnnotatedTypeFactory<NullnessValue,NullnessStore,NullnessTransfer,NullnessAnalysis>

Returns:

the invariant annotation for this type system

hasFieldInvariantAnnotation

protected boolean hasFieldInvariantAnnotation(AnnotatedTypeMirror type,
 VariableElement fieldElement)

Returns whether or not type has the invariant annotation.

If the type is a type variable, this method returns true if any possible instantiation of the type parameter could have the invariant annotation. See InitializationAnnotatedTypeFactory.hasFieldInvariantAnnotation(VariableTree) for an example.

In other words, is the lower bound @NonNull?

Specified by:

hasFieldInvariantAnnotation in class InitializationAnnotatedTypeFactory<NullnessValue,NullnessStore,NullnessTransfer,NullnessAnalysis>

Parameters:

type - of field that might have invariant annotation

fieldElement - the field element, which can be used to check annotations on the declaration

Returns:

whether or not type has the invariant annotation

createQualifierHierarchy

protected QualifierHierarchy createQualifierHierarchy()

Description copied from class: AnnotatedTypeFactory

Returns the QualifierHierarchy to be used by this checker.

The implementation builds the type qualifier hierarchy for the AnnotatedTypeFactory.getSupportedTypeQualifiers() using the meta-annotations found in them. The current implementation returns an instance of NoElementQualifierHierarchy.

Subclasses must override this method if their qualifiers have elements; the method must return an implementation of QualifierHierarchy, such as ElementQualifierHierarchy.

Overrides:

createQualifierHierarchy in class AnnotatedTypeFactory

Returns:

a QualifierHierarchy for this type system

containsNullnessAnnotation

protected boolean containsNullnessAnnotation(@Nullable List<? extends AnnotationTree> annoTrees,
 Tree typeTree)

Returns true if some annotation on the given type, or in the given list, is a nullness annotation such as @NonNull, @Nullable, @MonotonicNonNull, etc.

This method ignores aliases of nullness annotations that are declaration annotations, because they may apply to inner types.

Parameters:

annoTrees - a list of annotations that the Java parser attached to the variable/method declaration; null if this type is not from such a location. This is a list of extra annotations to check, in addition to those on the type.

typeTree - the type whose annotations to test

Returns:

true if some annotation is a nullness annotation

containsNullnessAnnotation

protected boolean containsNullnessAnnotation(List<? extends AnnotationTree> annoTrees)

Returns true if some annotation in the given list is a nullness annotation such as @NonNull, @Nullable, @MonotonicNonNull, etc.

This method ignores aliases of nullness annotations that are declaration annotations, because they may apply to inner types.

Clients that are processing a field or variable definition, or a method return type, should call containsNullnessAnnotation(List, Tree) instead.

Parameters:

annoTrees - a list of annotations to check

Returns:

true if some annotation is a nullness annotation

See Also:

• containsNullnessAnnotation(List, Tree)

isNullnessAnnotation

protected boolean isNullnessAnnotation(AnnotationMirror am)

Returns true if the given annotation is a nullness annotation such as @NonNull, @Nullable, @MonotonicNonNull, etc.

Parameters:

am - an annotation

Returns:

true if the given annotation is a nullness annotation

isNonNullOrAlias

protected boolean isNonNullOrAlias(AnnotationMirror am)

Returns true if the given annotation is @NonNull or an alias for it.

Parameters:

am - an annotation

Returns:

true if the given annotation is @NonNull or an alias for it

isNullableOrAlias

protected boolean isNullableOrAlias(AnnotationMirror am)

Returns true if the given annotation is @Nullable or an alias for it.

Parameters:

am - an annotation

Returns:

true if the given annotation is @Nullable or an alias for it

getDefaultValueAnnotatedType

public AnnotatedTypeMirror getDefaultValueAnnotatedType(TypeMirror typeMirror)

Description copied from class: GenericAnnotatedTypeFactory

Return the type of the default value of the given type. The default value is 0, false, or null.

Overrides:

getDefaultValueAnnotatedType in class GenericAnnotatedTypeFactory<NullnessValue,NullnessStore,NullnessTransfer,NullnessAnalysis>

Parameters:

typeMirror - a type

Returns:

the annotated type of type's default value

isImmutable

public boolean isImmutable(TypeMirror type)

A non-null reference to an object stays non-null under mutation.

Overrides:

isImmutable in class AnnotatedTypeFactory

Parameters:

type - type to test

Returns:

true if the type is immutable

wpiAdjustForUpdateField

public void wpiAdjustForUpdateField(Tree lhsTree,
 Element element,
 String fieldName,
 AnnotatedTypeMirror rhsATM)

Description copied from class: AnnotatedTypeFactory

Changes the type of rhsATM when being assigned to a field, for use by whole-program inference. The default implementation does nothing.

Overrides:

wpiAdjustForUpdateField in class AnnotatedTypeFactory

Parameters:

lhsTree - the tree for the field whose type will be changed

element - the element for the field whose type will be changed

fieldName - the name of the field whose type will be changed

rhsATM - the type of the expression being assigned to the field, which is side-effected by this method

wpiAdjustForUpdateNonField

public void wpiAdjustForUpdateNonField(AnnotatedTypeMirror rhsATM)

Description copied from class: AnnotatedTypeFactory

Changes the type of rhsATM when being assigned to anything other than a field, for use by whole-program inference. The default implementation does nothing.

Overrides:

wpiAdjustForUpdateNonField in class AnnotatedTypeFactory

Parameters:

rhsATM - the type of the rhs of the pseudo-assignment, which is side-effected by this method

wpiShouldInferTypesForReceivers

public boolean wpiShouldInferTypesForReceivers()

Description copied from class: AnnotatedTypeFactory

Returns whether whole-program inference should infer types for receiver expressions. For some type systems, such as nullness, it doesn't make sense for WPI to do inference on receivers.

Overrides:

wpiShouldInferTypesForReceivers in class AnnotatedTypeFactory

Returns:

true if WPI should infer types for method receiver parameters, false otherwise

createRequiresOrEnsuresQualifier

protected @Nullable AnnotationMirror createRequiresOrEnsuresQualifier(String expression,
 AnnotationMirror qualifier,
 AnnotatedTypeMirror declaredType,
 Analysis.BeforeOrAfter preOrPost,
 @Nullable List<AnnotationMirror> preconds)

Description copied from class: GenericAnnotatedTypeFactory

Creates a RequiresQualifier("...") or EnsuresQualifier("...") annotation for the given expression.

This is of the form @RequiresQualifier(expression="expression", qualifier=MyQual.class) or @EnsuresQualifier(expression="expression", qualifier=MyQual.class), where "expression" is exactly the string expression and MyQual is the annotation represented by qualifier.

Returns null if the expression is invalid when combined with the kind of annotation: for example, precondition annotations on "this" and parameters ("#1", etc.) are not supported, because receiver/parameter annotations should be inferred instead.

This implementation returns null if no annotation can be created, because the qualifier has elements/arguments, which @RequiresQualifier and @EnsuresQualifier do not support. Subclasses may override this method to return qualifiers that do have arguments instead of returning null.

Overrides:

createRequiresOrEnsuresQualifier in class GenericAnnotatedTypeFactory<NullnessValue,NullnessStore,NullnessTransfer,NullnessAnalysis>

Parameters:

expression - the expression to which the qualifier applies

qualifier - the qualifier that must be present

declaredType - the declared type of the expression, which is used to avoid inferring redundant pre- or postcondition annotations

preOrPost - whether to return a precondition or postcondition annotation

preconds - the list of precondition annotations; used to suppress redundant postconditions; non-null exactly when preOrPost is BeforeOrAfter.BEFORE

Returns:

a RequiresQualifier("...") or EnsuresQualifier("...") annotation for the given expression, or null

isMapGet

public boolean isMapGet(Node node)

Returns true if node is an invocation of Map.get.

Parameters:

node - a CFG node

Returns:

true if node is an invocation of Map.get