Frama-C A meta-article on benchmarking Some colleagues and I are about to submit this article on the subject of benchmarking static analyzers. Rather than another benchmark it is a list of general recommendations and pitfalls when benchmarking static analyzers. The article is illustrated on C program constructs because that's what we...
Read MoreFrama-C has a mailing-list. It's a place people visit for free to complain that they are not getting the quality, technical, detailed answers that they deserve, and to tell us what our priorities should be. I expressed my opinion about the mailing list a long time ago in this very...
Read MoreThis post is a follow-up of bug 990. When this issue was resolved the following question arose: "Why is it so dangerous to have a global c declared as a pointer in one compilation unit and defined as an array in another one given the fact that almost anywhere an...
Read MoreIf you like this blog, then on the basis of recent posts, you will with good probability like that blog. The recent posts I have read all deal with various subtle undefined behaviors in C.
Read MoreThe function in this post to the musl mailing list is a good candidate for formal verification. It should just barely be possible to verify the absence of undefined behaviors with Frama-C's value analysis and it should just barely be possible to verify it functionally with one of the Jessie...
Read More