Annotation Interface LTLengthOf
@
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

Optional Element Summary

Element Details

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



offset
This expression plus the annotated expression is less than the length of the sequence. Theoffset
element must ether be empty or the same length asvalue
.The expressions in
offset
may be addition/subtraction of any number of Java expressions. For example,@LessThanLengthOf(value = "a", offset = "x + y + 2"
}. Default:
 {}
