@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 Integer.MAX_VALUE. However, this annotation is derived from an org.checkerframework.checker.index.qual.NonNegative annotation.

IntRangeFromNonNegative annotations derived from NonNegative annotations are used to create IntRange annotations, but IntRangeFromNonNegative annotations are not checked when they appear on the left-hand side of expressions. Therefore, the Index Checker MUST be run on any code with @NonNegative annotations on the left-hand side of expressions, since the Value Checker will derive information from them but not check them.

It is an error to write this annotation directly. @NonNegative or IntRange(from = 0, to = Integer.MAX_VALUE) 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

Annotation Interface IntRangeFromNonNegative