Frama-C I have just sent a list of changewishes (1 2) to a static analysis competition mailing-list and that reminded me of a blog post I had to write on the strictness of the type-checker in upcoming Frama-C release Oxygen. This is the blog post. This post is not about uninitialized...
Read MoreContext A facetious colleague who claims that he should be better writing his thesis but keeps committing Coq and OCaml files on Frama-C's repository, asked me the following question: Is there a function in Frama-C's kernel that can fold[1] a function over all types that appear in a C program?...
Read MoreI reported bug 785 after getting three-quarters sure that the problem was in Frama-C (I used two different versions of GCC as oracles). I still cannot believe how twisted integer promotion rules are in C99. I had read them before but I had not followed the precise path I followed...
Read MoreEvery once in a while, someone asks about single-precision floating-point support in Frama-C. Until recently it was often in the context of the value analysis, but actually, thanks to a lot of interesting new results obtained in the context of this project people working on deductive verification within Frama-C can...
Read More