Yes, you can't prove important properties of the class of all programs, but you can prove properties of smaller, limited classes of programs that you are interested in.

So the Java IDE had been able to recognize an infinite loop of the kind you wrote by an algorithm, that can be proven to be correct for a limited class.

On the other hand, you can loop infinitely deciding to exit on the return value of opaque calls to some entity external to your analyzer, and your IDE shouldn't be able to catch that.