Package org.checkerframework.checker.index.qual

Annotation Interface LTLengthOf

@Documented @Retention(RUNTIME) @Target({TYPE_USE,TYPE_PARAMETER}) @SubtypeOf(LTEqLengthOf.class) 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:
See the Checker Framework Manual:
Index Checker

  • Required Element Summary

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

  • Element Details

    • value

      @JavaExpression String[] value
      Sequences, each of which is longer than the annotated expression's value.

    • offset

      @JavaExpression 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:
      {}