I disagree. Think of a loop where a break condition depends on the validity of, say, Goldbach's conjecture. No static analyzer can tell when (or if) such a program will halt. This is an extreme example, of course, but any sufficiently complicated expression that affects what code path is taken and/or termination of the program will pretty much have the same problem when it comes to static analysis.