I agree with your post, though I am curious to know if there is any use for "this function is likely to terminate" inside static analysis.
How this guarantee is possible, despite the halting problem, is because he designs an abstract representation of the program being analyzed. It loses a lot of information, but by using it, one can actually prove things about the program.
I would rather say: the halting problem shows that there exists at least one program for which it is impossible to prove termination - not that every termination problem is undecidable, as the trivial example "return 5;" shows.
The conclusion "this function is likely to terminate" may not be helpful, but "this function is likely to leak memory" may be extraordinarily helpful.
The reason that everyone brings up the halting problem in this context is not that we want to test programs if they halt. (Well, we may, but we're generally looking for other behaviors.) It's because for some behaviors, if you want to be able to handle all cases, then that problem can be reduced to the halting problem. Matt provides an excellent demonstration of this with array indices.
I'm confused by your restatement, because it does not restate what I said. You're talking about the halting problem. I'm talking about proving general behaviors in programs, despite the theoretical result that solving the halting problem is impossible, and that many behaviors can be reduced to the halting problem. The solution, as Matt explains, is to find ways to describe behaviors so they do not reduce to the halting problem. Using this technique, you still can have false negatives ("I don't know"), but you can guarantee no false positives.
PREfix incorporated analysis to identify likely exit functions. This help cut down false positives in situations like
if (p == NULL)
fatal_error();
*p = 0;
With the inference-based analysis we did in PREfix, if we don't recognize fatal_error() as a function that's likely to exit the program, we'd report a potential NULL pointer on the next line. But we didn't have the source code for fatal_error, how could we possibly know that? Ideally it would be a volatile function but a lot of older code is very sloppy about that. So we employed various heuristics based on the names of the functions (and gave the user an opportunity to tune the results) ... it worked surprisingly well in practice.
I am curious to know if there is any use for "this function is likely to terminate" inside static analysis.
Well, something like "this condition is likely to be true" could help give an estimate for whether a loop will run many times, which leads to things like a better estimate for the cost of spilling to the stack values used in that loop instead of keeping them in registers.
the halting problem shows that there exists at least one program for which it is impossible to prove termination
I'm not sure that "every halting checker has some input where it gives the wrong answer" permits the conclusion "there is some input where they all give the wrong answer." Is "the machine must generate a proof of its answer" what lets you make that extra leap?
How this guarantee is possible, despite the halting problem, is because he designs an abstract representation of the program being analyzed. It loses a lot of information, but by using it, one can actually prove things about the program.
I would rather say: the halting problem shows that there exists at least one program for which it is impossible to prove termination - not that every termination problem is undecidable, as the trivial example "return 5;" shows.