Package org.checkerframework.checker.index.qual

Annotation Interface EnsuresLTLengthOfIf

@Documented @Retention(RUNTIME) @Target({METHOD,CONSTRUCTOR}) @ConditionalPostconditionAnnotation(qualifier=LTLengthOf.class) @InheritedAnnotation @Repeatable(List.class) public @interface EnsuresLTLengthOfIf
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);
          }
      }
See Also:
See the Checker Framework Manual:
Index Checker

  • Nested Class Summary

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

  • Required Element Summary

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

  • Optional Element Summary

    Optional Elements
    Modifier and Type
    Optional Element
    Description
    String[]
    offset
    This expression plus each of the expressions is less than the length of the sequence after the method returns the given result.

  • Element Details

    • expression

      String[] expression
      Java expression(s) that are less than the length of the given sequences after the method returns the given result.
      See the Checker Framework Manual:
      Syntax of Java expressions

    • result

      boolean result
      The return value of the method that needs to hold for the postcondition to hold.

    • targetValue

      @JavaExpression @QualifierArgument("value") String[] targetValue
      Sequences, each of which is longer than each of the expressions' value after the method returns the given result.

    • offset

      @JavaExpression @QualifierArgument("offset") 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:
      the offset expressions
      Default:
      {}