Package org.checkerframework.checker.index.qual

Annotation Type IndexOrLow

@Documented
@Retention(RUNTIME)
@Target({TYPE_USE,TYPE_PARAMETER})
public @interface IndexOrLow

An integer that is either -1 or is a valid index for each of the given sequences.

The String.indexOf(String) method is declared as

   class String {
    @IndexOrLow("this") int indexOf(String str) { ... }
   }
 

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

See Also:

GTENegativeOne, 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 (or it's -1).

Element Detail

value

java.lang.String[] value

Sequences that the annotated expression is a valid index for (or it's -1).