Tag Archives: developer

Never forget to sanitize your input
Virgile Prevosto on 19 September 2012

This post is a follow up of this one A facetious colleague pointed out to me that the print_stmt function that is used to display the CFG in the post mentioned above behaves incorrectly when used over code that include string constants such as the one below: void f(const char...

Read More

Extracting information from Frama-C programmatically
Virgile Prevosto on 4 September 2012

Extending the framework Some time ago, one of our fellow users asked us whether it was possible to extract the control-flow graph (CFG) of C functions from Frama-C. Fact is, although the CFG is computed during the elaboration of the AST, nothing exists currently to present the information to the...

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