False Positive: INTEGER_OVERFLOW_L2 reported on safe loop with small compile-time upper bound

[mmnhgo]

Describe the bug
Infer incorrectly reports an INTEGER_OVERFLOW_L2 warning on a loop that is provably safe.

The loop counter counted is strictly bounded by expected=10, so counted += 1 can never reach Integer.MAX_VALUE. Nevertheless, Infer conservatively flags the call site because max = Integer.MAX_VALUE.

To Reproduce

public class a {

    public static void main(String[] args) {
        reproduceOverflowFP(10, Integer.MAX_VALUE);   // ← FP reported here
    }

    private static void reproduceOverflowFP(int expected, int max) {
        int counted;
        for (counted = 0; (counted <= max) && (counted < expected); counted += 1) {
            // loop body empty
        }
    }
}

Expected behavior
No INTEGER_OVERFLOW_L2 should be reported because:

expected is a small compile-time constant (10)
the loop condition (counted < expected) guarantees counted stays in range [0, 9]
counted += 1 can never cause integer overflow

Actual behavior
Infer reports:
Integer Overflow L2
([0, 2147483647] + 1):signed32 by call to void a.reproduceOverflowFP(int,int).
at line 5 (the call site in main)