framework/tests/value-ignore-range-overflow/TransferDivide.java

import org.checkerframework.common.value.qual.*;

public class TransferDivide {

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

    /** literals */
    @IntRange(from = 1) int e = -1 / -1;

    /** 0 / * -> NN */
    @IntRange(from = 0) int f = 0 / a;
    @IntRange(from = 0) int g = 0 / d;

    /** * / 1 -> * */
    @IntRange(from = -1) int h = a / 1;
    @IntRange(from = 0) int i = b / 1;
    @IntRange(from = 1) int j = c / 1;
    @IntRange(from = 1) int k = d / 1;

    /** pos / pos -> nn */
    @IntRange(from = 0) int l = d / c;
    @IntRange(from = 0) int m = c / d;
    // :: error: (assignment)
    @IntRange(from = 1) int n = c / d;

    /** nn / pos -> nn */
    @IntRange(from = 0) int o = b / c;
    // :: error: (assignment)
    @IntRange(from = 1) int p = b / d;

    /** pos / nn -> nn */
    @IntRange(from = 0) int q = d / l;
    // :: error: (assignment)
    @IntRange(from = 1) int r = c / l;

    /** nn / nn -> nn */
    @IntRange(from = 0) int s = b / q;
    // :: error: (assignment)
    @IntRange(from = 1) int t = b / q;

    /** n1p / pos -> n1p */
    @IntRange(from = -1) int u = a / d;
    @IntRange(from = -1) int v = a / c;
    // :: error: (assignment)
    @IntRange(from = 0) int w = a / c;

    /** n1p / nn -> n1p */
    @IntRange(from = -1) int x = a / l;
  }

  void testDivideByTwo(@IntRange(from = 0) int x) {
    @IntRange(from = 0) int y = x / 2;
  }
}