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 botha.length
andb.length
. The sequencesa
andb
might have different lengths.The
String.charAt(int)
method is declared asclass 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.
-