Pascal,
A meta-remark for the philosophers: are we all spending a lot of time for not much here? One of the discussions at the SCAM conference that I like for its discussions was whether we shouldn't all be working on Java rather than previous generation, difficult languages that will be obsolete before we produce satisfactory analyses for them.
This rather narrow minded uniformed point of view misses the important question. The question is how the academic tools compare to what commercial providers are supplying for C. I know of several projects that have developed tools like C-smith. The commercial market for such things is very small and nothing much has come of these projects. A comparison of Frama-C against some of the better C tools like QA/C or PC-lint would be interesting. Commercial runtime checking tools come and go very quickly because not enough people like to use them, so probably nothing to compare C-semantics against. -- Derek M. Jones tel: +44 (0) 1252 520 667 Knowledge Software Ltd mailto:derek@knosof.co.uk Source code analysis http://www.knosof.co.uk