checker/tests/index/SubtractingNonNegatives.java

// Test case for issue 98: https://github.com/kelloggm/checker-framework/issues/98

import org.checkerframework.checker.index.qual.*;

public class SubtractingNonNegatives {
  public static void m4(int[] a, @IndexFor("#1") int i, @IndexFor("#1") int j) {
    int k = i;
    if (k >= j) {
      @IndexFor("a") int y = k;
    }
    for (k = i; k >= j; k -= j) {
      @IndexFor("a") int x = k;
    }
  }

  @SuppressWarnings("lowerbound")
  void test(int[] a, @Positive int y) {
    @LTLengthOf("a") int x = a.length - 1;
    @LTLengthOf(
        value = {"a", "a"},
        offset = {"0", "y"})
    int z = x - y;
    a[z + y] = 0;
  }

  @SuppressWarnings("lowerbound")
  void test2(int[] a, @Positive int y) {
    @LTLengthOf("a") int x = a.length - 1;
    int z = x - y;
    a[z + y] = 0;
  }
}