checker/tests/index/LessThanLen.java

import org.checkerframework.checker.index.qual.*;
import org.checkerframework.common.value.qual.MinLen;

public class LessThanLen {

  public static void m1() {
    int[] shorter = new int[5];
    int[] longer = new int[shorter.length * 2];
    for (int i = 0; i < shorter.length; i++) {
      longer[i] = shorter[i];
    }
  }

  public static void m2(int @MinLen(1) [] shorter) {
    int[] longer = new int[shorter.length * 2];
    for (int i = 0; i < shorter.length; i++) {
      longer[i] = shorter[i];
    }
  }

  public static void m3(int[] shorter) {
    int[] longer = new int[shorter.length + 1];
    for (int i = 0; i < shorter.length; i++) {
      longer[i] = shorter[i];
    }
  }

  public static void m4(int @MinLen(1) [] shorter) {
    int[] longer = new int[shorter.length * 1];
    // :: error: (assignment)
    @LTLengthOf("longer") int x = shorter.length;
    @LTEqLengthOf("longer") int y = shorter.length;
  }

  public static void m5(int[] shorter) {
    // :: error: (array.length.negative)
    int[] longer = new int[shorter.length * -1];
    // :: error: (assignment)
    @LTLengthOf("longer") int x = shorter.length;
    // :: error: (assignment)
    @LTEqLengthOf("longer") int y = shorter.length;
  }

  public static void m6(int @MinLen(1) [] shorter) {
    int[] longer = new int[4 * shorter.length];
    // TODO: enable when https://github.com/kelloggm/checker-framework/issues/211 is fixed
    // // :: error: (assignment)
    // @LTLengthOf("longer") int x = shorter.length;
    @LTEqLengthOf("longer") int y = shorter.length;
  }

  public static void m7(int @MinLen(1) [] shorter) {
    int[] longer = new int[4 * shorter.length];
    @LTLengthOf("longer") int x = shorter.length;
    @LTEqLengthOf("longer") int y = shorter.length;
  }
}