Frama-C description

A webpage hosted on fedoraproject.org describes Frama-C as follows. I'm quoting the paragraph entirely although it is copyrighted by Red Hat Inc. and others. If I'm not too lazy I will criticize thoroughly which will make this fair use.

frama-c is a C source code analysis tool which may be used standalone or integrated with Emacs. frama-c includes a source browser and can calculate simple metrics such as sloc call depth and cyclomatic complexity for a project. It can also generate simple call graphs. Various assertions about the code may be tested and the code may be validated against a number of theorems. frama-c accepts user written plugins for additional custom analyses. More information on frama-c may be found at http://frama-c.com/.

"Frama-C" is proper. I know that developers are first to take liberties (OCaml variable names must start with lowercase. Many contexts do not accept dashes inside names. Unix commands traditionally are all lowercase etc.). This much is entirely our fault.

And now that I think of it it would be too easy to poke fun at someone who had to write a summary for a dozen comparably obscure tools that day so I will leave the jokes implied after all. At least it does not say Frama-C only has intervals dammit! Ok I'm done now. Where was I? Ah yes. Apparently this page is some sort of wiki. Have you heard of them? They are pages on the internet that you can modify. Perhaps it wouldn't be appropriate for someone who isn't a Fedora user to go there and fix the description. But if you are reading this blog and are not a Frama-C developer and happen to use Fedora then you can probably think of a better description and it is morally acceptable for you to offer it on that wiki.

PS: so much for fair use. Does implied criticism count? Well sue me.

PPS: the list of alarms detected by the value analysis is "uninitialized access use of a dangling pointer overflows in signed integer arithmetics invalid memory access invalid comparison of pointers division by zero undefined logical shift overflows in conversions from floating-point to integer infinite or NaN resulting from a floating-point operation undefined side-effects in expressions".