Tag Archives: CIL

Oxygen is stricter about types and why you should get used to it
Pascal Cuoq on 27 July 2012

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 More

Iterating over the AST
Virgile Prevosto on 21 May 2012

Context 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 More

C99 promotion rules: what ?!
Pascal Cuoq on 11 April 2011

I 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 More

IEEE 754 single-precision numbers in Frama-C
Pascal Cuoq on 20 November 2010

Every 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