org.checkerframework.checker.initialization.qual

Annotation Type UnderInitialization

@SubtypeOf(value=UnknownInitialization.class)
 @Documented
 @Retention(value=RUNTIME)
 @Target(value={TYPE_USE,TYPE_PARAMETER})
public @interface UnderInitialization

This type qualifier belongs to the freedom-before-commitment type-system for tracking initialization. This type-system is not used on its own, but in conjunction with some other type-system that wants to ensure safe initialization. For instance, NullnessChecker uses freedom-before-commitment to track initialization of NonNull fields.

This type qualifier indicates that the object is (definitely) under initialization at the moment and that no aliases that are typed differently exist.

Because the object is currently under initialization it is allowed to store potentially not fully initialized object in fields.

Similar to UnknownInitialization, this type qualifier supports type frames.

At the beginning of a constructor, the fields of the object are not yet initialized and thus UnknownInitialization(supertype) is used as the type of the self-reference this. Consider a class B that is a subtype of A. At the beginning of the constructor of B, this has the type @UnderInitialization(A.class), since all fields of A have been initialized by the super-constructor. If during the constructor also all fields of B are initialized, then the type of this changes to @UnderInitialization(B.class) (and otherwise, if not all fields are initialized, an error is issued).

Note that it would not be sound to type this as Initialized anywhere in a constructor (with the exception of final classes; but this is currently not implemented), because there might be subclasses with uninitialized fields. The following example shows why:

 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 would type 'this' as @Initialized, then the following call is valid:
        foo();
    }
    void foo() {}
 }

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

See the Checker Framework Manual:

Initialization Checker

Optional Element Summary

Optional Elements

Modifier and Type	Optional Element and Description
Class<?>	value The type-frame down to which the expression (of this type) has been initialized at least (inclusive).

Element Detail

value

public abstract Class<?> value

The type-frame down to which the expression (of this type) has been initialized at least (inclusive). That is, an expression of type @UnderInitialization(T.class) has all type-frames initialized starting at Object down to (and including) T.

Default:

java.lang.Object.class