Repository navigation
False Positive With Early Return #68
Description
The type checker fails to recognize that an early return can satisfy a refinement condition.
public class Example {
public static int divide(int a, @Refinement("b != 0") int b) {
return a / b;
}
public static void example1(int x, int y) {
if (y == 0) {
System.out.println("division by zero");
} else {
divide(x, y); // correct (no error)
}
}
public static void example2(int x, int y) {
if (y == 0) {
System.out.println("division by zero");
return; // early return
}
divide(x, y); // should also be correct but isnt
}
}In this example, the refinement b != 0 should be considered satisfied in both cases, since after the if (y == 0) branch returns, the only reachable path ensures y != 0.
Possible Fix
Convert early-exit branches into ternary (explicit if-else).
Activity