The Checker Framework Manual:
Custom pluggable types for Java

Chapter 3 Nullness Checker

If the Nullness Checker issues no warnings for a given program, then running that program will never throw a null pointer exception. In other words, the Nullness Checker prevents all NullPointerExceptions. See Section 3.1 for more details about the guarantee and what is checked.

The most important annotations supported by the Nullness Checker are @NonNull and @Nullable. @NonNull is rarely written, because it is the default. All of the annotations are explained in Section 3.2.

To run the Nullness Checker, supply the -processor org.checkerframework.checker.nullness.NullnessChecker command-line option to javac. For examples, see Section 3.5.

The NullnessChecker is actually an ensemble of three pluggable type-checkers that work together: the Nullness Checker proper (which is the main focus of this chapter), the Initialization Checker (Section 3.8), and the Map Key Checker (Chapter 4). Their type hierarchies are completely independent, but they work together to provide precise nullness checking.

3.1 What the Nullness Checker guarantees

If the Nullness Checker type-checks your program without errors, then your program will not crash with a NullPointerException that is caused by misuse of null in checked code. Section 2.3 notes some limitations to guarantees made by the Checker Framework.

The checker issues a warning in these cases:

• 1. When an expression of non-@NonNull type is dereferenced, because it might cause a null pointer exception. Dereferences occur not only when a field is accessed, but when an array is indexed, an exception is thrown, a lock is taken in a synchronized block, and more. For a complete description of all checks performed by the Nullness Checker, see the Javadoc for NullnessVisitor.

• 2. When an expression of @NonNull type might become null, because it is a misuse of the type: the null value could flow to a dereference that the checker does not warn about.

  As a special case of a @NonNull type becoming null, the checker also warns whenever a field of @NonNull type is not initialized in a constructor.

This example illustrates the programming errors that the checker detects:

    @Nullable Object   obj; // might    be null
    @NonNull Object nnobj; // never     null
    ...
    obj.toString()         // checker   warning:   dereference might cause null pointer exception
    nnobj = obj;           // checker   warning:   nnobj may become null
    if (nnobj == null)     // checker   warning:   redundant test

Parameter passing and return values are checked analogously to assignments.

The Nullness Checker also checks the correctness, and correct use, of initialization (see Section 3.8) and of map key annotations (see Chapter 4).

The checker performs additional checks if certain -Alint command-line options are provided. (See Section 34.7 for more details about the -Alint command-line option.)

3.1.1 Nullness Checker optional warnings

• 1. Options that control soundness:

  • • If you supply the -Alint=soundArrayCreationNullness command-line option, then the checker warns if it encounters an array creation with a non-null component type. See Section 3.3.4 for a discussion.

  • • If you supply the -Astubs=collection-object-parameters-may-be-null.astub command-line option, then in JDK collection classes, the checker unsoundly permits null as an argument for any key or value formal parameter whose type is Object (instead of the element type). See Section 3.4.2.

  • • If you supply the -Alint=trustArrayLenZero command-line option, then the checker will trust @ArrayLen(0) annotations. See Section 3.3.5 for a discussion.

  • • If you supply the -AassumeKeyFor command-line option, then the checker will unsoundly assume that the argument to Map.get is a key for the receiver map. It will not do any checking of @KeyFor and related qualifiers.

  • • If you supply the -AinvocationPreservesArgumentNullness command-line option, the Nullness Checker unsoundly assumes that arguments passed to non-null parameters in an invocation remain non-null after the invocation. This assumption is unsound in general, but holds for most code. For other ways to suppress warnings related to method side effects, see Section 33.7.5.

• 2. Options that warn about poor code style:

  • • If you supply the -Alint=redundantNullComparison command-line option, then the checker warns when a null check is performed against a value that is guaranteed to be non-null, as in ("m" == null). Such a check is unnecessary and might indicate a programmer error or misunderstanding. The lint option is disabled by default because sometimes such checks are part of ordinary defensive programming.

• 3. Options that enable checking modes:

  • • If you supply the -Alint=permitClearProperty command-line option, then the checker permits calls to System.setProperties() and calls to System.clearProperty that might clear one of the built-in properties.

    By default, the checker forbids calls to those methods, and also special-cases type-checking of calls to System.getProperty() and System.setProperties(). A call to one of these methods can return null in general, but by default the Nullness Checker treats it as returning non-null if the argument is one of the literal strings listed in the documentation of System.getProperties(). To make this behavior sound, the Nullness Checker forbids calls that might clear any built-in property, as described above.

3.2 Nullness annotations

The Nullness Checker uses three separate type hierarchies: one for nullness, one for initialization (Section 3.8), and one for map keys (Chapter 4). The Nullness Checker has four varieties of annotations: nullness type qualifiers, nullness method annotations, initialization type qualifiers, and map key type qualifiers.

3.2.1 Nullness qualifiers

The nullness hierarchy contains these qualifiers:

@Nullable

indicates a type that includes the null value. For example, the Java type Boolean is nullable: a variable of type Boolean always has one of the values TRUE, FALSE, or null. (Since @NonNull is the default type annotation, you would actually write this type as @Nullable Boolean.)

@NonNull

indicates a type that does not include the null value. The type boolean is non-null; a variable of type boolean always has one of the values true or false. The type @NonNull Boolean is also non-null: a variable of type @NonNull Boolean always has one of the values TRUE or FALSE — never null. Dereferencing an expression of non-null type can never cause a null pointer exception.

The @NonNull annotation is rarely written in a program, because it is the default (see Section 3.3.2).

@PolyNull

indicates qualifier polymorphism. For a description of qualifier polymorphism, see Section 32.2.

@MonotonicNonNull

indicates a reference that may be null, but if it ever becomes non-null, then it never becomes null again. This is appropriate for lazily-initialized fields, for field initialization that occurs in a lifecycle method other than the constructor (e.g., an override of android.app.Activity.onCreate), and other uses. @MonotonicNonNull is typically written on field types, but not elsewhere.

