checker/tests/index/LTLDivide.java

import org.checkerframework.checker.index.qual.LTEqLengthOf;
import org.checkerframework.checker.index.qual.LTLengthOf;

public class LTLDivide {
  int[] test(int[] array) {
    //        @LTLengthOf("array") int len = array.length / 2;
    int len = array.length / 2;
    int[] arr = new int[len];
    for (int a = 0; a < len; a++) {
      arr[a] = array[a];
    }
    return arr;
  }

  void test2(int[] array) {
    int len = array.length;
    int lenM1 = array.length - 1;
    int lenP1 = array.length + 1;
    // :: error: (assignment)
    @LTLengthOf("array") int x = len / 2;
    @LTLengthOf("array") int y = lenM1 / 3;
    @LTEqLengthOf("array") int z = len / 1;
    // :: error: (assignment)
    @LTLengthOf("array") int w = lenP1 / 2;
  }
}