Clang static analysis results for dmd

[Walter Bright]

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.