checker/tests/index/TransferAdd.java

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

public class TransferAdd {

  void test() {

    // adding zero and one and two

    int a = -1;

    @Positive int a1 = a + 2;

    @NonNegative int b = a + 1;
    @NonNegative int c = 1 + a;

    @GTENegativeOne int d = a + 0;
    @GTENegativeOne int e = 0 + a;

    // :: error: (assignment)
    @Positive int f = a + 1;

    @NonNegative int g = b + 0;

    @Positive int h = b + 1;

    @Positive int i = h + 1;
    @Positive int j = h + 0;

    // adding values

    @Positive int k = i + j;
    // :: error: (assignment)
    @Positive int l = b + c;
    // :: error: (assignment)
    @Positive int m = d + c;
    // :: error: (assignment)
    @Positive int n = d + e;

    @Positive int o = h + g;
    // :: error: (assignment)
    @Positive int p = h + d;

    @NonNegative int q = b + c;
    // :: error: (assignment)
    @NonNegative int r = q + d;

    @NonNegative int s = k + d;
    @GTENegativeOne int t = s + d;

    // increments

    // :: error: (assignment)
    @Positive int u = b++;

    @Positive int u1 = b;

    @Positive int v = ++c;

    @Positive int v1 = c;

    int n1p1 = -1, n1p2 = -1;

    @NonNegative int w = ++n1p1;

    @NonNegative int w1 = n1p1;

    // :: error: (assignment)
    @Positive int w2 = n1p1;
    // :: error: (assignment)
    @Positive int w3 = n1p1++;

    // :: error: (assignment)
    @NonNegative int x = n1p2++;

    @NonNegative int x1 = n1p2;

    // :: error: (assignment)
    @Positive int y = ++d;
    // :: error: (assignment)
    @Positive int z = e++;
  }
}
// a comment