Annotation Type IndexFor


  • @Documented
    @Retention(RUNTIME)
    @Target({TYPE_USE,TYPE_PARAMETER})
    public @interface IndexFor
    An integer that can be used to index any of the given sequences.

    For example, an expression with type @IndexFor({"a", "b"}) is non-negative and is less than both a.length and b.length. The sequences a and b might have different lengths.

    The String.charAt(int) method is declared as

    
     class String {
       char charAt(@IndexFor("this") index) { ... }
     }
     

    Writing @IndexFor("arr") is equivalent to writing @NonNegative @LTLengthOf("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 @LTLengthOf.

    See Also:
    NonNegative, LTLengthOf
    See the Checker Framework Manual:
    Index Checker
    • Required Element Summary

      Required Elements 
      Modifier and Type Required Element Description
      java.lang.String[] value
      Sequences that the annotated expression is a valid index for.
    • Element Detail

      • value

        java.lang.String[] value
        Sequences that the annotated expression is a valid index for.