Annotation Interface IntRangeFromGTENegativeOne
@Documented
@Retention(SOURCE)
@Target({})
@SubtypeOf(UnknownVal.class)
public @interface IntRangeFromGTENegativeOne
An expression with this type is exactly the same as an
IntRange annotation whose
from field is -1 and whose to field is the maximum value for its type. However,
this annotation is derived from an org.checkerframework.checker.index.qual.GTENegativeOne
annotation.
The Value Checker trusts this annotation. For soundness, the Index Checker must be run on any code with @GTENegativeOne annotations on the left-hand side of assignments.
It is an error to write this annotation directly. @GTENegativeOne, or an
@IntRange annotation whose from element is -1 and whose to
element is the maximum value of the annotated type, should always be written instead. This
annotation is not retained in bytecode, but is replaced with @UnknownVal, so that it is
not enforced on method boundaries. The @GTENegativeOne annotation it replaced is retained
in bytecode by the Lower Bound Checker instead.
- See the Checker Framework Manual:
- Constant Value Checker