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. This annotation is rarely used; it is more common to use @IndexFor.

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.

It is an error to write a LTLengthOf annotation with a different number of sequences and offsets, if an offset is included.

See Also:

IndexFor

See the Checker Framework Manual:

Index Checker

Required Element Summary

Required Elements

Modifier and Type	Required Element and Description
java.lang.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
java.lang.String[]	offset This expression plus the annotated expression is less than the length of the sequence.

Element Detail

value

public abstract java.lang.String[] value

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

offset

public abstract java.lang.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:

{}