Clang static analysis results for dmd

[Walter Bright]

On 7/29/2011 4:51 PM, bearophile wrote:
> Walter:
>
>> 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.
>
> You are missing something important. The purpose of Spec# (and newer things
> that are coming out now) is to create a small kernel (for an operating
> system) that is 100% proved correct (correct according to its specs, etc). If
> they don't use an automatic theorem prover, then they have to do 100% of the
> proofs by hand. Even if the tool is able to do only 30% of the proofs
> automatically (and another 40% with a bit of help) it's a lot of manual work
> saved. The papers report the percentage of the theorems done by the tool, the
> percentage of the theorems done partially by hand, and the remaining
> percentage done by hand. The source code is all available, to verify the
> numbers inside the papers are not made up.

 From the way you originally positioned it, I had higher expectations.


>> 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.
>
> Clang static analysis is a very new sub-tool. On the market there are
> commercial lint tools that are probably 15-18 times older than Clang. Give
> Clang two or three years are we'll see.

I think you misunderstand the scope of this problem. They've done data flow 
analysis, an off-the-shelf technology for the last 30 years at least. They 
haven't done any of the hard stuff that I can see.

It's like doing natural language translation using a dictionary. It looks like 
it'll work, and you can have promising early success with it, but then you hit a 
wall.