framework/tests/value/NegativeArrayLen.java

import org.checkerframework.common.value.qual.ArrayLen;
import org.checkerframework.common.value.qual.BottomVal;

public class NegativeArrayLen {
  void test1() {
    int @BottomVal [] a = new int[-1];
    int @BottomVal [] b = new int[Integer.MAX_VALUE + 1];
    // :: warning: (negative.arraylen)
    int @ArrayLen(-1) [] c = new int[-1];
  }

  void test2(
      // :: warning: (negative.arraylen)
      int @ArrayLen(Integer.MIN_VALUE) [] a,
      // :: warning: (negative.arraylen)
      int @ArrayLen({-1, 2, 0}) [] b) {
    int @BottomVal [] y = a;
    int @BottomVal [] x = b;
  }
}