The Checker Framework Manual:
Custom pluggable types for Java

Chapter 27 Initialized Fields Checker

The Initialized Fields Checker warns if a constructor does not initialize a field.

27.1 Running the Initialized Fields Checker

An example invocation is

javac -processor org.checkerframework.common.initializedfields.InitializedFieldsChecker MyFile.java

If you run it together with other checkers, then it issues warnings only if the default value assigned by Java (0, false, or null) is not consistent with the field’s annotation, for the other checkers. An example invocation is

javac -processor ValueChecker,InitializedFieldsChecker MyFile.java

27.2 Motivation: uninitialized fields

Without the Initialized Fields Checker, every type system is unsound with respect to fields that are never set. (Exception: The Nullness Checker (Chapter 3) is sound. Also, a type system is sound if every annotation is consistent with 0, false, and null.) Consider the following code:

import org.checkerframework.checker.index.qual.Positive;

class MyClass {
  @Positive int x;
  MyClass() {
    // empty body
  }

    @Positive int getX() {
      return x;
    }
}

Method getX is incorrect because it returns 0, which is not positive. However, the code type-checks because there is never an assignment to x whose right-hand side is not positive. If you run the Index Checker together with the Initialized Fields Checker, then the code correctly does not type-check.

Remaining unsoundness

Even with the Initialized Fields Checker, every type system (except the Nullness Checker, Chapter 3) is unsound with respect to partially-initialized fields. Consider the following code:

import org.checkerframework.checker.index.qual.Positive;

class MyClass {
  @Positive int x;
  MyClass() {
    foo();
    x = 1;
  }

    @Positive int foo() {
      // ... use x, expecting it to be positive ...
    }
}

Within method foo, x can have the value 0 even though the type of x is @Positive int.

27.3 Example

As an example, consider the following code:

import org.checkerframework.checker.index.qual.Positive;

class MyClass {

    @Positive int x;
    @Positive int y;
    int z;

    // Warning: field y is not initialized
    MyClass() {
      x = 1;
    }
}

When run by itself, the Initialized Fields Checker warns that fields y and z are not set.

When run together with the Index Checker, the Initialized Fields Checker warns that field y is not set. It does not warn about field z, because its default value (0) is consistent with its annotations.

27.4 Annotations

The Initialized Fields type system uses the following type annotations:

@InitializedFields

indicates which fields have definitely been initialized so far.

@InitializedFieldsBottom

is the type of null. Programmers rarely write this type.

@PolyInitializedFields

is a qualifier that is polymorphic over field initialization. For a description of qualifier polymorphism, see Section 32.2.

Figure 27.1 shows the subtyping relationships among the type qualifiers.

There is also a method declaration annotation:

@EnsuresInitializedFields

indicates which fields the method sets. Use this for helper methods that are called from a constructor.

27.5 Comparison to the Initialization Checker

The Initialized Fields Checker is a lightweight version of the Initialization Checker (Section 3.8). Here is a comparison between them.

* See Section 27.2 for an example.
** The Initialization Checker could be made to work with any type system, but doing so would require changing the implementation of both the type system and the Initialization Checker.