checker/tests/index/TransferMod.java

import org.checkerframework.checker.index.qual.GTENegativeOne;
import org.checkerframework.checker.index.qual.NonNegative;
import org.checkerframework.checker.index.qual.Positive;

public class TransferMod {

  void test() {
    int aa = -100;
    int a = -1;
    int b = 0;
    int c = 1;
    int d = 2;

    @Positive int e = 5 % 3;
    @NonNegative int f = -100 % 1;

    @NonNegative int g = aa % -1;
    @NonNegative int h = aa % 1;
    @NonNegative int i = d % -1;
    @NonNegative int j = d % 1;

    @NonNegative int k = d % c;
    @NonNegative int l = b % c;
    @NonNegative int m = c % d;

    @NonNegative int n = c % a;
    @NonNegative int o = b % a;

    @GTENegativeOne int p = a % a;
    @GTENegativeOne int q = a % d;
    @GTENegativeOne int r = a % c;
  }
}
// a comment