Indicates that the given expressions evaluate to an integer whose value is less than the lengths of all the given sequences, if the method returns the given result (either true or false).

As an example, consider the following method:

     @EnsuresLTLengthOfIf(
         expression = "end",
         result = true,
         targetValue = "array",
         offset = "#1 - 1"
     )
     public boolean tryShiftIndex(@NonNegative int x) {
         int newEnd = end - x;
         if (newEnd < 0) {
            return false;
         }
         end = newEnd;
         return true;
     }

Calling this function ensures that the field end of the this object is of type @LTLengthOf(value = "array", offset = "x - 1"), for the value x that is passed as the argument. This allows the Index Checker to verify that end + x is an index into array in the following code:

     public void useTryShiftIndex(@NonNegative int x) {
         if (tryShiftIndex(x)) {
             Arrays.fill(array, end, end + x, null);
         }
     }

Nested and Inner Type Summary

Modifier and Type	Class and Description
public static @interface	EnsuresLTLengthOfIf.List A wrapper annotation that makes the `EnsuresLTLengthOfIf` annotation repeatable.

Method Summary

Modifier and Type	Method and Description
public String[]	expression() Java expression(s) that are less than the length of the given sequences after the method returns the given result.
public String[]	Returns: the offset expressions offset() This expression plus each of the expressions is less than the length of the sequence after the method returns the given result.
public boolean	result() The return value of the method that needs to hold for the postcondition to hold.
public String[]	targetValue() Sequences, each of which is longer than each of the expressions' value after the method returns the given result.

Inherited from java.lang.annotation.Annotation:: annotationType equals hashCode toString

Method Detail

expression	back to summary
public String[] expression() Java expression(s) that are less than the length of the given sequences after the method returns the given result.

offset back to summary

offset	back to summary
public String[] offset() This expression plus each of the expressions is less than the length of the sequence after the method returns the given result. The `offset` element must ether be empty or the same length as `targetValue`. Returns:String[] the offset expressions Annotations @JavaExpression @QualifierArgument:offset

public String[] offset()

This expression plus each of the expressions is less than the length of the sequence after the method returns the given result. The offset element must ether be empty or the same length as targetValue.

Returns:String[]

the offset expressions

Annotations

@JavaExpression
@QualifierArgument:offset

result	back to summary
public boolean result() The return value of the method that needs to hold for the postcondition to hold.

targetValue	back to summary
public String[] targetValue() Sequences, each of which is longer than each of the expressions' value after the method returns the given result. Annotations @JavaExpression @QualifierArgument:value

targetValue

back to summary

public String[] targetValue()

Sequences, each of which is longer than each of the expressions' value after the method returns the given result.

Annotations

@JavaExpression
@QualifierArgument:value

org.checkerframework.checker.index.qual back to summary

public @Interface EnsuresLTLengthOfIf.List

Annotations

extends Annotation

@Documented
@Retention:RUNTIME
@Target:METHOD, CONSTRUCTOR
@ConditionalPostconditionAnnotation
qualifier:LTLengthOf
@InheritedAnnotation

A wrapper annotation that makes the EnsuresLTLengthOfIf annotation repeatable.

Programmers generally do not need to write this. It is created by Java when a programmer writes more than one EnsuresLTLengthOfIf annotation at the same location.

Method Summary

Modifier and Type	Method and Description
public EnsuresLTLengthOfIf[]	Returns: the repeatable annotations value() Return the repeatable annotations.

Inherited from java.lang.annotation.Annotation:: annotationType equals hashCode toString

Method Detail

value	back to summary
public EnsuresLTLengthOfIf[] value() Return the repeatable annotations. Returns:EnsuresLTLengthOfIf[] the repeatable annotations

value

back to summary

public EnsuresLTLengthOfIf[] value()

Return the repeatable annotations.

Returns:EnsuresLTLengthOfIf[]: the repeatable annotations