Package org.checkerframework.checker.initialization

Class InitializationChecker

java.lang.Object
javax.annotation.processing.AbstractProcessor
org.checkerframework.javacutil.AbstractTypeProcessor
org.checkerframework.framework.source.SourceChecker
org.checkerframework.common.basetype.BaseTypeChecker
org.checkerframework.checker.initialization.InitializationChecker
All Implemented Interfaces:
Processor, OptionConfiguration
Direct Known Subclasses:
NullnessChecker
public abstract class InitializationChecker extends BaseTypeChecker
Tracks whether a value is initialized (all its fields are set), and checks that values are initialized before being used. Implements the freedom-before-commitment scheme for initialization, augmented by type frames.

Because there is a cyclic dependency between this type system and the target type system, using this checker is more complex than for others. Specifically:

  1. Any target type system must provide two checkers: the target checker does all of the checking of the target type system (e.g., nullness), while the target checker's parent belongs to a subclass of the InitializationChecker. You can look at the NullnessChecker for an example: For the nullness type system, the NullnessNoInitSubchecker is the target checker which actually checks NonNull and related qualifiers, while the NullnessChecker is a subclass of this checker and thus checks Initialized and related qualifiers. The parent-child relationship between the checkers is necessary because this checker is dependent on the target checker to know which fields should be checked for initialization, and when such a field is initialized: A field is checked for initialization if its declared type is not the top type and does not have the meta-annotation HoldsForDefaultValue (e.g., NonNull). Such a field becomes initialized as soon as its refined type agrees with its declared type (which can happen either by assigning the field or by a contract annotation like EnsuresNonNull).
  2. The target checker must add the InitializationFieldAccessSubchecker as a subchecker and the InitializationFieldAccessTreeAnnotator as a tree annotator. This is necessary to give possibly uninitialized fields the top type of the target hierarchy (e.g., Nullable), ensuring that all fields are initialized before being used. This needs to be a separate checker because the target checker cannot access any type information from its parent, which is only initialized after all subcheckers have finished.
  3. The target checker must override all necessary methods in the target checker's type factory to take the type information from the InitializationFieldAccessSubchecker into account. You can look at NullnessNoInitAnnotatedTypeFactory for examples.
  4. Any subclass of the InitializationChecker should support the command-line option -AassumeInitialized via @SupportedOptions({"assumeInitialized"}), so initialization checking can be turned off. This gives users of, e.g., the NullnessChecker an easy way to turn off initialization checking without having to directly call the NullnessNoInitSubchecker.

If you want to modify the freedom-before-commitment scheme in your subclass, note that the InitializationChecker does not use the default convention where, e.g., the annotated type factory for NameChecker is NameAnnotatedTypeFactory. Instead every subclass of this checker always uses the InitializationAnnotatedTypeFactory unless this behavior is overridden. Note also that the flow-sensitive type refinement for this type system is performed by the InitializationFieldAccessSubchecker; this checker performs no refinement, instead reusing the results from that one.

See the Checker Framework Manual:
Initialization Checker

  • Constructor Details

    • InitializationChecker

      public InitializationChecker()
      Default constructor for InitializationChecker.

  • Method Details

    • checkPrimitives

      public abstract boolean checkPrimitives()
      Whether to check primitives for initialization.
      Returns:
      whether to check primitives for initialization

    • getTargetCheckerClass

      public abstract Class<? extends BaseTypeChecker> getTargetCheckerClass()
      The checker for the target type system for which to check initialization.
      Returns:
      the checker for the target type system.

    • getSuppressWarningsPrefixes

      public NavigableSet<String> getSuppressWarningsPrefixes()
      Description copied from class: SourceChecker
      Returns a modifiable set of lower-case strings that are prefixes for SuppressWarnings strings.

      The collection must not be empty and must not contain only SourceChecker.SUPPRESS_ALL_PREFIX.

      Overrides:
      getSuppressWarningsPrefixes in class SourceChecker
      Returns:
      non-empty modifiable set of lower-case prefixes for SuppressWarnings strings

    • getImmediateSubcheckerClasses

      protected Set<Class<? extends BaseTypeChecker>> getImmediateSubcheckerClasses()
      Description copied from class: BaseTypeChecker
      Returns the set of subchecker classes on which this checker depends. Returns an empty set if this checker does not depend on any others.

      Subclasses should override this method to specify subcheckers. If they do so, they should call the super implementation of this method and add dependencies to the returned set so that checkers required for reflection resolution are included if reflection resolution is requested.

      Each subchecker of this checker may also depend on other checkers. If this checker and one of its subcheckers both depend on a third checker, that checker will only be instantiated once.

      Though each checker is run on a whole compilation unit before the next checker is run, error and warning messages are collected and sorted based on the location in the source file before being printed. (See BaseTypeChecker.printOrStoreMessage(Diagnostic.Kind, String, Tree, CompilationUnitTree).)

      WARNING: Circular dependencies are not supported nor do checkers verify that their dependencies are not circular. Make sure no circular dependencies are created when overriding this method. (In other words, if checker A depends on checker B, checker B cannot depend on checker A.)

      This method is protected so it can be overridden, but it should only be called internally by the BaseTypeChecker.

      The BaseTypeChecker will not modify the set returned by this method, but clients that override the method do modify the set.

      Overrides:
      getImmediateSubcheckerClasses in class BaseTypeChecker
      Returns:
      the subchecker classes on which this checker depends; will be modified by callees in overriding methods

    • getAllFields

      public static List<VariableTree> getAllFields(ClassTree clazz)
      Returns a list of all fields of the given class.
      Parameters:
      clazz - the class
      Returns:
      a list of all fields of clazz

    • getTypeFactory

      public InitializationAnnotatedTypeFactory getTypeFactory()
      Description copied from class: BaseTypeChecker
      Return the type factory associated with this checker.
      Overrides:
      getTypeFactory in class BaseTypeChecker
      Returns:
      the type factory associated with this checker

    • createSourceVisitor

      protected InitializationVisitor createSourceVisitor()
      Description copied from class: BaseTypeChecker
      Returns the appropriate visitor that type-checks the compilation unit according to the type system rules.

      This implementation uses the checker naming convention to create the appropriate visitor. If no visitor is found, it returns an instance of BaseTypeVisitor. It reflectively invokes the constructor that accepts this checker and the compilation unit tree (in that order) as arguments.

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

      Overrides:
      createSourceVisitor in class BaseTypeChecker
      Returns:
      the type-checking visitor

    • messageKeyMatches

      protected boolean messageKeyMatches(String messageKey, String messageKeyInSuppressWarningsString)
      Description copied from class: SourceChecker
      Does the given messageKey match a messageKey that appears in a SuppressWarnings? Subclasses should override this method if they need additional logic to compare message keys.
      Overrides:
      messageKeyMatches in class SourceChecker
      Parameters:
      messageKey - the message key
      messageKeyInSuppressWarningsString - the message key in a SuppressWarnings
      Returns:
      true if the arguments match