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

IntRangeFromGTENegativeOne annotations derived from GTENegativeOne annotations are used to create IntRange annotations, but IntRangeFromGTENegativeOne 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 @GTENegativeOne 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. @GTENegativeOne or IntRange(from = -1, 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 @GTENegativeOne annotation it replaced is retained in bytecode by the Lower Bound Checker instead.

See the Checker Framework Manual:: Constant Value Checker

Annotation Interface IntRangeFromGTENegativeOne