checker/tests/value-index-interaction/MinLenFromPositive.java

import org.checkerframework.checker.index.qual.Positive;
import org.checkerframework.common.value.qual.ArrayLen;
import org.checkerframework.common.value.qual.IntRange;
import org.checkerframework.common.value.qual.MinLen;

public class MinLenFromPositive {

  public @Positive int x = 0;

  void testField() {
    this.x = -1;
    @IntRange(from = 1) int f = this.x;
    int @MinLen(1) [] y = new int[x];
  }

  void testArray(@Positive int @ArrayLen(1) [] x) {
    int @MinLen(1) [] array = new int[x[0]];
  }

  void useTestArray(int @ArrayLen(1) [] x, int[] y) {
    testArray(x);
    // :: error: (argument)
    testArray(y);
  }

  void test(@Positive int x) {
    @IntRange(from = 1) int z = x;
    @Positive int q = x;
    @Positive int a = -1;
    int @MinLen(1) [] array = new int[a];
  }

  // Ensure that just running the value checker doesn't result in an LHS warning.
  void foo2(int x) {
    test(x);
  }

  @Positive int id(@Positive int x) {
    return -1;
  }

  @Positive int plus(@Positive int x, @Positive int y) {
    // :: error: (assignment)
    @IntRange(from = 0) int z = x + y;
    // :: error: (assignment)
    @IntRange(from = 1) int q = x + y;

    return x + y;
  }

  // Ensure that LHS warnings aren't issued even for arrays of Positives
  @Positive int[] array_test() {
    int[] a = {-1, 2, 3};
    return a;
  }
}