org.checkerframework.checker.index.qual

Annotation Type LTLengthOf

@SubtypeOf(value=LTEqLengthOf.class)
 @Retention(value=RUNTIME)
 @Target(value={TYPE_USE,TYPE_PARAMETER})
public @interface LTLengthOf

The annotated expression evaluates to an integer whose value is less than the lengths of all the given sequences.

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

The @LTLengthOf annotation takes an optional offset element. If it is nonempty, then the annotated expression plus the expression in offset[i] is less than the length of the sequence specified by value[i].

For example, suppose expression e has type @LTLengthOf(value = {"a", "b"}, offset = {"-1", "x"}). Then e - 1 is less than a.length, and e + x is less than b.length.

See the Checker Framework Manual:

Index Checker

Required Element Summary

Required Elements

Modifier and Type	Required Element and Description
String[]	value Sequences, each of which is longer than the annotated expression's value.

Optional Element Summary

Optional Elements

Modifier and Type	Optional Element and Description
String[]	offset This expression plus the annotated expression is less than the length of the sequence.

Element Detail

value

public abstract String[] value

Sequences, each of which is longer than the annotated expression's value.

offset

public abstract String[] offset

This expression plus the annotated expression is less than the length of the sequence. The offset element must ether be empty or the same length as value.

The expressions in offset may be addition/subtraction of any number of Java expressions. For example, @LessThanLengthOf(value = "a", offset = "x + y + 2"}.

Default:

{}