On 7/29/2011 2:53 PM, Brad Roberts wrote:
You keep using the term impossible.
It's the halting problem. How are you going to prove that a->b->c yields the
same result after you've done pretty much any function call?
It's impossible to be 100% correct in
100% of the code bases.
When it is built into the compiler, I think it should be 100%. And frankly, the
marketing of these false positive tools bugs me. They'll run their tool over
some code base, then publish the results and make claims about all these
hundreds of "bugs" they've found. Even worse, others will uncritically read
those pages and assume those code bases are "buggy".
Sure, but that's obviously not the goal. The
goal is to be correct enough on enough code to be useful. A far more
achievable goal. Clang isn't there yet, but with time and effort it can
improve towards that goal. That's where producing test cases on things it
fails on is useful.. standard bug reporting (or feature gap reporting in
this case).
If B can be shown to be a super set of A, which is very doable for a
reasonable set of cases, then that false positive can be eliminated.
Continuing to think of these tools as either perfect or useless and useful
discussions about them are kinda hard to have.
There are two things one can try with static analysis:
1. Flag the code if one cannot prove it is good.
2. Flag the code if one can prove it is bad.
clang is going for (1). I think (2) is more appropriate.
BTW, a while back Spec# was touted here as having this great theorem contract
prover, and what a great tool that was. Reading the documentation on it, it
looked great. So I tried it out in pastebin. It pretty much only works on the
examples given in the marketing literature. It couldn't even handle bitwise ops.
I know enough about data flow analysis to infer what clang is doing from its
pattern of reports, and it hasn't even begun to solve this problem.
As for breaking new ground, I really like what D is doing with value range
propagation in implicit conversions. So far it's been a solid base hit.