The benefit of @MonotonicNonNull over @Nullable is that after a check of a @MonotonicNonNull field, all subsequent accesses within that method can be assumed to be @NonNull, even after arbitrary external method calls that have access to the given field. By contrast, for a @Nullable field, the Nullness Checker assumes that most method calls might set it to null. (Exceptions are calls to methods that are @SideEffectFree, or that have an @EnsuresNonNull or @EnsuresNonNullIf annotation.)

A @MonotonicNonNull field may be initialized to null, but the field may not be assigned to null anywhere else in the program. If you supply the noInitForMonotonicNonNull lint flag (for example, supply -Alint=noInitForMonotonicNonNull on the command line), then @MonotonicNonNull fields are not allowed to have initializers at their declarations.

Use of @MonotonicNonNull on a static field is a code smell: it may indicate poor design. You should consider whether it is possible to make the field a member field that is set in the constructor.

In the type system, @MonotonicNonNull is a supertype of @NonNull and a subtype of @Nullable.

Figure 3.1 shows part of the type hierarchy for the Nullness type system. (The annotations exist only at compile time; at run time, Java has no multiple inheritance.)

3.2.2 Nullness method annotations

The Nullness Checker supports several annotations that specify method behavior. These are declaration annotations, not type annotations: they apply to the method itself rather than to some particular type.

@RequiresNonNull

indicates a method precondition. The annotated method expects the specified variables to be non-null when the method is invoked. Don’t use this for formal parameters (just annotate their type as @NonNull). @RequiresNonNull is appropriate for a field that is @Nullable in general, but some method requires the field to be non-null.

@EnsuresNonNull

indicates a method postcondition. With @EnsuresNonNull, the successful return (i.e., a non-exceptional return) of the annotated method results in the given expressions being non-null. See the Javadoc for examples of its use.

@EnsuresNonNullIf

indicates a method postcondition. With @EnsuresNonNull, the given expressions are non-null after the method returns; this is useful for a method that initializes a field, for example. With @EnsuresNonNullIf, if the annotated method returns the given boolean value (true or false), then the given expressions are non-null. See Section 3.3.3 and the Javadoc for examples of their use.

3.2.3 Initialization qualifiers

The Nullness Checker invokes an Initialization Checker, whose annotations indicate whether an object is fully initialized — that is, whether all of its fields have been assigned.

@Initialized

@UnknownInitialization

@UnderInitialization

Use of these annotations can help you to type-check more code. Figure 3.5 shows their type hierarchy. For details, see Section 3.8.

3.2.4 Map key qualifiers

@KeyFor

indicates that a value is a key for a given map — that is, that map.containsKey(value) would evaluate to true.

This annotation is checked by a Map Key Checker (Chapter 4) that the Nullness Checker invokes. The @KeyFor annotation enables the Nullness Checker to treat calls to Map.get precisely rather than assuming it may always return null. In particular, a call mymap.get(mykey) returns a non-null value if two conditions are satisfied:

• 1. mymap’s values are all non-null; that is, mymap was declared as Map<KeyType, @NonNull ValueType>. Note that @NonNull is the default type, so it need not be written explicitly.

• 2. mykey is a key in mymap; that is, mymap.containsKey(mykey) returns true. You express this fact to the Nullness Checker by declaring mykey as @KeyFor("mymap") KeyType mykey. For a local variable, you generally do not need to write the @KeyFor("mymap") type qualifier, because it can be inferred.

If either of these two conditions is violated, then mymap.get(mykey) has the possibility of returning null.

The command-line argument -AassumeKeyFor makes the Nullness Checker not run the Map Key Checker. The Nullness Checker will unsoundly assume that the argument to Map.get is a key for the receiver map. That is, the second condition above is always considered to be true.

3.3 Writing nullness annotations

3.3.1 Implicit qualifiers

The Nullness Checker adds implicit qualifiers, reducing the number of annotations that must appear in your code (see Section 33.4). For example, enum types are implicitly non-null, so you never need to write @NonNull MyEnumType.

If you want details about implicitly-added nullness qualifiers, see the implementation of NullnessAnnotatedTypeFactory.

3.3.2 Default annotation

Unannotated references are treated as if they had a default annotation. All types default to @NonNull, except that @Nullable is used for casts, locals, instanceof, and implicit bounds (see Section 33.5.3). A user can choose a different defaulting rule by writing a @DefaultQualifier annotation on a package, class, or method. In the example below, fields are defaulted to @Nullable instead of @NonNull.

@DefaultQualifier(value = Nullable.class, locations = TypeUseLocation.FIELD)
class MyClass {
    Object nullableField = null;
    @NonNull Object nonNullField = new Object();
}

3.3.3 Conditional nullness

The Nullness Checker supports a form of conditional nullness types, via the @EnsuresNonNullIf method annotations. The annotation on a method declares that some expressions are non-null, if the method returns true (false, respectively).

Consider java.lang.Class. Method Class.getComponentType() may return null, but it is specified to return a non-null value if Class.isArray() is true. You could declare this relationship in the following way (this particular example is already done for you in the annotated JDK that comes with the Checker Framework):

    class Class<T> {
      @EnsuresNonNullIf(expression="getComponentType()", result=true)
      public native boolean isArray();

        public native @Nullable Class<?> getComponentType();
    }

A client that checks that a Class reference is indeed that of an array can then dereference the result of Class.getComponentType safely without any nullness check. The Checker Framework source code itself uses such a pattern:

    if (clazz.isArray()) {
      // no possible null dereference on the following line
      TypeMirror componentType = typeFromClass(clazz.getComponentType());
      ...
    }

Another example is Queue.peek and Queue.poll, which return non-null if isEmpty returns false.

The argument to @EnsuresNonNullIf is a Java expression, including method calls (as shown above), method formal parameters, fields, etc.; for details, see Section 33.8. More examples of the use of these annotations appear in the Javadoc for @EnsuresNonNullIf.

Java programs sometimes contain more complex nullness invariants. When these invariants are more complex than handled by the Nullness Checker, you will need to suppress a warning (see Section 3.4).

3.3.4 Nullness and array initialization

Suppose that you declare an array to contain non-null elements:

    Object [] oa = new Object[10];

