Notes to self on frama-c

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.

1 Comment

Filed under Uncategorized

One response to “Notes to self on frama-c

  1. problemchild68

    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!

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.