See: Description
| Enum | Description |
|---|---|
| LiteralKind |
Specifies kinds of literal trees.
|
| TypeKind |
Specifies kinds of types.
|
| TypeUseLocation |
Specifies the locations to which a
DefaultQualifier annotation applies. |
| 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 specifies that the given
annotation should be the default for.
|
| 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.
|
| IgnoreInWholeProgramInference |
This annotation can be used two ways:
|
| InheritedAnnotation |
A meta-annotation that specifies if an 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.
|
| 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. |
| 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 written.
|
| 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 specifies that the given
annotation should be upper bound for.
|
They may serve as documentation for the type qualifiers, and aid the Checker Framework to infer the relations between the type qualifiers.