org.checkerframework.checker.initialization.qual

Annotation Type UnknownInitialization

@Documented
 @Retention(value=RUNTIME)
 @Target(value={TYPE_USE,TYPE_PARAMETER})
 @SubtypeOf(value={})
 @DefaultFor(value={LOCAL_VARIABLE,RESOURCE_VARIABLE})
public @interface UnknownInitialization

This type qualifier indicates how much of an object has been fully initialized. An object is fully initialized when each of its fields contains a value that satisfies the field's declaration.

An expression of type @UnknownInitialization(T.class) refers to an object that has all fields of T (and any super-classes) initialized. Just @UnknownInitialization is equivalent to @UnknownInitialization(Object.class). Please see the manual for examples of how to use the annotation (the link appears below).

Reading a field of an object of type @UnknownInitialization might yield a value that does not correspond to the declared type qualifier for that field. For instance, consider a non-null field:

@NonNull Object f;

In a partially-initialized object, field f might be null despite its @NonNull type annotation.

What type qualifiers on the field are considered depends on the checker; for instance, the NullnessChecker considers NonNull. The initialization type system is not used on its own, but in conjunction with some other type-system that wants to ensure safe initialization.

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 @UnknownInitialization(T.class) has all type-frames initialized starting at Object down to (and including) T.

Returns:

the type whose fields are fully initialized

Default:

java.lang.Object.class