Class LowerBoundAnnotatedTypeFactory
- All Implemented Interfaces:
AnnotationProvider
The type hierarchy is:
Top = lbu ("Lower Bound Unknown")
|
gte-1 ("Greater than or equal to -1")
|
nn ("NonNegative")
|
pos ("Positive")
In general, check whether the constant Value Checker can determine the value of a variable; if it
can, use that; if not, use more specific rules based on expression type. This class implements
the following type rules:
- 1. If the value checker type for any expression is ≥ 1, refine that expression's type to positive.
- 2. If the value checker type for any expression is ≥ 0 and case 1 did not apply, then refine that expression's type to non-negative.
- 3. If the value checker type for any expression is ≥ -1 and cases 1 and 2 did not apply, then refine that expression's type to GTEN1.
- 4. A unary prefix decrement shifts the type "down" in the hierarchy (i.e.
--iwheniis non-negative implies thatiwill be GTEN1 afterwards). Should this be 3 rules? - 5. A unary prefix increment shifts the type "up" in the hierarchy (i.e.
++iwheniis non-negative implies thatiwill be positive afterwards). Should this be 3 rules? - 6. Unary negation on a NegativeIndexFor from the SearchIndex type system results in a non-negative.
- 7. The result of a call to Math.max is the GLB of its arguments.
- 8. If an array has a MinLen type ≥ 1 and its length is accessed, the length expression is positive.
-
Nested Class Summary
Nested classes/interfaces inherited from class org.checkerframework.framework.type.GenericAnnotatedTypeFactory
GenericAnnotatedTypeFactory.ScanStateNested classes/interfaces inherited from class org.checkerframework.framework.type.AnnotatedTypeFactory
AnnotatedTypeFactory.CapturedTypeVarSubstitutor, AnnotatedTypeFactory.ParameterizedExecutableType -
Field Summary
FieldsModifier and TypeFieldDescriptionfinal AnnotationMirrorThe bottom annotation.final AnnotationMirrorThe canonical @GTENegativeOneannotation.final AnnotationMirrorThe canonical @NonNegativeannotation.final AnnotationMirrorThe canonical @PolyLowerBoundannotation.final AnnotationMirrorThe canonical @Positiveannotation.final AnnotationMirrorThe canonical @LowerBoundUnknownannotation.Fields inherited from class org.checkerframework.checker.index.BaseAnnotatedTypeFactoryForIndexChecker
hasSubsequenceFromElement, hasSubsequenceSubsequenceElement, hasSubsequenceToElementFields 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, typeAnnotatorFields 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, typeInformationPresenter, types, typeVarSubstitutor, uid, wpiOutputFormat -
Constructor Summary
ConstructorsConstructorDescriptionCreate a new LowerBoundAnnotatedTypeFactory. -
Method Summary
Modifier and TypeMethodDescriptionvoidaddComputedTypeAnnotations(Tree tree, AnnotatedTypeMirror type, boolean iUseFlow) Handles cases 1, 2, and 3.voidaddComputedTypeAnnotations(Element element, AnnotatedTypeMirror type) Handles cases 1, 2, and 3.protected Set<Class<? extends Annotation>> Returns a mutable set of annotation classes that are supported by a checker.Returns aTreeAnnotatorthat adds annotations to a type based on the contents of a tree.Returns the LessThan Checker's annotated type factory.Returns the SearchIndexFor Checker's annotated type factory.Returns the Value Checker's annotated type factory.booleanisNonNegative(Tree tree) Checks if the expression is non-negative, i.e.Methods inherited from class org.checkerframework.checker.index.BaseAnnotatedTypeFactoryForIndexChecker
hasSubsequenceFromValue, hasSubsequenceSubsequenceValue, hasSubsequenceToValueMethods inherited from class org.checkerframework.common.basetype.BaseAnnotatedTypeFactory
createFlowAnalysisMethods inherited from class org.checkerframework.framework.type.GenericAnnotatedTypeFactory
addAnnotationsFromDefaultForType, addCheckedCodeDefaults, addCheckedStandardDefaults, addComputedTypeAnnotations, addComputedTypeAnnotationsForWarnRedundant, addDefaultAnnotations, addSharedCFGForTree, addUncheckedStandardDefaults, analyze, annotationsForIrrelevantJavaType, applyInferredAnnotations, applyQualifierParameterDefaults, applyQualifierParameterDefaults, checkAndPerformFlowAnalysis, checkForDefaultQualifierInHierarchy, constructorFromUse, constructorFromUsePreSubstitution, createAndInitQualifierDefaults, createCFGVisualizer, createContractsFromMethod, createDefaultForTypeAnnotator, createDefaultForUseTypeAnnotator, createDependentTypesHelper, createFlowTransferFunction, createQualifierDefaults, createQualifierPolymorphism, createRequiresOrEnsuresQualifier, createTypeAnnotator, getAnnotatedTypeLhs, getAnnotatedTypeLhsNoTypeVarDefault, getAnnotatedTypeRhsUnaryAssign, getAnnotatedTypeVarargsArray, getAnnotationFromJavaExpression, getAnnotationFromJavaExpressionString, getAnnotationMirrorFromJavaExpressionString, getAnnotationsFromJavaExpression, getCFGVisualizer, getContractAnnotations, getContractAnnotations, getContractExpressions, getContractsFromMethod, getDefaultAnnotations, getDefaultAnnotationsForWarnRedundant, getDefaultForTypeAnnotator, getDefaultValueAnnotatedType, 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, methodFromUse, methodFromUsePreSubstitution, parseJavaExpressionString, performFlowAnalysis, postAnalyze, postAsMemberOf, postDirectSuperTypes, postInit, preProcessClassTree, setRoot, typeVariablesFromUseMethods inherited from class org.checkerframework.framework.type.AnnotatedTypeFactory
adaptGetClassReturnTypeToReceiver, addAliasedDeclAnnotation, addAliasedTypeAnnotation, addAliasedTypeAnnotation, addAliasedTypeAnnotation, addAliasedTypeAnnotation, addAnnotationFromFieldInvariant, addInheritedAnnotation, applyCaptureConversion, applyCaptureConversion, applyUnboxing, areSameByClass, binaryTreeArgTypes, binaryTreeArgTypes, canonicalAnnotation, checkInvalidOptionsInferSignatures, compoundAssignmentTreeArgTypes, constructorFromUse, constructorFromUseWithoutTypeArgInference, containsCapturedTypes, containsSameByClass, createAnnotatedTypeFormatter, createAnnotationClassLoader, createAnnotationFormatter, createQualifierHierarchy, createQualifierUpperBounds, createTypeArgumentInference, createTypeHierarchy, createTypeInformationPresenter, 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, getMethodReturnType, getNarrowedAnnotations, getNarrowedPrimitive, getPath, getProcessingEnv, getQualifierHierarchy, getQualifierParameterHierarchies, getQualifierParameterHierarchies, getQualifierUpperBounds, getReceiverType, getResultingTypeOfConstructorMemberReference, getSelfType, getStringType, getSupportedTypeQualifierNames, getSupportedTypeQualifiers, getTreeUtils, getTypeArgumentInference, getTypeDeclarationBounds, getTypeHierarchy, getTypeOfExtendsImplements, getTypeVarSubstitutor, getUnboxedType, getVisitorTreePath, getWholeProgramInference, getWidenedAnnotations, getWidenedType, getWidenedType, hasExplicitNoQualifierParameterInHierarchy, hasExplicitQualifierParameterInHierarchy, hasQualifierParameterInHierarchy, hasQualifierParameterInHierarchy, initializeAtm, initializeReflectionResolution, isDeterministic, isFromByteCode, isFromStubFile, isImmutable, isSideEffectFree, isSupportedQualifier, isSupportedQualifier, isSupportedQualifier, isTop, isWithinConstructor, logGat, makeConditionConsistentWithOtherMethod, mergeAnnotationFileAnnosIntoType, methodFromUse, methodFromUse, methodFromUse, methodFromUseWithoutTypeArgInference, methodFromUseWithoutTypeArgInference, negateConstant, order, parseAnnotationFiles, postProcessClassTree, replaceAnnotations, replaceAnnotations, setEnclosingElementForArtificialTree, setVisitorTreePath, shouldWarnIfStubRedundantWithBytecode, toAnnotatedType, toString, type, wpiAdjustForUpdateField, wpiAdjustForUpdateNonField, wpiPrepareMethodForWriting, wpiPrepareMethodForWriting, wpiShouldInferTypesForReceivers
-
Field Details
-
GTEN1
The canonical @GTENegativeOneannotation. -
NN
The canonical @NonNegativeannotation. -
POS
The canonical @Positiveannotation. -
BOTTOM
The bottom annotation. -
UNKNOWN
The canonical @LowerBoundUnknownannotation. -
POLY
The canonical @PolyLowerBoundannotation.
-
-
Constructor Details
-
LowerBoundAnnotatedTypeFactory
Create a new LowerBoundAnnotatedTypeFactory.- Parameters:
checker- the type-checker
-
-
Method Details
-
createSupportedTypeQualifiers
Description copied from class:AnnotatedTypeFactoryReturns 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 ofElementType.TYPE_PARAMETER, but no otherElementTypevalues) are automatically considered as supported annotations.To support a different set of annotations than those in the qual subdirectory, or that have other
ElementTypevalues, see examples below.In total, there are 5 ways to indicate annotations that are supported by a checker:
- Only support annotations located in a checker's qual directory:
This is the default behavior. Simply place those annotations within the qual directory.
- 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 callingAnnotatedTypeFactory.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); } - Supporting only annotations that are explicitly listed: Override
AnnotatedTypeFactory.createSupportedTypeQualifiers()and return a mutable set of the supported annotations. Code example:
The set of qualifiers returned by@Override protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers() { return new HashSet<Class<? extends Annotation>>( Arrays.asList(A.class, B.class)); }AnnotatedTypeFactory.createSupportedTypeQualifiers()must be a fresh, mutable set. The methodsAnnotatedTypeFactory.getBundledTypeQualifiers(Class...)must return a fresh, mutable set
- Overrides:
createSupportedTypeQualifiersin classAnnotatedTypeFactory- Returns:
- the type qualifiers supported this processor, or an empty set if none
- Only support annotations located in a checker's qual directory:
-
addComputedTypeAnnotations
Handles cases 1, 2, and 3.- Overrides:
addComputedTypeAnnotationsin classGenericAnnotatedTypeFactory<CFValue,CFStore, CFTransfer, CFAnalysis> - Parameters:
element- an elementtype- the type obtained fromelt
-
addComputedTypeAnnotations
Handles cases 1, 2, and 3.- Overrides:
addComputedTypeAnnotationsin classGenericAnnotatedTypeFactory<CFValue,CFStore, CFTransfer, CFAnalysis> - Parameters:
tree- an AST nodetype- the type obtained from treeiUseFlow- whether to use information from dataflow analysis
-
getValueAnnotatedTypeFactory
Returns the Value Checker's annotated type factory. -
getSearchIndexAnnotatedTypeFactory
Returns the SearchIndexFor Checker's annotated type factory. -
getLessThanAnnotatedTypeFactory
Returns the LessThan Checker's annotated type factory. -
createTreeAnnotator
Description copied from class:GenericAnnotatedTypeFactoryReturns aTreeAnnotatorthat adds annotations to a type based on the contents of a tree.The default tree annotator is a
ListTreeAnnotatorof the following:PropagationTreeAnnotator: Propagates annotations from subtreesLiteralTreeAnnotator: Adds annotations based onQualifierForLiteralsmeta-annotationsDependentTypesTreeAnnotator: 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:
createTreeAnnotatorin classGenericAnnotatedTypeFactory<CFValue,CFStore, CFTransfer, CFAnalysis> - Returns:
- a tree annotator
-
isNonNegative
Checks if the expression is non-negative, i.e. it has Positive on NonNegative annotation.
-