checker/tests/index/Modulo.java

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

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;

public class Modulo {
  void m1(Object[] a, @IndexOrHigh("#1") int i, @NonNegative int j) {
    @IndexFor("a") int k = j % i;
  }

  void m1p(Object[] a, @Positive @LTEqLengthOf("#1") int i, @Positive int j) {
    @IndexFor("a") int k = j % i;
  }

  void m2(Object[] a, int i, @IndexFor("#1") int j) {
    @IndexFor("a") int k = j % i;
  }

  void m2(Object[] a, Object[] b, @IndexFor("#1") int i, @IndexFor("#2") int j) {
    @IndexFor({"a", "b"}) int k = j % i;
  }
}