Class GrowOnlyChecker
java.lang.Object
javax.annotation.processing.AbstractProcessor
org.checkerframework.javacutil.AbstractTypeProcessor
org.checkerframework.framework.source.SourceChecker
org.checkerframework.common.basetype.BaseTypeChecker
org.checkerframework.checker.index.growonly.GrowOnlyChecker
- All Implemented Interfaces:
Processor,OptionConfiguration
@RelevantJavaTypes({java.util.Collection.class,java.util.Iterator.class})
@SuppressWarningsPrefix({"index","mutable"})
public class GrowOnlyChecker
extends BaseTypeChecker
A type-checker that enforces rules about mutable-length sequences.
This checker ensures that references annotated as @GrowOnly are not used to call
methods that can shrink the sequence (e.g., remove(), clear()). This allows other
checkers, like the Upper Bound Checker, to reason that indices for @GrowOnly collections
remain valid after mutations.
-
Nested Class Summary
Nested classes/interfaces inherited from class org.checkerframework.framework.source.SourceChecker
SourceChecker.CheckerMessage -
Field Summary
Fields inherited from class org.checkerframework.common.basetype.BaseTypeChecker
baseTypeCheckerClassArray, ultimateParentCheckerFields inherited from class org.checkerframework.framework.source.SourceChecker
activeOptions, currentRoot, DETAILS_SEPARATOR, elements, elementsWithSuppressedWarnings, immediateSubcheckers, javacErrored, messager, messagesProperties, messageStore, MSGS_FILE, OPTION_SEPARATOR, parentChecker, subcheckers, supportedOptions, SUPPRESS_ALL_MESSAGE_KEY, SUPPRESS_ALL_PREFIX, suppressWarningsPrefixesOfSubcheckers, treePathCacher, trees, types, UNNEEDED_SUPPRESSION_KEY, upstreamCheckerNames, useAllcheckersPrefix, visitorFields inherited from class javax.annotation.processing.AbstractProcessor
processingEnv -
Constructor Summary
Constructors -
Method Summary
Methods inherited from class org.checkerframework.common.basetype.BaseTypeChecker
createSourceVisitor, createSourceVisitorPublic, createSupportedLintOptions, getAnnotationProvider, getTypeFactory, getTypeFactoryOfSubcheckerOrNull, getUltimateParentChecker, getVisitor, invokeConstructorFor, processErrorMessageArg, shouldAddShutdownHook, shutdownHookMethods inherited from class org.checkerframework.framework.source.SourceChecker
expandCFOptions, fullMessageOf, getBooleanOption, getBooleanOption, getElementUtils, getExtraStubFiles, getImmediateSubcheckerClasses, getLintOption, getLintOption, getMessagesProperties, getOption, getOption, getOptionConfiguration, getOptions, getOptionsNoSubcheckers, getParentChecker, getPathToCompilationUnit, getProcessingEnvironment, getProperties, getRelatedClassName, getStandardSuppressWarningsPrefixes, getStringsOption, getStringsOption, getSubchecker, getSubCheckerIndex, getSubcheckers, getSupportedAnnotationTypes, getSupportedLintOptions, getSupportedOptions, getSupportedSourceVersion, getSuppressWarningsPrefixes, getSuppressWarningsPrefixesOfSubcheckers, getTreePathCacher, getTreeUtils, getTypeUtils, getUpstreamCheckerNames, hasOption, hasOptionNoSubcheckers, init, initChecker, instantiateSubcheckers, message, message, messageKeyMatches, printOrStoreMessage, printOrStoreMessage, printStats, printStoredMessages, report, reportError, reportWarning, setLintOption, setParentChecker, setRoot, shouldResolveReflection, shouldSkipDefs, shouldSkipDefs, shouldSkipDefs, shouldSkipFiles, shouldSkipUses, shouldSkipUses, shouldSuppressWarnings, shouldSuppressWarnings, shouldSuppressWarnings, typeProcess, typeProcessingOver, typeProcessingStart, useConservativeDefault, warnUnneededSuppressions, warnUnneededSuppressionsMethods inherited from class org.checkerframework.javacutil.AbstractTypeProcessor
getCompilerLog, processMethods inherited from class javax.annotation.processing.AbstractProcessor
getCompletions, isInitializedMethods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, waitMethods inherited from interface org.checkerframework.framework.util.OptionConfiguration
getStringsOption, getStringsOption
-
Constructor Details
-
GrowOnlyChecker
public GrowOnlyChecker()Creates a new GrowOnlyChecker.
-