Why don't you verify the entire Internet ?

... or at least the C codebase available on there, anyway?

Don't be fooled by the positive examples presented here and there. Verifying arbitrary programs is still arbitrarily difficult. There is some cherry-picking going on in the results we, and others, present.

In the case of Frama-C's value analysis, dynamic allocation is one issue. This analysis was never intended to analyze programs that use it. I wonder if it would be possible to get interesting results by modelizing the heap as a single large array whose contents are voluntarily kept imprecise. But I never tried, if that tells you how optimistic I am.

Aside: this is purely a limitation of the value analysis plug-in, not of the framework. See for instance this plug-in for an attempt that we are eager to hear more about to handle C programs with dynamic allocation.

Surprisingly often though the reason I do not start a new experiment is not that Frama-C's value analysis couldn't handle the source code but that I couldn't. Functional C code is often ugly — for reasons that given the language and the objectives are unavoidable. The program tries to work as a shared library; it want to compile on 1995's version of DJGPP for MS-DOS; ...

Yesterday at 17:00 I was discovering another gem of simple and efficient code comparable in cleanliness to Skein. And not to boast or anything simply as a measure of how efficient one can be when equipped with the right tool today at the same time I was reporting a tiny flaw in said library that has since been semi-acknowledged by its author.

I'd start a new thread but I haven't finished presenting the analysis of Skein.