Frama-C 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 MoreMac OS X and assembly labels A few months ago, I was moving things around in Zarith. It's a good way to relax not unlike gardening. And then I noticed something strange. On Mac OS X a label in assembly code is marked as local by prefixing it with "L"...
Read MoreThe previous post on this blog points out how subtle just floating-point constants can be. In a previous previous post exactly one year ago I was already alluding to these difficulties in the context of Frama-C's front-end. Programming a code analyzer that can answer question 5 How should the program...
Read MoreFor printing the results of automated Frama-C tests, we need printing functions with the following properties: they should print all the information available (doing otherwise might mask an existing bug); they should produce results readable enough for a person to validate the result of each test once; and their output...
Read MoreHere is a series of posts that highlight interesting features in the recently released Frama-C Nitrogen 20111001. There is new functionality in Nitrogen, that we hope will entice both existing and prospective users. Other improvements yet will only have meaning for existing users. I will start off with two items...
Read More