Annotation Interface IntRangeFromPositive
@Documented
@Retention(SOURCE)
@Target({})
@SubtypeOf(UnknownVal.class)
public @interface IntRangeFromPositive
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.Positive
annotation.
The Value Checker trusts this annotation. For soundness, the Index Checker must be run on any code with @Positive annotations on the left-hand side of assignments.
It is an error to write this annotation directly. @Positive, 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 @Positive annotation it replaced is retained in bytecode by the Lower
Bound Checker instead.
- See the Checker Framework Manual:
- Constant Value Checker