They may serve as documentation for the type qualifiers, and aid the Checker Framework to infer the relations between the type qualifiers.
| Modifier and Type | Annotation and Description |
|---|---|
| public @interface | AnnotatedFor
Indicates that this class has been annotated for the given type system. |
| public @interface | CFComment
This annotation is for comments related to the Checker Framework. |
| public @interface | ConditionalPostconditionAnnotation
A meta-annotation that indicates that an annotation E is a conditional postcondition annotation,
i.e., E is a type-specialized version of |
| public @interface | 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. |
| public @interface | DefaultFor
A meta-annotation applied to the declaration of a type qualifier. |
| public @interface | DefaultQualifier
Applied to a declaration of a package, type, method, variable, etc., specifies that the given annotation should be the default. |
| public @interface | DefaultQualifierForUse
Declaration annotation applied to type declarations to specify the qualifier to be added to unannotated uses of the type. |
| public @interface | 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. |
| public @interface | EnsuresQualifier
A postcondition annotation to indicate that a method ensures that certain expressions have a certain type qualifier once the method has successfully terminated. |
| public @interface | 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
|
| public @interface | FieldInvariant
Specifies that a field's type, in the class on which this annotation is written, is a subtype of its declared type. |
| public @interface | 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. |
| public @interface | FromStubFile
If a method is annotated with this declaration annotation, then its signature was read from a stub file. |
| public @interface | HasQualifierParameter
This is a declaration annotation that applies to type declarations and packages. |
| public @interface | |
| public @interface | InheritedAnnotation
A meta-annotation that specifies if a declaration annotation should be inherited. |
| public @interface | InvisibleQualifier
A meta-annotation indicating that an annotation is a type qualifier that should not be visible in output. |
| public @interface | 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. |
| public @interface | MonotonicQualifier
A meta-annotation that indicates that a qualifier indicates that an expression goes monotonically
from a type qualifier |
| public @interface | 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. |
| public @interface | NoQualifierParameter
This is a declaration annotation that applies to type declarations. |
| public @interface | PolymorphicQualifier
A meta-annotation that indicates that an annotation is a polymorphic type qualifier. |
| public @interface | PostconditionAnnotation
A meta-annotation that indicates that an annotation E is a postcondition annotation, i.e., E is a
type-specialized version of |
| public @interface | PreconditionAnnotation
A meta-annotation that indicates that an annotation R is a precondition annotation, i.e., R is a
type-specialized version of |
| public @interface | PurityUnqualified
An annotation intended solely for representing an unqualified type in the qualifier hierarchy for the Purity Checker. |
| public @interface | 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. |
| public @interface | QualifierForLiterals
A meta-annotation that indicates what qualifier should be given to literals. |
| public @interface | RelevantJavaTypes
An annotation on a SourceChecker subclass to specify which Java types are processed by the checker. |
| public @interface | 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. |
| public @interface | StubFiles
An annotation on a SourceChecker subclass to provide additional stub files that should be used in
addition to |
| public @interface | SubtypeOf
A meta-annotation to specify all the qualifiers that the given qualifier is an immediate subtype of. |
| public @interface | TargetLocations
Note This meta-annotation is not currently enforced. |
| public @interface | Unused
Declares that the field may not be accessed if the receiver is of the specified qualifier type (or any supertype). |
| public @interface | UpperBoundFor
A meta-annotation applied to the declaration of a type qualifier. |
| Modifier and Type | Enum and Description |
|---|---|
| public enum | LiteralKind
Specifies kinds of literal trees. |
| public enum | TypeKind
Specifies kinds of types. |
| public enum | TypeUseLocation
Specifies the locations to which a |