Annotation Interface IntRangeFromNonNegative
@Documented
@Retention(SOURCE)
@Target({})
@SubtypeOf(UnknownVal.class)
public @interface IntRangeFromNonNegative
An expression with this type is exactly the same as an
IntRange annotation whose
from field is 0 and whose to field is the maximum value for its type. However,
this annotation is derived from an org.checkerframework.checker.index.qual.NonNegative
annotation.
The Value Checker trusts this annotation. For soundness, the Index Checker must be run on any code with @NonNegative annotations on the left-hand side of assignments.
It is an error to write this annotation directly. @NonNegative, or an
@IntRange annotation whose from element is 0 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 @NonNegative annotation it replaced is retained in bytecode by the
Lower Bound Checker instead.
- See the Checker Framework Manual:
- Constant Value Checker