Value Checker Reports @UnknownVal for Compound Assignment on Some Variables

[zcai1]

Example:

import org.checkerframework.common.value.qual.*;
class A {
        @IntRange(from = 5, to = 10) int a;

        void foo1() {
            if (a == 5) {
                a += 5;
            }
        }

        void foo2(@IntRange(from = 5, to = 10) int b) {
            if (b == 5) {
                b += 5;
            }
        }
}

I expect the constant value checker to produce no errors, but it generates the following error messages:

error: [compound.assignment.type.incompatible] expression type incompatible with left-hand side in compound assignment.
                a += 5;
                  ^
  found   : @UnknownVal int
  required: @IntRange(from=5, to=10) int

error: [compound.assignment.type.incompatible] expression type incompatible with left-hand side in compound assignment.
                b += 5;
                  ^
  found   : @UnknownVal int
  required: @IntRange(from=5, to=10) int

As shown above, this issue happens to fields and method parameters. But if a was a local variable declared in the method body, then the checker will work as expected.

When a is a field, the corresponding CFG node is:

Before: CFStore#207(
 this.a > CFAV{@IntVal(5), int})
~~~~~~~~~
(this)   [ ImplicitThis ]
(this).a   [ FieldAccess ]    > CFAV{@IntVal(5), int}
5   [ IntegerLiteral ]    > CFAV{@IntVal(5), int}
((this).a + 5)   [ NumericalAddition ]    > CFAV{@IntVal(10), int}
(@org.checkerframework.common.value.qual.IntRange(from=5L, to=10L) int)((this).a + 5)   [ TypeCast ]    > CFAV{@UnknownVal, int}
(this).a = (@org.checkerframework.common.value.qual.IntRange(from=5L, to=10L) int)((this).a + 5)   [ Assignment ]    > CFAV{@UnknownVal, int}

When b is a method parameter, the corresponding CFG node is:

Before: CFStore#219(
 b > CFAV{@IntVal(5), int}
 this.a > CFAV{@IntRange(from=5, to=10), int})
~~~~~~~~~
b   [ LocalVariable ]    > CFAV{@IntVal(5), int}
5   [ IntegerLiteral ]    > CFAV{@IntVal(5), int}
(b + 5)   [ NumericalAddition ]    > CFAV{@IntVal(10), int}
(@org.checkerframework.common.value.qual.IntRange(from=5L, to=10L) int)(b + 5)   [ TypeCast ]    > CFAV{@UnknownVal, int}
b = (@org.checkerframework.common.value.qual.IntRange(from=5L, to=10L) int)(b + 5)   [ Assignment ]    > CFAV{@UnknownVal, int}

When a is a local variable declared in the method body, the corresponding CFG node is:

Before: CFStore#221(
 a > CFAV{@IntVal(5), int}
 c > CFAV{@IntRange(from=-2147483648, to=2147483647), int})
~~~~~~~~~
a   [ LocalVariable ]    > CFAV{@IntVal(5), int}
5   [ IntegerLiteral ]    > CFAV{@IntVal(5), int}
(a + 5)   [ NumericalAddition ]    > CFAV{@IntVal(10), int}
(int)(a + 5)   [ TypeCast ]    > CFAV{@IntVal(10), int}
a = (int)(a + 5)   [ Assignment ]    > CFAV{@IntVal(10), int}

Observe that the type changes after "TypeCast".