checker/tests/index/IndexOrLowTests.java

import org.checkerframework.checker.index.qual.GTENegativeOne;
import org.checkerframework.checker.index.qual.IndexOrHigh;
import org.checkerframework.checker.index.qual.IndexOrLow;
import org.checkerframework.checker.index.qual.LTLengthOf;

public class IndexOrLowTests {
  int[] array = {1, 2};

  @IndexOrLow("array") int index = -1;

  void test() {

    if (index != -1) {
      array[index] = 1;
    }

    @IndexOrHigh("array") int y = index + 1;
    // :: error: (array.access.unsafe.high)
    array[y] = 1;
    if (y < array.length) {
      array[y] = 1;
    }
    // :: error: (assignment)
    index = array.length;
  }

  void test2(@LTLengthOf("array") @GTENegativeOne int param) {
    index = array.length - 1;
    @LTLengthOf("array") @GTENegativeOne int x = index;
    index = param;
  }
}