(recall that Object means the same thing as @NonNull Object). By default, the Nullness Checker unsoundly permits this code.

To make the Nullness Checker conservatively reject code that may leave a null value in an array of non-null element type, use the command-line option -Alint=soundArrayCreationNullness. The option is currently disabled because it makes the checker issue many false positive errors.

With the option enabled, you can write your code to create a nullable or @MonotonicNonNull array, initialize each component, and then assign the result to a non-null array:

    @MonotonicNonNull Object [] temp = new @MonotonicNonNull Object[10];
    for (int i = 0; i < temp.length; ++i) {
      temp[i] = new Object();
    }
    @SuppressWarnings("nullness") // temp array is now fully initialized
    @NonNull Object [] oa = temp;

Note that the checker is currently not powerful enough to ensure that each array component was initialized. Therefore, the last assignment needs to be trusted: that is, a programmer must verify that it is safe, then write a @SuppressWarnings annotation.

3.3.5 Nullness and conversions from collections to arrays

The nullness semantics of Collection.toArray(T[]) cannot be captured by just the nullness type system, though the Nullness Checker contains special-case code to type-check calls to toArray. Therefore, you will probably have to write @SuppressWarnings("nullness") on any overriding definitions of toArray.

The nullness type of the returned array depends on the size of the passed parameter. In particular, the returned array’s component type is @NonNull if the following conditions hold:

• • The receiver collection’s type argument (that is, the element type) is @NonNull, and

• • The passed array size is less than or equal to the collection size. The Nullness Checker uses these heuristics to handle the most common cases:

  • – the argument has length 0:

    • * an empty array initializer, e.g., c.toArray(new String[] {}), or

    • * array creation tree of size 0, e.g., c.toArray(new String[0]).

  • – array creation tree with a collection size() method invocation as argument c.toArray(new String[c.size()]).

Additionally, when you supply the -Alint=trustArrayLenZero command-line option, a call to Collection.toArray will be estimated to return an array with a non-null component type if the argument is a field access where the field declaration has a @ArrayLen(0) annotation. This trusts the @ArrayLen(0) annotation, but does not verify it. Run the Constant Value Checker (see Chapter 24) to verify that annotation.

Note: The nullness of the returned array doesn’t depend on the nullness of the passed array. This is a fact about Collection.toArray(T[]), not a limitation of this heuristic.

3.3.6 Run-time checks for nullness

When you perform a run-time check for nullness, such as if (x != null) ..., then the Nullness Checker refines the type of x to @NonNull. The refinement lasts until the end of the scope of the test or until x may be side-effected. For more details, see Section 33.7.

3.3.7 Inference of @NonNull and @Nullable annotations

It can be tedious to write annotations in your code. Tools exist that can automatically infer annotations and insert them in your source code. (This is different than type qualifier refinement for local variables (Section 33.7), which infers more specific types for local variables and uses them during type-checking but does not insert them in your source code. Type qualifier refinement is always enabled, no matter how annotations on signatures got inserted in your source code.)

Your choice of tool depends on what default annotation (see Section 3.3.2) your code uses. You only need one of these tools.

• • Inference of @Nullable: If your code uses the standard CLIMB-to-top default (Section 33.5.3) or the NonNull default, then use the AnnotateNullable tool of the Daikon invariant detector.

• • Inference of @NonNull: If your code uses the Nullable default (this is unusual), use one of these tools:

  • – Non-null checker and inferencer of the JastAdd Extensible Compiler.

3.4 Suppressing nullness warnings

When the Nullness Checker reports a warning, it’s best to change the code or its annotations, to eliminate the warning. Alternately, you can suppress the warning, which does not change the code but prevents the Nullness Checker from reporting this particular warning to you.

The Checker Framework supplies several ways to suppress warnings, most notably the @SuppressWarnings("nullness") annotation (see Chapter 34). An example use is

    // might return null
    @Nullable Object getObject(...) { ... }

    void myMethod() {
      @SuppressWarnings("nullness") // with argument x, getObject always returns a non-null value
      @NonNull Object o2 = getObject(x);
    }

The Nullness Checker supports an additional warning suppression string, nullness:generic.argument. Use of @SuppressWarnings("nullness:generic.argument") causes the Nullness Checker to suppress warnings related to misuse of generic type arguments. One use for this key is when a class is declared to take only @NonNull type arguments, but you want to instantiate the class with a @Nullable type argument, as in List<@Nullable Object>.

The Nullness Checker also permits you to use assertions or method calls to suppress warnings; see below.

3.4.1 Suppressing warnings with assertions and method calls

Occasionally, it is inconvenient or verbose to use the @SuppressWarnings annotation. For example, Java does not permit annotations such as @SuppressWarnings to appear on statements, expressions, static initializers, etc. Here are three ways to suppress a warning in such cases:

• • Create a local variable to hold a subexpression, and suppress a warning on the local variable declaration.

• • Use the @AssumeAssertion string in an assert message (see Section 34.2).

• • Write a call to the NullnessUtil.castNonNull method.

The rest of this section discusses the castNonNull method. It is useful if you wish to suppress a warning within an expression.

The Nullness Checker considers both the return value and the argument to be non-null after the castNonNull method call. The Nullness Checker issues no warnings in any of the following code:

    // One way to use castNonNull as a cast:
    @NonNull String s = castNonNull(possiblyNull1);

    // Another way to use castNonNull as a cast:
    castNonNull(possiblyNull2).toString();

    // It is possible, but not recommended, to use castNonNull as a statement:
    // (It would be better to write an assert statement with @AssumeAssertion
    // in its message, instead.)
    castNonNull(possiblyNull3);
    possiblyNull3.toString();

The castNonNull method throws AssertionError if Java assertions are enabled and the argument is null. However, it is not intended for general defensive programming; see Section 34.2.1.

To use the castNonNull method, the checker-util.jar file must be on the classpath at run time.

The Nullness Checker introduces a new method, rather than re-using an existing method such as org.junit.Assert.assertNotNull(Object) or com.google.common.base.Preconditions.checkNotNull(Object). Those methods are commonly used for defensive programming, so it is impossible to know the programmer’s intent when writing them. Therefore, it is important to have a method call that is used only for warning suppression. See Section 34.2.1 for a discussion of the distinction between warning suppression and defensive programming.

