checker/tests/index/Issue2452.java

// Test case for https://github.com/typetools/checker-framework/issues/2452

import java.lang.reflect.Array;
import org.checkerframework.checker.index.qual.IndexFor;
import org.checkerframework.checker.index.qual.IndexOrHigh;
import org.checkerframework.checker.index.qual.LTEqLengthOf;
import org.checkerframework.checker.index.qual.NonNegative;
import org.checkerframework.checker.index.qual.Positive;
import org.checkerframework.common.value.qual.MinLen;

class Issue2452 {
  Object m1(Object[] a1) {
    if (Array.getLength(a1) > 0) {
      return Array.get(a1, 0);
    } else {
      return null;
    }
  }

  void m2() {
    int[] arr = {1, 2, 3};
    @LTEqLengthOf({"arr"}) int a = Array.getLength(arr);
  }

  void testMinLenSubtractPositive(String @MinLen(10) [] s) {
    @Positive int i1 = s.length - 9;
    @NonNegative int i0 = Array.getLength(s) - 10;
    // ::  error: (assignment)
    @NonNegative int im1 = Array.getLength(s) - 11;
  }

  void testLessThanLength(String[] s, @IndexOrHigh("#1") int i, @IndexOrHigh("#1") int j) {
    if (i < Array.getLength(s)) {
      @IndexFor("s") int in = i;
      // ::  error: (assignment)
      @IndexFor("s") int jn = j;
    }
  }
}