Description
Infer fails to report a DIVIDE_BY_ZERO error when an unrelated statement (such as System.out.println("")) is inserted before a division by zero, even though the divisor is explicitly initialized to 0 within the same local scope.
To Reproduce
public class test {
// Case 1
void bugDetected(int x) {
int i = 0;
int result = x / i; //<- reported (TP)
}
// Case 2
void bugMissed(int x) {
// Unrelated statements added
System.out.println("");
int i = 0;
int result = x / i; // <- should report (FN)
}
}
Expected behavior
Infer should report a DIVIDE_BY_ZERO error for the line int result = x / i; in both Case1 and Case2. The presence of a standard library call like System.out.println should not interfere with the symbolic execution or constant propagation of the local variable i.
Actual behavior
Only Case 1 is reported and Case 2 is ignored.