org.checkerframework.checker.index.qual

Annotation Type IndexFor

@Documented
 @Retention(value=RUNTIME)
 @Target(value={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 and Description
String[]	value Sequences that the annotated expression is a valid index for.

Element Detail

value

public abstract String[] value

Sequences that the annotated expression is a valid index for.