public class SameLenAnnotatedTypeFactory
extends org.checkerframework.common.basetype.BaseAnnotatedTypeFactory
This annotated type factory refines types in X cases:
@PolyAll
and @PolyLength
are refined to @PolySameLen
.
@SameLen
annotation, then the type
of the new variable is the union of the user-written arrays in the annotation and the
arrays listed in the SameLen types of each of those arrays.
new T[a.length]
is the union of the
SameLen type of a
and the arrays listed in a
's SameLen type.
Modifier and Type | Class and Description |
---|---|
protected class |
SameLenAnnotatedTypeFactory.SameLenTreeAnnotator
SameLen needs a tree annotator in order to properly type the right side of assignments of new
arrays that are initialized with the length of another array.
|
Modifier and Type | Field and Description |
---|---|
javax.lang.model.element.AnnotationMirror |
UNKNOWN |
analysis, cfgVisualizer, defaults, dependentTypesHelper, emptyStore, FLOW_BY_DEFAULT, flowResult, flowResultAnalysisCaches, initializationStaticStore, initializationStore, methodInvocationStores, poly, regularExitStores, returnStatementStores, scannedClasses, transfer, treeAnnotator, typeAnnotator
checker, elements, fromExpressionTreeCache, fromMemberTreeCache, fromTypeTreeCache, ignoreUninferredTypeArguments, loader, processingEnv, qualHierarchy, reflectionResolver, root, shouldCache, trees, typeArgumentInference, typeFormatter, typeHierarchy, types, typeVarSubstitutor, uid, visitorState
Constructor and Description |
---|
SameLenAnnotatedTypeFactory(org.checkerframework.common.basetype.BaseTypeChecker checker)
Handles case 1.
|
Modifier and Type | Method and Description |
---|---|
javax.lang.model.element.AnnotationMirror |
createCombinedSameLen(org.checkerframework.dataflow.analysis.FlowExpressions.Receiver rec1,
org.checkerframework.dataflow.analysis.FlowExpressions.Receiver rec2,
javax.lang.model.element.AnnotationMirror a1,
javax.lang.model.element.AnnotationMirror a2)
Combines the given arrays and annotations into a single SameLen annotation.
|
javax.lang.model.element.AnnotationMirror |
createCombinedSameLen(java.util.List<org.checkerframework.dataflow.analysis.FlowExpressions.Receiver> receivers,
java.util.List<javax.lang.model.element.AnnotationMirror> annos)
For the use of the transfer function; generates a SameLen that includes a and b, as well as
everything in sl1 and sl2, if they are SameLen annotations.
|
org.checkerframework.framework.type.QualifierHierarchy |
createQualifierHierarchy(org.checkerframework.framework.util.MultiGraphQualifierHierarchy.MultiGraphFactory factory) |
javax.lang.model.element.AnnotationMirror |
createSameLen(java.lang.String... val)
Creates a @SameLen annotation whose values are the given strings.
|
protected java.util.Set<java.lang.Class<? extends java.lang.annotation.Annotation>> |
createSupportedTypeQualifiers() |
org.checkerframework.framework.type.treeannotator.TreeAnnotator |
createTreeAnnotator() |
org.checkerframework.framework.type.AnnotatedTypeMirror |
getAnnotatedTypeLhs(Tree tree)
Handles case 2.
|
javax.lang.model.element.AnnotationMirror |
getCombinedSameLen(java.util.List<java.lang.String> a1Names,
java.util.List<java.lang.String> a2Names)
This function finds the union of the values of two annotations.
|
java.util.List<java.lang.String> |
getSameLensFromString(java.lang.String sequenceExpression,
Tree tree,
TreePath currentPath)
Find all the sequences that are members of the SameLen annotation associated with the
sequence named in sequenceExpression along the current path.
|
static boolean |
shouldUseInAnnotation(org.checkerframework.dataflow.analysis.FlowExpressions.Receiver receiver) |
createFlowAnalysis
addCheckedCodeDefaults, addCheckedStandardDefaults, addComputedTypeAnnotations, addComputedTypeAnnotations, addComputedTypeAnnotations, addDefaultAnnotations, addTypeNameImplicit, addUncheckedCodeDefaults, addUncheckedStandardDefaults, analyze, analyze, applyInferredAnnotations, checkAndPerformFlowAnalysis, checkForDefaultQualifierInHierarchy, constructorFromUse, createAndInitQualifierDefaults, createCFGVisualizer, createDependentTypesHelper, createFlowTransferFunction, createQualifierDefaults, createQualifierPolymorphism, createTypeAnnotator, fromNewClass, getAnnotatedTypeLhsNoTypeVarDefault, getAnnotatedTypeRhsUnaryAssign, getAnnotatedTypeVarargsArray, getAnnotationFromJavaExpressionString, getAnnotationFromReceiver, getCFGVisualizer, getDependentTypesHelper, getEmptyStore, getFinalLocalValues, getFirstNodeOfKindForTree, getInferredValueFor, getMethodReturnType, getMethodReturnType, getNodesForTree, getReceiverFromJavaExpressionString, getRegularExitStore, getResultingTypeOfConstructorMemberReference, getReturnStatementStores, getShouldDefaultTypeVarLocals, getSortedQualifierNames, getStoreAfter, getStoreAfter, getStoreAfter, getStoreBefore, getStoreBefore, getStoreBefore, getSupportedMonotonicTypeQualifiers, getTypeFactoryOfSubchecker, handleCFGViz, methodFromUse, performFlowAnalysis, postDirectSuperTypes, postInit, preProcessClassTree, setRoot, typeVariablesFromUse
adaptGetClassReturnTypeToReceiver, addAliasedAnnotation, addAliasedAnnotation, addAliasedAnnotation, addAliasedAnnotation, addAliasedDeclAnnotation, addAnnotationFromFieldInvariant, addInheritedAnnotation, aliasedAnnotation, annotateInheritedFromClass, annotateInheritedFromClass, checkInvalidOptionsInferSignatures, createAnnotatedTypeFormatter, createAnnotationClassLoader, createAnnotationFormatter, createQualifierHierarchy, createQualifierHierarchy, createQualifierHierarchyFactory, createTypeArgumentInference, createTypeHierarchy, createTypeVariableSubstitutor, declarationFromElement, fromElement, fromElement, fromElement, getAnnotatedNullType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedType, getAnnotatedTypeFormatter, getAnnotatedTypeFromTypeTree, getAnnotationFormatter, getAnnotationMirror, getAnnotationWithMetaAnnotation, getBoxedType, getBundledTypeQualifiersWithoutPolyAll, getBundledTypeQualifiersWithPolyAll, getCacheSize, getContext, getCurrentClassTree, getCurrentClassType, getCurrentMethodReceiver, getDeclAnnotation, getDeclAnnotationNoAliases, getDeclAnnotations, getDeclAnnotationWithMetaAnnotation, getElementUtils, getEnclosingMethod, getEnclosingType, getFieldInvariantAnnotationTree, getFieldInvariantDeclarationAnnotations, getFieldInvariants, getFnInterfaceFromTree, getFnInterfaceFromTree, getImplicitReceiverType, getNarrowedPrimitive, getPath, getProcessingEnv, getQualifierHierarchy, getReceiverType, getSelfType, getStringType, getSupportedTypeQualifiers, getTreeUtils, getTypeArgumentInference, getTypeHierarchy, getTypeVarSubstitutor, getUnboxedType, getUninferredWildcardType, getVisitorState, getWholeProgramInference, initializeReflectionResolution, isAnyEnclosingThisDeref, isFromByteCode, isFromStubFile, isMostEnclosingThisDeref, isSupportedQualifier, isWithinConstructor, methodFromUse, parseStubFiles, postAsMemberOf, postProcessClassTree, postTypeVarSubstitution, setPathHack, toAnnotatedType, toString, type, widenToUpperBound
public SameLenAnnotatedTypeFactory(org.checkerframework.common.basetype.BaseTypeChecker checker)
protected java.util.Set<java.lang.Class<? extends java.lang.annotation.Annotation>> createSupportedTypeQualifiers()
createSupportedTypeQualifiers
in class org.checkerframework.framework.type.AnnotatedTypeFactory
public org.checkerframework.framework.type.QualifierHierarchy createQualifierHierarchy(org.checkerframework.framework.util.MultiGraphQualifierHierarchy.MultiGraphFactory factory)
createQualifierHierarchy
in class org.checkerframework.framework.type.AnnotatedTypeFactory
public org.checkerframework.framework.type.AnnotatedTypeMirror getAnnotatedTypeLhs(Tree tree)
getAnnotatedTypeLhs
in class org.checkerframework.framework.type.GenericAnnotatedTypeFactory<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore,org.checkerframework.framework.flow.CFTransfer,org.checkerframework.framework.flow.CFAnalysis>
public javax.lang.model.element.AnnotationMirror getCombinedSameLen(java.util.List<java.lang.String> a1Names, java.util.List<java.lang.String> a2Names)
public javax.lang.model.element.AnnotationMirror createCombinedSameLen(org.checkerframework.dataflow.analysis.FlowExpressions.Receiver rec1, org.checkerframework.dataflow.analysis.FlowExpressions.Receiver rec2, javax.lang.model.element.AnnotationMirror a1, javax.lang.model.element.AnnotationMirror a2)
createCombinedSameLen(List, List)
.public javax.lang.model.element.AnnotationMirror createCombinedSameLen(java.util.List<org.checkerframework.dataflow.analysis.FlowExpressions.Receiver> receivers, java.util.List<javax.lang.model.element.AnnotationMirror> annos)
receivers
- a list of receivers representing arrays to be included in the combined
annotationannos
- a list of the current annotations of the receivers. Must be the same length as
receivers.public static boolean shouldUseInAnnotation(org.checkerframework.dataflow.analysis.FlowExpressions.Receiver receiver)
public org.checkerframework.framework.type.treeannotator.TreeAnnotator createTreeAnnotator()
createTreeAnnotator
in class org.checkerframework.framework.type.GenericAnnotatedTypeFactory<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore,org.checkerframework.framework.flow.CFTransfer,org.checkerframework.framework.flow.CFAnalysis>
public javax.lang.model.element.AnnotationMirror createSameLen(java.lang.String... val)
public java.util.List<java.lang.String> getSameLensFromString(java.lang.String sequenceExpression, Tree tree, TreePath currentPath)