<div class="gmail_quote">On Fri, Jul 29, 2011 at 4:51 PM, bearophile <span dir="ltr"><<a href="mailto:bearophileHUGS@lycos.com">bearophileHUGS@lycos.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">

Walter:<br>
<div class="im"><br>
> BTW, a while back Spec# was touted here as having this great theorem contract<br>
> prover, and what a great tool that was. Reading the documentation on it, it<br>
> looked great. So I tried it out in pastebin. It pretty much only works on the<br>
> examples given in the marketing literature. It couldn't even handle bitwise ops.<br>
<br>
</div>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)</blockquote><div><br>Woah Woah Woah<br>If that's the purpose, why the hell would they be using C#? Have they proven the entire CLR as well?<br>

 </div><blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">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.<br>


<div class="im"><br>
<br>
> I know enough about data flow analysis to infer what clang is doing from its<br>
> pattern of reports, and it hasn't even begun to solve this problem.<br>
<br>
</div>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).<font color="#888888"><br>

</font></blockquote><div><br>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. <br>

</div></div><br>