// Test case for Issue 867:
// https://github.com/typetools/checker-framework/issues/867

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

public class Issue867 {
  void test1() {
    @IntVal({0, 1}) int x = 0;
    @IntVal(0) int zero = x++;
    @IntVal(1) int one = x;
    // :: error: (unary.increment)
    x++;

    x = 1;
    one = x--;
    zero = x;
    // :: error: (unary.decrement)
    x--;
  }

  void test2() {
    @IntVal({0, 1, 2}) int x = 0;
    @IntVal(1) int one = x++ + x++;
    @IntVal(2) int two = x;
    // :: error: (unary.increment)
    x++;

    x = 2;
    @IntVal(3) int three = x-- + x--;
    @IntVal(0) int zero = x;
    // :: error: (unary.decrement)
    x--;
  }

  void test3() {
    @IntVal({0, 1, 2}) int x = 0;
    @IntVal(2) int two = x++ + ++x;
    two = x;
    // :: error: (unary.increment)
    x++;

    x = 2;
    two = x-- + --x;
    @IntVal(0) int zero = x;
    // :: error: (unary.decrement)
    x--;
  }

  void test4() {
    @IntVal({0, 1}) int x = 0;
    m0(x++);
    // :: error: (argument)
    m0(x);
    // :: error: (unary.increment)
    m1(x++);

    x = 1;
    m1(x--);
    // :: error: (argument)
    m1(x);
    // :: error: (unary.decrement)
    m0(x--);
  }

  void m0(@IntVal(0) int x) {}

  void m1(@IntVal(1) int x) {}
}