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.
Best Answer