Coverity can't report infinite loop defect

I have following Java code with potential infinite loop if I pass in divisor with 0 value. But Coverity can't report this bug for me.

class InfinityLoopExample {
  public int div(final int dividend, final int divisor)  {
    int ret = 0;
    int x = dividend;
    while (x > divisor) {
      x = x - divisor;
      ret++;
    }
    return ret;
  }
}

//And following code to actually call that method i.e. in main.
//This will make sure infinite loop real happens
final InfinityLoopExample infinityLoopExample = new InfinityLoopExample();
final int ret1 = infinityLoopExample.div(3,0);
System.out.println("infinityLoopExample.div:" + ret1);

From following coverity link it is clear say that coverity can report this kind of bugs during its static code analysis: https://cwe.mitre.org/data/definitions/835.html

I ran coverity code scan against above Java code, it can't report infinity loop problem. Has anyone ran coverity code scan against Java project can give some light?

P.S I have coverity build log file with size 151K. I can post it if needed.

Solution

As one of the two people who originally designed the INFINITE_LOOP checker back in 2010 or so when I worked for Coverity (I do not anymore), I can say a bit about why this might not be reported, although I can't go into great detail because this pertains to Coverity (now Synopsys) proprietary intellectual property.

First, one must recognize that Coverity does not report all instances of any given defect type. That's related to the undecidability of the halting problem; it is mathematically impossible for a fully automatic static analysis to be perfectly accurate. Furthermore, most Coverity checkers are designed to report no more than about 20% false positives, and in order to do that, it requires that the code contain fairly strong evidence of a problem before it is willing to report.

The function div does not contain sufficiently strong evidence of a problem because it is plausible that divisor is never supposed to be passed in as zero. If instead it contained something like if (divisor==0) {...}, that would be strong evidence that a zero argument is supposed to be tolerated. That's not the only sort of evidence the tool recognizes, of course. If you added code like that, containing clear evidence of an internal contradiction in the logic, and the checker still did not report, then I would suggest reporting the example to the Coverity support team.

Now, in addition to div, your example includes a call site:

final int ret1 = infinityLoopExample.div(3,0);

Based on this, divisor can obviously be zero, right? Yes--but now you've likely run into a limitation of this particular checker.

Let's divert for a moment to compare to another checker, FORWARD_NULL, which is the main checker responsible for reporting null dereference issues. FORWARD_NULL will not report this:

int deref(MyClass c) { return c.someField; }

The method deref will throw NullPointerException if c is null, but we have no evidence that c ever is null. However, FORWARD_NULL recognizes the potential, so it remembers that deref unconditionally dereferences its argument. Later if it sees a call site like:

deref(null);

then it will report that call site.

However, INFINITE_LOOP does not, or at least did not when originally designed, have a comparable mechanism. If it cannot find sufficient justification to report a loop within the containing function, then it does not report, regardless of what might happen at call sites.

It would not be unreasonable to make an enhancement request to the Coverity team to expand the detection capabilities of INFINITE_LOOP in this way. However, if you do that, I would strongly encourage submitting code where the calling code is more realistic. Did Coverity miss a real defect in your actual, production code? Submit that. Another element of the Coverity design philosophy is to emphasize accuracy on real code rather than contrived examples, since the two have many important differences that the analysis is quite sensitive to.