| Annotation Type | Description | 
|---|---|
| ArrayLen | An annotation indicating the length of an array. | 
| ArrayLenRange | An expression with this type evaluates to an array whose length is in the given range. | 
| BoolVal | An annotation indicating the possible values for a bool type. | 
| BottomVal | The bottom type in the Constant Value type system. | 
| DoubleVal | An annotation indicating the possible values for a double or float type. | 
| IntRange | An expression with this type evaluates to an integral value (byte, short, char, int, or long) in
 the given range. | 
| IntRangeFromPositive | An expression with this type is exactly the same as an  IntRangeannotation whosefromfield is1and whosetofield isInteger.MAX_VALUE. | 
| IntVal | An annotation indicating the possible values for a byte, short, char, int, or long type. | 
| MinLen | The value of the annotated expression is a sequence containing at least the given number of
 elements. | 
| MinLenFieldInvariant | A specialization of  FieldInvariantfor specifying the minimum length of an array. | 
| PolyValue | A polymorphic qualifier for the Constant Value Checker. | 
| StaticallyExecutable | StaticallyExecutable is a method annotation that indicates that the compiler is allowed to run
 the method at compile time, if all of the method's arguments are compile-time constants. | 
| StringVal | An annotation indicating the possible values for a String type. | 
| UnknownVal | UnknownVal is a type annotation indicating that the expression's value is not known at compile
 type. |