search

eisop / checker-framework

Pluggable type-checking for Java
https://eisop.github.io/
Other
17 stars 16 forks source link

Value Checker issue with boxed primitives and type refinements #687

Open wmdietl opened 6 months ago

wmdietl commented 6 months ago

When a boxed primitive is refined, that refinement is only stored with the un-boxed value, not with the original boxed primitive:

> cat Demo.java 
class Demo {
  void foo(Integer i) {
    int x = i > 5 ? i : 5;
  }
}

> ./checker/bin/javac -processor value Demo.java
Demo.java:3: error: [conditional.type.incompatible] incompatible types in conditional expression.
    int x = i > 5 ? i : 5;
                    ^
  found   : Integer
  required: @IntRange(from=5, to=2147483647) int
1 error
> cat Demo.java
import org.checkerframework.common.value.qual.IntVal;

class Demo {
  @IntVal(5) int foo(Integer i) {
    if (i == 5) {
       return i;
    } else {
      return 5;
    }
  }
}
wdietl@beryl ~/w/e/checker-framework-hacking (master)> ./checker/bin/javac -processor value Demo.java
Demo.java:6: error: [return.type.incompatible] incompatible types in return.
       return i;
              ^
  type of expression: Integer
  method return type: @IntVal(5L) int
1 error

Both examples pass if the parameter i is changed to int.

Thanks @thomaskirz for the report!