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.
|
Bottom |
A special annotation intended solely for representing the bottom type in the qualifier hierarchy.
|
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 . |
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 |
Applied to the declaration of a type qualifier specifies that the given annotation should be the
default for a particular location.
|
DefaultInUncheckedCodeFor |
Applied to the declaration of a type qualifier, specifies that the given annotation should be the
default for unannotated type uses (in bytecode or source code) at the given location(s).
|
DefaultQualifier |
Applied to a declaration of a package, type, method, variable, etc., specifies that the given
annotation should be the default.
|
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.
|
DefaultQualifierInHierarchyInUncheckedCode |
Indicates that the annotated qualifier is the default qualifier on unannotated type uses (in
bytecode or source code that has not been type-checked).
|
DefaultQualifiers |
Specifies the annotations to be included in a type without having to provide them explicitly.
|
EnsuresQualifier |
A postcondition annotation to indicate that a method ensures certain expressions to have a
certain type qualifier once the method has successfully terminated.
|
EnsuresQualifierIf |
A conditional postcondition annotation to indicate that a method ensures that certain expressions
have a certain qualifier once the method has finished, and if the result is as indicated by
result . |
EnsuresQualifiers |
A meta-annotation to allow multiple postcondition annotations.
|
EnsuresQualifiersIf |
A meta-annotation to allow multiple conditional postcondition annotations.
|
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:
|
ImplicitFor |
A meta-annotation that specifies the trees and types for which the framework should automatically
add that qualifier.
|
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 . |
PolyAll |
A polymorphic type qualifier that varies over all type hierarchies.
|
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 . |
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.
|
RelevantJavaTypes |
An annotation on a SourceChecker subclass to specify which 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.
|
RequiresQualifiers |
A meta-annotation to allow multiple precondition annotations.
|
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.
|
Unqualified |
A special annotation intended solely for representing an unqualified type in the qualifier
hierarchy, as an argument to
SubtypeOf.value() , in the type qualifiers declarations. |
Unused |
Declares that the field may not be accessed if the receiver is of the specified qualifier type
(or any supertype).
|
They may serve as documentation for the type qualifiers, and aid the Checker Framework to infer the relations between the type qualifiers.