Package org.checkerframework.checker.index.qual

Annotation Interface IndexOrHigh

@Documented @Retention(RUNTIME) @Target({TYPE_USE,TYPE_PARAMETER}) public @interface IndexOrHigh
An integer that, for each of the given sequences, is either a valid index or is equal to the sequence's length.

The Arrays.binarySearch method is declared as 


 class Arrays {
   int binarySearch(Object[] a, @IndexFor("#1") int fromIndex, @IndexOrHigh("#1") int toIndex, Object key)
 }

Writing @IndexOrHigh("arr") is equivalent to writing @NonNegative @LTEqLengthOf("arr"), and that is how it is treated internally by the checker. Thus, if you write an @IndexFor("arr") annotation, you might see warnings about @NonNegative or @LTEqLengthOf.

See Also:
See the Checker Framework Manual:
Index Checker

  • Required Element Summary

    Required Elements
    Modifier and Type
    Required Element
    Description
    String[]
    value
    Sequences that the annotated expression is a valid index for or is equal to the lengeth of.

  • Element Details

    • value

      String[] value
      Sequences that the annotated expression is a valid index for or is equal to the lengeth of.