Frama-C is a full-fledged framework

I wish researchers would stop calling the plug-in they are using \Frama-C". "Frama-C" is the framework. It has very few of the properties that are attributed to it. One plug-in or the other usually is to blame or praise.

This is not just because when researchers bring it up it is usually to say something bad about it: everyone has a bridge they want to sell you. A consequence is that you hear more often "Frama-C does not support recursion" "Frama-C does not handle pointer casts" or generally "this bridge is so much better than Frama-C" than "Frama-C is great: it can verify this binary search implementation and it finds the overflow that Google engineers pointed out" or "Frama-C found a subtle bug in QuickLZ that had escaped 'a year of beta testing regression testing code reviewing and static analysis tooling'". No what irks me is that researchers are supposed to be scientists. All the fictional quotes above are true and they are all false and they are generally so fuzzy as to be worthless. They remind me of example sentences that Richard Feynman would give when talking about the scientific method — and I don't mean "example" as in "good example".

For each of the quotes above the author is clearly talking about some plug-in but the reader hearing about Frama-C for the first time gets a completely distorted view of what it is what it can do and what it is all about.

And did I mention that the property attributed to it that will form the reader's first impression is usually both negative and unfair?