| package org.checkerframework.checker.initialization.qual; |
| |
| import java.lang.annotation.Documented; |
| import java.lang.annotation.ElementType; |
| import java.lang.annotation.Retention; |
| import java.lang.annotation.RetentionPolicy; |
| import java.lang.annotation.Target; |
| import org.checkerframework.checker.nullness.qual.NonNull; |
| import org.checkerframework.framework.qual.DefaultFor; |
| import org.checkerframework.framework.qual.SubtypeOf; |
| import org.checkerframework.framework.qual.TypeUseLocation; |
| |
| /** |
| * 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. |
| * |
| * <p>An expression of type {@code @UnknownInitialization(T.class)} refers to an object that has all |
| * fields of {@code T} (and any super-classes) initialized. Just {@code @UnknownInitialization} is |
| * equivalent to {@code @UnknownInitialization(Object.class)}. Please see the manual for examples of |
| * how to use the annotation (the link appears below). |
| * |
| * <p>Reading a field of an object of type {@code @UnknownInitialization} might yield a value that |
| * does not correspond to the declared type qualifier for that field. For instance, consider a |
| * non-null field: |
| * |
| * <pre>@NonNull Object f;</pre> |
| * |
| * In a partially-initialized object, field {@code f} might be {@code null} despite its |
| * {@literal @}{@link NonNull} type annotation. |
| * |
| * <p>What type qualifiers on the field are considered depends on the checker; for instance, the |
| * {@link org.checkerframework.checker.nullness.NullnessChecker} considers {@link 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. |
| * |
| * @checker_framework.manual #initialization-checker Initialization Checker |
| */ |
| @Documented |
| @Retention(RetentionPolicy.RUNTIME) |
| @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) |
| @SubtypeOf({}) |
| @DefaultFor({TypeUseLocation.LOCAL_VARIABLE, TypeUseLocation.RESOURCE_VARIABLE}) |
| public @interface UnknownInitialization { |
| /** |
| * The type-frame down to which the expression (of this type) has been initialized at least |
| * (inclusive). That is, an expression of type {@code @UnknownInitialization(T.class)} has all |
| * type-frames initialized starting at {@code Object} down to (and including) {@code T}. |
| * |
| * @return the type whose fields are fully initialized |
| */ |
| Class<?> value() default Object.class; |
| } |