3.4.2 Null arguments to collection classes

For collection methods with Object formal parameter type, such as contains, indexOf, and remove, the annotated JDK forbids null as an argument.

The reason is that some implementations (like ConcurrentHashMap) throw NullPointerException if null is passed. It would be unsound to permit null, because it could lead to a false negative: the Checker Framework issuing no warning even though a NullPointerException can occur at run time.

However, many other common implementations permit such calls, so some users may wish to sacrifice soundness for a reduced number of false positive warnings. To permit null as an argument to these methods, pass the command-line argument -Astubs=collection-object-parameters-may-be-null.astub.

3.4.3 Conservative nullness annotations on the JDK

The JDK contains nullness annotations that preserve the Nullness Checker’s guarantee (see Section 3.1) that your program will not crash with a NullPointerException. A formal parameter may be null in some circumstances, but must be non-null in other circumstances, and those circumstances are not expressible using the Nullness Checker’s annotations.

An example is restrictions on collection arguments (see Section 3.4.2).

Another example is this WeakReference constructor:

     ...
     * @param q the queue with which the reference is to be registered,
     *          or {@code null} if registration is not required
     */
    public WeakReference(@Nullable T referent, ReferenceQueue<? super T> q) {
       ...

For some calls, q must be non-null. Therefore, q is annotated as @NonNull (which is the default and need not be explicitly written).

These JDK annotations reflect a verification philosophy: a verification tool finds all possible errors, but it sometimes issues a false positive warning. An alternate philosophy is a bug-finding philosophy: permit all calls that might be correct at run time, but sometimes miss a real error. If you wish to use the Checker Framework with the bug-finding philosophy (though the Checker Framework is still much more thorough than other bug-finders), you can do so by passing the command-line argument -Astubs=sometimes-nullable.astub.

3.5 Examples

3.5.1 Tiny examples

To try the Nullness Checker on a source file that uses the @NonNull qualifier, use the following command (where javac is the Checker Framework compiler that is distributed with the Checker Framework, see Section 39.6 for details):

    javac -processor org.checkerframework.checker.nullness.NullnessChecker docs/examples/NullnessExample.java

Compilation will complete without warnings.

To see the checker warn about incorrect usage of annotations (and therefore the possibility of a null pointer exception at run time), use the following command:

    javac -processor org.checkerframework.checker.nullness.NullnessChecker docs/examples/NullnessExampleWithWarnings.java

The compiler will issue two warnings regarding violation of the semantics of @NonNull.

3.5.2 Example annotated source code

Some libraries that are annotated with nullness qualifiers are:

• • The Nullness Checker itself.

• • The Java projects in the plume-lib GitHub organization. Type-checking occurs on each build.

• • The Daikon invariant detector. Run the command make check-nullness.

3.5.3 Publications

The papers “Practical pluggable types for Java” [PAC⁺08] (ISSTA 2008, https://homes.cs.washington.edu/~mernst/pubs/pluggable-checkers-issta2008.pdf) and “Building and using pluggable type-checkers” [DDE⁺11] (ICSE 2011, https://homes.cs.washington.edu/~mernst/pubs/pluggable-checkers-icse2011.pdf) describe case studies in which the Nullness Checker found previously-unknown errors in real software.

3.6 Tips for getting started

Here are some tips about getting started using the Nullness Checker on a legacy codebase. For more generic advice (not specific to the Nullness Checker), see Section 2.4.2. Also see the Checker Framework tutorial, which includes an example of using the Nullness Checker.

Your goal is to add @Nullable annotations to the types of any variables that can be null. (The default is to assume that a variable is non-null unless it has a @Nullable annotation.) Then, you will run the Nullness Checker. Each of its errors indicates either a possible null pointer exception, or a wrong/missing annotation. When there are no more warnings from the checker, you are done!

We recommend that you start by searching the code for occurrences of null in the following locations; when you find one, write the corresponding annotation:

• • in Javadoc: add @Nullable annotations to method signatures (parameters and return types).

• • return null: add a @Nullable annotation to the return type of the given method.

• • param == null: when a formal parameter is compared to null, then in most cases you can add a @Nullable annotation to the formal parameter’s type.

• • TypeName field = null;: when a field is initialized to null in its declaration, then it needs either a @Nullable or a @MonotonicNonNull annotation. If the field is always set to a non-null value in the constructor, then you can just change the declaration to Type field;, without an initializer, and write no type annotation (because the default is @NonNull).

• • declarations of contains, containsKey, containsValue, equals, get, indexOf, lastIndexOf, and remove (with Object as the argument type): change the argument type to @Nullable Object; for remove, also change the return type to @Nullable Object.

You should ignore all other occurrences of null within a method body. In particular, you rarely need to annotate local variables (except their type arguments or array element types).

Only after this step should you run the Nullness Checker. The reason is that it is quicker to search for places to change than to repeatedly run the checker and fix the errors it tells you about, one at a time.

Here are some other tips:

• •

  In any file where you write an annotation such as @Nullable, don’t forget to add import org.checkerframework.checker.nullness.qual.*;.

• • To indicate an array that can be null, write, for example: int @Nullable [].
  By contrast, @Nullable Object [] means a non-null array that contains possibly-null objects.

• • If you know that a particular variable is definitely not null, but the Nullness Checker estimates that the variable might be null, then you can make the Nullness Checker trust your judgment by writing an assertion (see Section 34.2):

  assert var != null : "@AssumeAssertion(nullness)";
  

• • To indicate that a routine returns the same value every time it is called, use @Pure (see Section 33.7.5).

• • To indicate a method precondition (a contract stating the conditions under which a client is allowed to call it), you can use annotations such as @RequiresNonNull (see Section 3.2.2).

3.7 Other tools for nullness checking

The Checker Framework’s nullness annotations are similar to annotations used in other tools. You might prefer to use the Checker Framework because it has a more powerful analysis that can warn you about more null pointer errors in your code. Most of the other tools are bug-finding tools rather than verification tools, since they give up precision, soundness, or both in favor of being fast and easy to use. Also see Section 40.10.1 for a comparison to other tools.

If your code is already annotated with a different nullness annotation, the Checker Framework can type-check your code. It treats annotations from other tools as if you had written the corresponding annotation from the Nullness Checker, as described in Figures 3.2, 3.3, and 3.4. If the other annotation is a declaration annotation, it may be moved; see Section 40.6.10.

The Checker Framework may issue more or fewer errors than another tool. This is expected, since each tool uses a different analysis. Remember that the Checker Framework aims at soundness: it aims to never miss a possible null dereference, while at the same time limiting false reports. Also, note SpotBugs’s non-standard meaning for @Nullable (Section 3.7.2).

Java permits you to import at most one annotation of a given name. For example, if you use both android.annotation.NonNull and lombok.NonNull in your source code, then you must write at least one of them in fully-qualified form, as @android.annotation.NonNull rather than as @NonNull.

3.7.1 Which tool is right for you?

Different tools are appropriate in different circumstances. Section 40.10.1 compares verification tools like the Checker Framework with bug detectors like SpotBugs and Error Prone. In brief, a bug detector is easier to use because it requires fewer annotations, but it misses lots of real bugs that a verifier finds. You should use whichever tool is appropriate for the importance of your code.

You may also choose to use multiple tools, especially since each tool focuses on different types of errors. If you know that you will eventually want to do verification for some particular task (say, nullness checking), there is little point using the nullness analysis of a bug detector such as SpotBugs first. It is easier to go straight to using the Checker Framework.

If some other tool discovers a nullness error that the Checker Framework does not, please report it to us (see Section 41.2) so that we can enhance the Checker Framework. For example, SpotBugs might detect an error that the Nullness Checker does not, if you are using an unannotated library (including an unannotated part of the JDK) and running the Checker Framework in an unsound mode (see Section 2.2.2).

3.7.2 Incompatibility note about FindBugs and SpotBugs @Nullable

FindBugs and SpotBugs have a non-standard definition of @Nullable. This treatment is not documented in the annotation’s own Javadoc; it is different from the definition of @Nullable in every other tool for nullness analysis; it means the same thing as @NonNull when applied to a formal parameter; and it invariably surprises programmers. Thus, SpotBugs’s @Nullable is detrimental rather than useful as documentation. In practice, your best bet is to not rely on SpotBugs for nullness analysis, even if you find SpotBugs useful for other purposes.

You can skip the rest of this section unless you wish to learn more details.

SpotBugs suppresses all warnings at uses of a @Nullable variable. (You have to use @CheckForNull to indicate a nullable variable that SpotBugs should check.) For example:

       // declare getObject() to possibly return null
       @Nullable Object getObject() { ... }

       void myMethod() {
         @Nullable Object o = getObject();
         // SpotBugs issues no warning about calling toString on a possibly-null reference!
         o.toString();
       }

The Checker Framework does not emulate this non-standard behavior of SpotBugs, even if the code uses FindBugs/SpotBugs annotations.

With SpotBugs, you annotate a declaration, which suppresses checking at all client uses, even the places that you want to check. It is better to suppress warnings at only the specific client uses where the value is known to be non-null; the Checker Framework supports this, if you write @SuppressWarnings at the client uses. The Checker Framework also supports suppressing checking at all client uses, by writing a @SuppressWarnings annotation at the declaration site. Thus, the Checker Framework supports both use cases, whereas SpotBugs supports only one and gives the programmer less flexibility.

In general, the Checker Framework will issue more warnings than SpotBugs, and some of them may be about real bugs in your program. See Section 3.4 for information about suppressing nullness warnings.

FindBugs and SpotBugs made a poor choice of names. The choice of names should have made a clear distinction between annotations that specify whether a reference is null, and annotations that suppress false warnings. The choice of names should also have been consistent with other tools, and intuitively clear to programmers. The FindBugs/SpotBugs choices make the SpotBugs annotations less helpful to people, and much less useful for other tools.

Another problem is that the SpotBugs @Nullable annotation is a declaration annotation rather than a type annotation. This means that it cannot be written in important locations such as type arguments, and it is misleading when written on a field of array type or a method that returns an array.

Overall, it is best to stay away from the SpotBugs nullness annotations and analysis, and use a tool with a more principled design.

3.7.3 Relationship to Optional<T>

Many null pointer exceptions occur because the programmer forgets to check whether a reference is null before dereferencing it. Java 8’s Optional<T> class provides a partial solution: a programmer must call the get method to access the value, and the designers of Optional hope that the syntactic occurrence of the get method will remind programmers to first check that the value is present. This is still easy to forget, however.

The Checker Framework contains an Optional Checker (see Chapter 5) that guarantees that programmers use Optional correctly, such as calling isPresent before calling get.

There are some limitations to the utility of Optional, which might lead you to choose to use regular Java references rather than Optional. (For more details, see the article “Nothing is better than the Optional type”.)

• • It is still possible to call get on a non-present Optional, leading to a NoSuchElementException. In other words, Optional doesn’t solve the underlying problem — it merely converts a NullPointerException into a NoSuchElementException, and in either case your code crashes.

• • NullPointerException is still possible in code that uses Optional.

• • Optional adds syntactic complexity, making your code longer and harder to read.

• • Optional adds time and space overhead.

• • Optional does not address important sources of null pointer exceptions, such as partially-initialized objects and calls to Map.get.

The Nullness Checker does not suffer these limitations. Furthermore, it works with existing code and types, it ensures that you check for null wherever necessary, and it infers when the check for null is not necessary based on previous statements in the method.

Java’s Optional class provides utility routines to reduce clutter when using Optional. The Nullness Checker provides an Opt class that provides all the same methods, but written for regular possibly-null Java references. To use the Opt class, the checker-util.jar file must be on the classpath at run time.

3.8 Initialization Checker

The Initialization Checker determines whether an object is initialized or not. For any object that is not fully initialized, the Nullness Checker treats its fields as possibly-null — even fields annotated as @NonNull. (The Initialization Checker focuses on @NonNull fields, to detect null pointer exceptions when using them. It does not currently ensure that primitives or @Nullable fields are initialized. Use the Initialized Fields Checker (Chapter 27) to check initialization with respect to properties other than nullness.)

Every object’s fields start out as null. By the time the constructor finishes executing, the @NonNull fields have been set to a different value. Your code can suffer a NullPointerException when using a @NonNull field, if your code uses the field during initialization. The Nullness Checker prevents this problem by warning you anytime that you may be accessing an uninitialized field. This check is useful because it prevents errors in your code. However, the analysis can be confusing to understand. If you wish to disable the initialization checks, see Section 3.8.8.

An object is partially initialized from the time that its constructor starts until its constructor finishes. This is relevant to the Nullness Checker because while the constructor is executing — that is, before initialization completes — a @NonNull field may be observed to be null, until that field is set. In particular, the Nullness Checker issues a warning for code like this:

    public class MyClass {
      private @NonNull Object f;
      public MyClass(int x) {
        // Error because constructor contains no assignment to this.f.
        // By the time the constructor exits, f must be initialized to a non-null value.
      }
      public MyClass(int x, int y) {
        // Error because this.f is accessed before f is initialized.
        // At the beginning of the constructor's execution, accessing this.f
        // yields null, even though field f has a non-null type.
        this.f.toString();
        f = new Object();
      }
      public MyClass(int x, int y, int z) {
        m();
        f = new Object();
      }
      public void m() {
        // Error because this.f is accessed before f is initialized,
        // even though the access is not in a constructor.
        // When m is called from the constructor, accessing f yields null,
        // even though field f has a non-null type.
        this.f.toString();
      }
    }

When a field f is declared with a @NonNull type, then code can depend on the fact that the field is not null. However, this guarantee does not hold for a partially-initialized object.

The Initialization Checker uses three annotations to indicate whether an object is initialized (all its @NonNull fields have been assigned), under initialization (its constructor is currently executing), or its initialization state is unknown.

These distinctions are mostly relevant within the constructor, or for references to this that escape the constructor (say, by being stored in a field or passed to a method before initialization is complete). Use of initialization annotations is rare in most code.

3.8.1 Initialization qualifiers

The initialization hierarchy is shown in Figure 3.5. The initialization hierarchy contains these qualifiers:

@Initialized

indicates a type that contains a fully-initialized object. Initialized is the default, so there is little need for a programmer to write this explicitly.

@UnknownInitialization

indicates a type that may contain a partially-initialized object. In a partially-initialized object, fields that are annotated as @NonNull may be null because the field has not yet been assigned.

@UnknownInitialization takes a parameter that is the class the object is definitely initialized up to. For instance, the type @UnknownInitialization(Foo.class) denotes an object in which every field declared in Foo or its superclasses is initialized, but other fields might not be. Just @UnknownInitialization is equivalent to @UnknownInitialization(Object.class).

@UnderInitialization

indicates a type that contains a partially-initialized object that is under initialization — that is, its constructor is currently executing. It is otherwise the same as @UnknownInitialization. Within the constructor, this has @UnderInitialization type until all the @NonNull fields have been assigned.

A partially-initialized object (this in a constructor) may be passed to a helper method or stored in a variable; if so, the method receiver, or the field, would have to be annotated as @UnknownInitialization or as @UnderInitialization.

If a reference has @UnknownInitialization or @UnderInitialization type, then all of its @NonNull fields are treated as @MonotonicNonNull: when read, they are treated as being @Nullable, but when written, they are treated as being @NonNull.

The initialization hierarchy is orthogonal to the nullness hierarchy. It is legal for a reference to be @NonNull @UnderInitialization, @Nullable @UnderInitialization, @NonNull @Initialized, or @Nullable @Initialized. The nullness hierarchy tells you about the reference itself: might the reference be null? The initialization hierarchy tells you about the @NonNull fields in the referred-to object: might those fields be temporarily null in contravention of their type annotation? Figure 3.6 contains some examples.

class C {
  @NonNull Object f;
  @Nullable Object g;
  ...
}

3.8.2 How an object becomes initialized

Within the constructor, this starts out with @UnderInitialization type. As soon as all of the @NonNull fields in class C have been initialized, then this is treated as @UnderInitialization(C). This means that this is still being initialized, but all initialization of C’s fields is complete, including all fields of supertypes. Eventually, when all constructors complete, the type is @Initialized.

The Initialization Checker issues an error if the constructor fails to initialize any @NonNull field. This ensures that the object is in a legal (initialized) state by the time that the constructor exits. This is different than Java’s test for definite assignment (see JLS ch.16), which does not apply to fields (except blank final ones, defined in JLS §4.12.4) because fields have a default value of null.

All @NonNull fields must either have a default in the field declaration, or be assigned in the constructor or in a helper method that the constructor calls. If your code initializes (some) fields in a helper method, you will need to annotate the helper method with an annotation such as @EnsuresNonNull({"field1", "field2"}) for all the fields that the helper method assigns.

3.8.3 @UnderInitialization examples

The most common use for the @UnderInitialization annotation is for a helper routine that is called by a constructor. For example:

    class MyClass {
      Object field1;
      Object field2;
      Object field3;

        public MyClass(String arg1) {
          this.field1 = arg1;
          init_other_fields();
        }

        // A helper routine that initializes all the fields other than field1.
        @EnsuresNonNull({"field2", "field3"})
        private void init_other_fields(@UnderInitialization(Object.class) MyClass this) {
          field2 = new Object();
          field3 = new Object();
        }

        public MyClass(String arg1, String arg2, String arg3) {
          this.field1 = arg1;
          this.field2 = arg2;
          this.field3 = arg3;
          checkRep();
        }

        // Verify that the representation invariants are satisfied.
        // Works as long as the MyClass fields are initialized, even if the receiver's
        // class is a subclass of MyClass and not all of the subclass fields are initialized.
        private void checkRep(@UnderInitialization(MyClass.class) MyClass this) {
          ...
        }



    }

At the end of the constructor, this is not fully initialized. Rather, it is @UnderInitialization(CurrentClass.class). The reason is that there might be subclasses with uninitialized fields. The following example illustrates this:

class A {
   @NonNull String a;
   public A() {
       a = "";
       // Now, all fields of A are initialized.
       // However, if this constructor is invoked as part of 'new B()', then
       // the fields of B are not yet initialized.
       // If we were to type 'this' as @Initialized, then the following call is valid:
       doSomething();
   }
   void doSomething() {}
}

class B extends A {
   @NonNull String b;
   @Override
   void doSomething() {
       // Dereferencing 'b' is ok, because 'this' is @Initialized and 'b' @NonNull.
       // However, when executing 'new B()', this line throws a null-pointer exception.
       b.toString();
   }
}

3.8.4 Partial initialization

So far, we have discussed initialization as if it is an all-or-nothing property: an object is uninitialized until initialization completes, and then it is initialized. The full truth is a bit more complex: during the initialization process an object can be partially initialized, and as the object’s superclass constructors complete, its initialization status is updated. The Initialization Checker lets you express such properties when necessary.

Consider a simple example:

class A {
  Object aField;
  A() {
    aField = new Object();
  }
}
class B extends A {
  Object bField;
  B() {
    super();
    bField = new Object();
  }
}

Consider what happens during execution of new B().

• 1. B’s constructor begins to execute. At this point, neither the fields of A nor those of B have been initialized yet.

• 2. B’s constructor calls A’s constructor, which begins to execute. No fields of A nor of B have been initialized yet.

• 3. A’s constructor completes. Now, all the fields of A have been initialized, and their invariants (such as that field a is non-null) can be depended on. However, because B’s constructor has not yet completed executing, the object being constructed is not yet fully initialized.

• 4. B’s constructor completes. The fields declared in A and B are initialized. However, the type system cannot assume that the object is fully initialized — there might be a class C extends B {...}, and B’s constructor might have been invoked from that.

At any moment during initialization, the superclasses of a given class can be divided into those that have completed initialization and those that have not yet completed initialization. More precisely, at any moment there is a point in the class hierarchy such that all the classes above that point are fully initialized, and all those below it are not yet initialized. As initialization proceeds, this dividing line between the initialized and uninitialized classes moves down the type hierarchy.

The Nullness Checker lets you indicate where the dividing line is between the initialized and uninitialized classes. The @UnderInitialization(classliteral) annotation indicates the first class that is known to be fully initialized. When you write @UnderInitialization(OtherClass.class) MyClass x;, that means that variable x is initialized for OtherClass and its superclasses, and x is (possibly) uninitialized for subclasses of OtherClass.

The example above lists 4 moments during construction. At those moments, the type of the object being constructed is:

• 1. @UnderInitialization B

• 2. @UnderInitialization A

• 3. @UnderInitialization(A.class) A

• 4. @UnderInitialization(B.class) B

Note that neither @UnderInitialization(A.class) A nor @UnderInitialization(A.class) B may be used where @Initialized A is required. Permitting that would be unsound. For example, consider this code, where all types are @NonNull because @NonNull is the default annotation:

class A {
  Object aField;
  A() {
    aField = new Object();
  }
  Object get() {
    return aField;
  }
}
class B extends A {
  Object bField;
  B() {
    super();
    bField = new Object();
  }
  @Override
  Object get() {
    return bField;
  }
}

Given these declarations:

@Initialized A w;
@Initialized B x;
@UnderInitialization(A.class) A y;
@UnderInitialization(A.class) B z;

the expressions w.get() and x.get() evaluate to a non-null value, but y.get() and z.get() might evaluate to null. (y.get() might evaluate to null because the run-time type of y might be B. That is, y and z might refer to the same value, just as w and x might refer to the same value.)

3.8.5 Method calls from the constructor

Consider the following incorrect program.

class A {
  Object aField;
  A() {
    aField = new Object();
    process(5); // illegal call
  }
  public void process(int arg) { ... }
}

The call to process() is not legal. process() is declared to be called on a fully-initialized receiver, which is the default if you do not write a different initialization annotation. At the call to process(), all the fields of A have been set, but this is not fully initialized because fields in subclasses of A have not yet been set. The type of this is @UnderInitialization(A.class), meaning that this is partially-initialized, with the A part of initialization done but the initialization of subclasses not yet complete.

The Initialization Checker output indicates this problem:

Client.java:7: error: [method.invocation] call to process(int) not allowed on the given receiver.
    process(5); // illegal call
           ^
  found   : @UnderInitialization(A.class) A
  required: @Initialized A

Here is a subclass and client code that crashes with a NullPointerException.

class B extends A {
  List<Integer> processed;
  B() {
    super();
    processed = new ArrayList<Integer>();
  }
  @Override
  public void process(int arg) {
    super.process(arg);
    processed.add(arg);
  }
}
class Client {
  public static void main(String[] args) {
    new B();
  }
}

You can correct the problem in multiple ways.

One solution is to not call methods that can be overridden from the constructor: move the call to process() to after the constructor has completed.

Another solution is to change the declaration of process():

    public void process(@UnderInitialization(A.class) A this, int arg) { ... }

If you choose this solution, you will need to rewrite the definition of B.process() so that it is consistent with the declared receiver type.

A non-solution is to prevent subclasses from overriding process() by using final on the method. This doesn’t work because even if process() is not overridden, it might call other methods that are overridden.

As final classes cannot have subclasses, they can be handled more flexibly: once all fields of the final class have been initialized, this is fully initialized.

3.8.6 Initialization of circular data structures

There is one final aspect of the initialization type system to be considered: the rules governing reading from and writing to objects that are currently under initialization (both reading from fields of objects under initialization and writing objects under initialization to fields). By default, only fully-initialized objects can be stored in a field of another object. If this were the only option, then it would not be possible to create circular data structures (such as a doubly-linked list) where fields have a @NonNull type. However, the annotation @NotOnlyInitialized can be used to indicate that a field can store objects that are currently under initialization. In this case, the rules for reading from and writing to that field become a little bit more interesting, to soundly support circular structures.

The rules for reading from a @NotOnlyInitialized field are summarized in Figure 3.7. Essentially, nothing is known about the initialization status of the value returned unless the receiver was @Initialized.

Similarly, Figure 3.8 shows under which conditions an assignment x.f = y is allowed for a @NotOnlyInitialized field f. If the receiver x is @UnderInitialization, then y can be of any initialization state. If y is known to be fully initialized, then any receiver is allowed. All other assignments are disallowed.

These rules allow for the safe initialization of circular structures. For instance, consider a doubly linked list:

    class List<T> {
      @NotOnlyInitialized
      Node<T> sentinel;

        public List() {
          this.sentinel = new Node<>(this);
        }

        void insert(@Nullable T data) {
          this.sentinel.insertAfter(data);
        }

        public static void main() {
          List<Integer> l = new List<>();
          l.insert(1);
          l.insert(2);
        }
    }

    class Node<T> {
      @NotOnlyInitialized
      Node<T> prev;

        @NotOnlyInitialized
        Node<T> next;

        @NotOnlyInitialized
        List<T> parent;

        @Nullable
        T data;

        // for sentinel construction
        Node(@UnderInitialization List<T> parent) {
          this.parent = parent;
          this.prev = this;
          this.next = this;
        }

        // for data node construction
        Node(Node<T> prev, Node<T> next, @Nullable T data) {
          this.parent = prev.parent;
          this.prev = prev;
          this.next = next;
          this.data = data;
        }

        void insertAfter(@Nullable T data) {
          Node<T> n = new Node<>(this, this.next, data);
          this.next.prev = n;
          this.next = n;
        }
    }

3.8.7 How to handle warnings

“error: the constructor does not initialize fields: …”

Like any warning, “error: the constructor does not initialize fields: …” indicates that either your annotations are incorrect or your code is buggy. You can fix either the annotations or the code.

• • Declare the field as @Nullable. Recall that if you did not write an annotation, the field defaults to @NonNull.

• • Declare the field as @MonotonicNonNull. This is appropriate if the field starts out as null but is later set to a non-null value. You may then wish to use the @EnsuresNonNull annotation to indicate which methods set the field, and the @RequiresNonNull annotation to indicate which methods require the field to be non-null.

• • Initialize the field in the constructor or in the field’s initializer, if the field should be initialized. (In this case, the Initialization Checker has found a bug!)

  Do not initialize the field to an arbitrary non-null value just to eliminate the warning. Doing so degrades your code: it introduces a value that will confuse other programmers, and it converts a clear NullPointerException into a more obscure error.

“call to … is not allowed on the given receiver”

If your code calls an instance method from a constructor, you may see a message such as the following:

MyFile.java:123: error: call to initHelper() not allowed on the given receiver.
    initHelper();
              ^
  found   : @UnderInitialization(com.google.Bar.class) @NonNull MyClass
  required: @Initialized @NonNull MyClass

The problem is that the current object (this) is under initialization, but the receiver formal parameter (Section 40.6.1) of method initHelper() is implicitly annotated as @Initialized. If initHelper() doesn’t depend on its receiver being initialized — that is, it’s OK to call x.initHelper even if x is not initialized — then you can indicate that by using @UnderInitialization or @UnknownInitialization.

class MyClass {
  void initHelper(@UnknownInitialization MyClass this, String param1) { ... }
}

You are likely to want to annotate initHelper() with @EnsuresNonNull as well; see Section 3.2.2.

You may get the “call to … is not allowed on the given receiver” error even if your constructor has already initialized all the fields. For this code:

public class MyClass {
  @NonNull Object field;
  public MyClass() {
    field = new Object();
    helperMethod();
  }
  private void helperMethod() {
  }
}

the Nullness Checker issues the following warning:

MyClass.java:7: error: call to helperMethod() not allowed on the given receiver.
    helperMethod();
                ^
  found   : @UnderInitialization(MyClass.class) @NonNull MyClass
  required: @Initialized @NonNull MyClass
1 error

The reason is that even though the object under construction has had all the fields declared in MyClass initialized, there might be a subclass of MyClass. Thus, the receiver of helperMethod should be declared as @UnderInitialization(MyClass.class), which says that initialization has completed for all the MyClass fields but may not have been completed overall. If helperMethod had been a public method that could also be called after initialization was actually complete, then the receiver should have type @UnknownInitialization, which is the supertype of @Initialized and @UnderInitialization.

3.8.8 Suppressing warnings

To suppress most warnings related to partially-initialized values, use the warning suppression string “initialization”. You can write @SuppressWarnings("initialization") on a field, constructor, or class, or pass the command-line argument -AsuppressWarnings=initialization when running the Nullness Checker. (For more about suppressing warnings, see Chapter 34.) You will no longer get a guarantee of no null pointer exceptions, but you can still use the Nullness Checker to find most of the null-pointer problems in your code.

This suppresses warnings that are specific to the Initialization Checker, but does not suppress warnings issued by the Checker Framework itself, such as about assignments or method overriding.

It is not possible to completely disable initialization checking while retaining nullness checking. That is because of an implementation detail of the Nullness and Initialization Checkers: they are actually the same checker, rather than being two separate checkers that are aggregated together.

3.8.9 More details about initialization checking

Use of method annotations

A method with an uninitialized receiver may assume that a few fields (but not all of them) are non-null, and it sometimes sets some more fields to non-null values. To express these concepts, use the @RequiresNonNull, @EnsuresNonNull, and @EnsuresNonNullIf method annotations; see Section 3.2.2.

Source of the type system

The type system enforced by the Initialization Checker is based on “Freedom Before Commitment” [SM11]. Our implementation changes its initialization modifiers (“committed”, “free”, and “unclassified”) to “initialized”, “unknown initialization”, and “under initialization”. Our implementation also has several enhancements. For example, it supports partial initialization (the argument to the @UnknownInitialization and @UnderInitialization annotations). The benefit (in terms of reduced false positive initialization warnings) from supporting partial initialization is greater than the benefit from adopting the Freedom Before Commitment system.