Frama-C is a giant modular system for writing formal proofs of C code. For months I’ve been on-and-off trying to see if we could use it to do useful proofs for any parts of the projects we write, like qemu, libvirt, libguestfs, nbdkit etc. I got side-tracked at first with this frama-c tutorial which is fine, but I got stuck trying to make the GUI work.
Yesterday I discovered this set of 3 short command-line based tutorials: https://maniagnosis.crsr.net/2017/06/AFL-brute-force-search.html https://maniagnosis.crsr.net/2017/06/AFL-bug-in-quicksearch.html https://maniagnosis.crsr.net/2017/07/AFL-correctness-of-quicksearch.html
I thought I’d start by trying to apply this to a small section of qemu code, the fairly self-contained range functions.
The first problem is how to invoke frama-c:
frama-c -wp -wp-rte -wp-print util/range.c -cpp-extra-args=" -I include -I build -I /usr/include -DQEMU_WARN_UNUSED_RESULT= "
You have to give all the include directories and define out some qemu-isms.
The first time you run it, this won’t work for “reasons”. You have to initialize the why3 verifier using:
why3 config --full-config
Really frama-c should just do this for you, or at least tell you what you need to do in the obscure error message it prints.
This still won’t work because
util/range.c includes glib headers which use GCC attributes and builtins and frama-c simply cannot parse any of that. So I ended up hacking on the source to replace the headers with standard C headers and remove the one glib-based function in the file.
At this point it does compile and the frama-C WP plugin runs. Of course without having added any annotations it simply produces a long list of problems. Also it takes a fair bit of time to run, which is interesting. I wonder if it will get faster with annotations?
That’s as far as I’ve got for the moment. I’ll come back later and try to add annotations.
One response to “Notes to self on frama-c”
Hi Richard, my first taste of Formal proofs was “Z” in university. Proving anything non-trivial is well …non trivial. I’ll be interested to see how this system works on your code..What kind of problems does it find and hows does it improve your output and how does it effect your productivity.
Lots of questions …it’ll be nice to see answers when you have some more experience of the tool!