Clang static analysis results for dmd

[Andrew Wiley]

On Fri, Jul 29, 2011 at 4:51 PM, bearophile <bearophileHUGS at lycos.com>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)


Woah Woah Woah
If that's the purpose, why the hell would they be using C#? Have they proven
the entire CLR as well?


> 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.
>
>
> > 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. Its creators have created a good C++
> compiler in a very short time, and its back-end is already rivalling GCC in
> optimizations (it's not there yet, but the distance is not so much,
> auto-vectorization is one of the most important differences between the two
> back-ends).
>

I've seen several times that a major feature of a lint tool was that you
could disable warnings of certain types, which is necessary because there
are just too many false positives. Clang will doubtlessly get better, but
the fact will still remain that C and C++ are terrible languages to try to
run static analyses on.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.puremagic.com/pipermail/digitalmars-d/attachments/20110729/9241bc1f/attachment.html>