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

Enum Summary

Enum	Description
LiteralKind	Specifies kinds of literal trees.
TypeKind	Specifies kinds of types.
TypeUseLocation	Specifies the locations to which a DefaultQualifier annotation applies.

Annotation Types Summary

Annotation Type	Description
AnnotatedFor	Indicates that this class has been annotated for the given type system.
CFComment	This annotation is for comments related to the Checker Framework.
ConditionalPostconditionAnnotation	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.
Covariant	A marker annotation, written on a class declaration, that signifies that one or more of the class's type parameters can be treated covariantly.
DefaultFor	A meta-annotation applied to the declaration of a type qualifier.
DefaultQualifier	Applied to a declaration of a package, type, method, variable, etc., specifies that the given annotation should be the default.
DefaultQualifier.List	A wrapper annotation that makes the DefaultQualifier annotation repeatable.
DefaultQualifierForUse	Declaration annotation applied to type declarations to specify the qualifier to be added to unannotated uses of the type.
DefaultQualifierInHierarchy	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.
EnsuresQualifier	A postcondition annotation to indicate that a method ensures that certain expressions have a certain type qualifier once the method has successfully terminated.
EnsuresQualifier.List	A wrapper annotation that makes the EnsuresQualifier annotation repeatable.
EnsuresQualifierIf	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.
EnsuresQualifierIf.List	A wrapper annotation that makes the EnsuresQualifierIf annotation repeatable.
FieldInvariant	Specifies that a field's type, in the class on which this annotation is written, is a subtype of its declared type.
FromByteCode	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.
FromStubFile	If a method is annotated with this declaration annotation, then its signature was read from a stub file.
HasQualifierParameter	This is a declaration annotation that applies to type declarations and packages.
IgnoreInWholeProgramInference	This annotation can be used two ways:
InheritedAnnotation	A meta-annotation that specifies if a declaration annotation should be inherited.
InvisibleQualifier	A meta-annotation indicating that an annotation is a type qualifier that should not be visible in output.
JavaExpression	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.
MonotonicQualifier	A meta-annotation that indicates that a qualifier indicates that an expression goes monotonically from a type qualifier T to another qualifier S.
NoDefaultQualifierForUse	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.
NoQualifierParameter	This is a declaration annotation that applies to type declarations.
PolymorphicQualifier	A meta-annotation that indicates that an annotation is a polymorphic type qualifier.
PostconditionAnnotation	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.
PreconditionAnnotation	A meta-annotation that indicates that an annotation R is a precondition annotation, i.e., R is a type-specialized version of RequiresQualifier.
PurityUnqualified	An annotation intended solely for representing an unqualified type in the qualifier hierarchy for the Purity Checker.
QualifierArgument	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.
QualifierForLiterals	A meta-annotation that indicates what qualifier should be given to literals.
RelevantJavaTypes	An annotation on a SourceChecker subclass to specify which Java types are processed by the checker.
RequiresQualifier	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.
RequiresQualifier.List	A wrapper annotation that makes the RequiresQualifier annotation repeatable.
StubFiles	An annotation on a SourceChecker subclass to provide additional stub files that should be used in addition to jdk.astub.
SubtypeOf	A meta-annotation to specify all the qualifiers that the given qualifier is an immediate subtype of.
TargetLocations	A meta-annotation that restricts the type-use locations where a type qualifier may be applied.
Unused	Declares that the field may not be accessed if the receiver is of the specified qualifier type (or any supertype).
UpperBoundFor	A meta-annotation applied to the declaration of a type qualifier.