Package org.checkerframework.framework.qual


package org.checkerframework.framework.qual
Contains the basic annotations to be used by all type systems and meta-annotations to qualify annotations (qualifiers).

They may serve as documentation for the type qualifiers, and aid the Checker Framework to infer the relations between the type qualifiers.

See the Checker Framework Manual:
Writing a checker
  • Class
    Description
    Indicates that this class has been annotated for the given type system.
    This annotation is for comments related to the Checker Framework.
    A meta-annotation that indicates that an annotation E is a conditional postcondition annotation, i.e., E is a type-specialized version of EnsuresQualifierIf or EnsuresQualifierIf.List.
    A marker annotation, written on a class declaration, that signifies that one or more of the class's type parameters can be treated covariantly.
    A meta-annotation applied to the declaration of a type qualifier.
    Applied to a declaration of a package, type, method, variable, etc., specifies that the given annotation should be the default.
    A wrapper annotation that makes the DefaultQualifier annotation repeatable.
    Declaration annotation applied to type declarations to specify the qualifier to be added to unannotated uses of the type.
    Indicates that the annotated qualifier is the default qualifier in the qualifier hierarchy: it applies if the programmer writes no explicit qualifier and no other default has been specified for the location.
    A postcondition annotation to indicate that a method ensures that certain expressions have a certain type qualifier once the method has successfully terminated.
    A wrapper annotation that makes the EnsuresQualifier annotation repeatable.
    A conditional postcondition annotation to indicate that a method ensures that certain expressions have a certain qualifier once the method has terminated, and if the result is as indicated by result.
    A wrapper annotation that makes the EnsuresQualifierIf annotation repeatable.
    Specifies that a field's type, in the class on which this annotation is written, is a subtype of its declared type.
    If a method is annotated with this declaration annotation, then its signature is not written in a stub file and the method is not declared in source.
    If a method is annotated with this declaration annotation, then its signature was read from a stub file.
    This is a declaration annotation that applies to type declarations and packages.
    This annotation can be used two ways:
    A meta-annotation that specifies if a declaration annotation should be inherited.
    A meta-annotation indicating that an annotation is a type qualifier that should not be visible in output.
    An annotation to use on an element of a dependent type qualifier to specify which elements of the annotation should be interpreted as Java expressions.
    Specifies kinds of literal trees.
    A meta-annotation that indicates that a qualifier indicates that an expression goes monotonically from a type qualifier T to another qualifier S.
    Declaration annotation applied to type declarations to specify that the annotation on the type declaration should not be applied to unannotated uses of the type.
    This is a declaration annotation that applies to type declarations.
    A meta-annotation that indicates that an annotation can be used on a type variable use to explicitly indicate that the type variable is parametric in that type hierarchy.
    A meta-annotation that indicates that an annotation is a polymorphic type qualifier.
    A meta-annotation that indicates that an annotation E is a postcondition annotation, i.e., E is a type-specialized version of EnsuresQualifier or of EnsuresQualifier.List.
    A meta-annotation that indicates that an annotation R is a precondition annotation, i.e., R is a type-specialized version of RequiresQualifier.
    An annotation intended solely for representing an unqualified type in the qualifier hierarchy for the Purity Checker.
    An annotation to use on an element of a contract annotation to indicate that the element specifies the value of an argument of the qualifier.
    A meta-annotation that indicates what qualifier should be given to literals.
    An annotation on a SourceChecker subclass to specify which Java types are processed by the checker.
    A precondition annotation to indicate that a method requires certain expressions to have a certain qualifier at the time of the call to the method.
    A wrapper annotation that makes the RequiresQualifier annotation repeatable.
    An annotation on a SourceChecker subclass to provide additional stub files that should be used in addition to jdk.astub.
    A meta-annotation to specify all the qualifiers that the given qualifier is an immediate subtype of.
    A meta-annotation that restricts the type-use locations where a type qualifier may be applied.
    Specifies kinds of types.
    Specifies the locations to which a DefaultQualifier annotation applies.
    Declares that the field may not be accessed if the receiver is of the specified qualifier type (or any supertype).
    A meta-annotation applied to the declaration of a type qualifier.