Tag Archives: OCaml

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

Making OCaml native code 0.5% shorter on Mac OS X
Pascal Cuoq on 7 January 2012

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

Analyzing single-precision floating-point constants
Pascal Cuoq on 14 November 2011

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

A portable OCaml function to print floats
Pascal Cuoq on 29 October 2011

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

Features in Frama-C Nitrogen, part 1
Pascal Cuoq on 14 October 2011

Here 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