BugFinder unable to find any NTL?

I know that BugFinder analysis is not supposed to be as exhaustive as CodeProver, but somehow even the most simplistic form of non terminating loops are not marked in the results. Is this expected behavior?

In a file I analyzed using a few tools,

while(g_tj.rounds);

can be not terminating because g_tj is not marked volatile, so the compiler would be allowed to cache the access. This is of course marked as a red check in CodeProver, but even free ccpcheck marks it as suspicious.

As you can see in the image from the BugFinder result, the tooltip seems to be speculating about non termination, but the line is not marked (for that) in the result output, even though all BugFinder checks are enabled.

What am I missing?

Answer 1

[Anirban]

Hi Oliver,

Code Prover can find this and other much more sophisticated cases of non-terminating loops. Bug Finder uses the same engine underneath (with different underlying assumptions for faster analysis) and as you have noticed in the tooltip, Bug Finder can also detect this simple infinite loop. However, this capability is not available as a checker in Bug Finder.

In practice, infinite loops such as the ones you point will also manifest as an issue in the loop body (for instance, an Out of Bounds Array Index on some array access or an Overflow on some math operation), and Bug Finder will be able to detect those issues. Therefore, a checker on the loop statement itself is not always necessary.

In most cases, it is safe to assume that Bug Finder will find simpler cases while Code Prover, because of its exhaustive analysis, will find more sophisticated examples of an issue. For instance, both products have an Out of Bounds Array Index checker. The case of non-terminating loops seems to be an exception currently where Bug Finder does not have an explicit checker at all. This situation might change in future releases.