How to use Frama-C in the command line

Yesterday, I wrote a blog about using ChatGPT and Frama-C together. The funny thing is the work to set up Frama-C was such a hassle itself that I deemed it deserves its own article.

Last time I used Frama-C was like 2018 and I haven’t been keeping up with its status, but I remembered using it in a GUI program interactively. Imagine my surprise when, after following the instructions on their website to install it on my Macbook, this happened:

$ frama-c-gui
...
zsh: segmentation fault  frama-c-gui

It seg-faulted. I didn’t know what to do. I Googled around for a long while but no solution was found. I then re-read the install message from opam, which says:

Ivette is a new GUI for Frama-C, currently in development.

Huh. They have a new GUI now? I went back to their website to investigate. It turned out that, according to INSTALL.md, as of February 2023,

The traditional GTK-based Frama-C GUI no longer works on macOS!

You need to use Ivette, the new Frama-C graphical interface. Instructions on installing and running it are presented by opam when the frama-c package is installed. Follow them to get Ivette running.

Well, shit. I guess I better check out this Ivette thing. I followed the instructions to set it up. The new design does look pretty good; it’s much better than the old one. I tried it on some source files, but I couldn’t find any of the functionalities that the old GUI had. I then discovered that:

Ivette is currently for Eva; WP and others will follow later

Fuck. Arguably the most important plugin, WP, is not on Ivette yet.

What do I do now? The way I saw it, I had three options:

Wait until WP is on Ivette
Use a different OS and use the old GUI
Use the frama-c command line tool

There’s no way I’m waiting for god knows how long until it’s on there, and I, along with most people, I believe, learned Frama-C by using the GUI. So yesterday, I went with option 2. I set up an entire Ubuntu VM just to use frama-c-gui the old way.

Today, I thought I’d give frama-c the command line tool a go. I have not yet found any Frama-C tutorial on the Internet that teaches it with the command line tool instead of the old GUI, but I thought to myself, how hard could it be? (very)

I tried it on some random file but looks like all it did was parse it.

$ frama-c sort.c
[kernel] Parsing sort.c (with preprocessing)

Naturally, I’d then try to get some form of help message:

$ frama-c --help

This is Frama-C 26.1 (Iron)

Usage:
    frama-c [options files ...]

Main Options:
    -help        This message.
    -version     Version number only.
    -plugins     List of installed plugins.
    -kernel-h    Additional help and options.

Plug-in Options:
    -<plugin>    Plug-in activation.
    -<plugin>-h  Additional help and options.

… and that wasn’t helpful at all. I sighed deeply. I decided to get in the mud myself and trudge through the manuals.

I started reading the Frama-C User Manual. In “3.3.1 Getting Help”, my previous confusion was dissipated. You have to use the option -<plug-in shortname>-help to get the help message of a specific plugin. It works!

$ frama-c -wp-help
Plug-in name: WP
Plug-in shortname: wp
Description: Proof by Weakest Precondition Calculus

Most options of the form '-wp-option-name' and without any parameter
have an opposite with the name '-wp-no-option-name'.

Most options of the form '-option-name' and without any parameter
have an opposite with the name '-no-option-name'.

Options taking a string as argument should preferably be written
-option-name="argument".

***** LIST OF AVAILABLE OPTIONS:
...

Now I switched to the WP User Manual. Luckily, there is a tutorial section right at the start of the book at “1.2 Tutorial”. From there, I learned that you should run WP like this:

$ frama-c -wp sort.c
[kernel] Parsing sort.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 34 goals scheduled
[wp] [Timeout] typed_SWAP_ensures (Qed 5ms) (Alt-Ergo 10s)
[wp] [Timeout] typed_sortNetwork_ensures (Qed 35ms) (Alt-Ergo 10s)
[wp] [Timeout] typed_sortNetwork_ensures_2 (Qed 27ms) (Alt-Ergo 10s)
[wp] Proved goals:   31 / 34
  Qed:              26
  Alt-Ergo 2.4.3:    5 (12ms-4.7s-10s)
  Timeout:           3

sort.c is from yesterday’s article:

/*@ requires \valid(a+i) && \valid(a+j);
    assigns a[i], a[j];
    ensures a[i] <= a[j];
    ensures (a[i] == \old(a[i]) && a[j] == \old(a[j])) ||
            (a[i] == \old(a[j]) && a[j] == \old(a[i]));
 */
void SWAP(int a[], int i, int j) {
    if (i != j) {  // Only swap if the indices are different
        int temp = a[i];
        a[i] = a[j];
        a[j] = temp;
    }
}

/*@ requires \valid(a + (0..4));
    assigns a[0..4];

    // the array elements at method return are sorted
    ensures sorted : \forall integer i; 0 <= i <= 3 ==> a[i] <= a[i+1];

    // the array elements at method return are a permutation of the initial elements
    ensures \forall integer i; 0 <= i <= 4 ==>
            (\exists integer j; 0 <= j <= 4 && a[i] == \old(a[j]));
    ensures \forall integer i; 0 <= i <= 4 ==>
            (\exists integer j; 0 <= j <= 4 && \old(a[i]) == a[j]);
 */
void sortNetwork(int a[]) {
    SWAP(a, 0, 1);
    SWAP(a, 3, 4);
    SWAP(a, 2, 4);
    SWAP(a, 2, 3);
    SWAP(a, 0, 3);
    SWAP(a, 0, 2);
    SWAP(a, 1, 4);
    SWAP(a, 1, 3);
    SWAP(a, 1, 2);
}

Nice. From the last few lines you can tell it proved 31 out of 34 goals where 26 were proved with Qed and 5 with Alt-Ergo and then there are 3 timeouts.

However, the middle part looks a bit cryptic. I assume those are the timed-out cases, but what exactly are those properties? I can’t tell which ensures from my source code is the typed_sortNetwork_ensures_2 here.

Enter the Report plug-in. Apparently, you can just run it like this:

$ frama-c -wp sort.c -then -report
[kernel] Parsing sort.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 34 goals scheduled
[wp] [Timeout] typed_SWAP_ensures (Qed 5ms) (Alt-Ergo 10s)
[wp] [Timeout] typed_sortNetwork_ensures (Qed 36ms) (Alt-Ergo 10s)
[wp] [Timeout] typed_sortNetwork_ensures_2 (Qed 26ms) (Alt-Ergo 10s)
[wp] Proved goals:   31 / 34
  Qed:              26
  Alt-Ergo 2.4.3:    5 (11ms-4.7s-10s)
  Timeout:           3
[report] Computing properties status...

--------------------------------------------------------------------------------
--- Properties of Function 'SWAP'
--------------------------------------------------------------------------------

[  Valid  ] Pre-condition (file sort.c, line 6)
            by Call Preconditions.
[    -    ] Post-condition (file sort.c, line 8)
            tried with Wp.typed.
[  Valid  ] Post-condition (file sort.c, line 9)
            by Wp.typed.
[  Valid  ] Assigns (file sort.c, line 7)
            by Wp.typed.
[    -    ] Default behavior
            tried with Frama-C kernel.

--------------------------------------------------------------------------------
--- Properties of Function 'sortNetwork'
--------------------------------------------------------------------------------

[  Valid  ] Post-condition 'sorted'
            by Wp.typed.
[    -    ] Post-condition (file sort.c, line 28)
            tried with Wp.typed.
[    -    ] Post-condition (file sort.c, line 30)
            tried with Wp.typed.
[  Valid  ] Assigns (file sort.c, line 22)
            by Wp.typed.
[    -    ] Default behavior
            tried with Frama-C kernel.
[  Valid  ] Instance of 'Pre-condition (file sort.c, line 6)' at call 'SWAP' (file sort.c, line 34)

            by Wp.typed.
[  Valid  ] Instance of 'Pre-condition (file sort.c, line 6)' at call 'SWAP' (file sort.c, line 35)

            by Wp.typed.
[  Valid  ] Instance of 'Pre-condition (file sort.c, line 6)' at call 'SWAP' (file sort.c, line 36)

            by Wp.typed.
[  Valid  ] Instance of 'Pre-condition (file sort.c, line 6)' at call 'SWAP' (file sort.c, line 37)

            by Wp.typed.
[  Valid  ] Instance of 'Pre-condition (file sort.c, line 6)' at call 'SWAP' (file sort.c, line 38)

            by Wp.typed.
[  Valid  ] Instance of 'Pre-condition (file sort.c, line 6)' at call 'SWAP' (file sort.c, line 39)

            by Wp.typed.
[  Valid  ] Instance of 'Pre-condition (file sort.c, line 6)' at call 'SWAP' (file sort.c, line 40)

            by Wp.typed.
[  Valid  ] Instance of 'Pre-condition (file sort.c, line 6)' at call 'SWAP' (file sort.c, line 41)

            by Wp.typed.
[  Valid  ] Instance of 'Pre-condition (file sort.c, line 6)' at call 'SWAP' (file sort.c, line 42)

            by Wp.typed.

--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
    14 Completely validated
     5 To be validated
    19 Total
--------------------------------------------------------------------------------

And there it is! It shows the properties’ line numbers so we know how to link between them. We can immediately make this more readable by adding labels to the properties:

/*@ requires valid_ptrs: \valid(a+i) && \valid(a+j);
    assigns              a[i], a[j];
    ensures         leq: a[i] <= a[j];
    ensures    preserve: (a[i] == \old(a[i]) && a[j] == \old(a[j])) ||
                         (a[i] == \old(a[j]) && a[j] == \old(a[i]));
 */
void SWAP(int a[], int i, int j) {
    if (i != j) {  // Only swap if the indices are different
        int temp = a[i];
        a[i] = a[j];
        a[j] = temp;
    }
}

/*@ requires valid_ptrs: \valid(a + (0..4));
    assigns              a[0..4];
    ensures      sorted: \forall integer i; 0 <= i <= 3 ==> a[i] <= a[i+1];
    ensures permutation: \forall integer i; 0 <= i <= 4 ==>
                         (\exists integer j; 0 <= j <= 4 && a[i] == \old(a[j]));
    ensures permutation: \forall integer i; 0 <= i <= 4 ==>
                         (\exists integer j; 0 <= j <= 4 && \old(a[i]) == a[j]);
 */
void sortNetwork(int a[]) {
    SWAP(a, 0, 1);
    SWAP(a, 3, 4);
    SWAP(a, 2, 4);
    SWAP(a, 2, 3);
    SWAP(a, 0, 3);
    SWAP(a, 0, 2);
    SWAP(a, 1, 4);
    SWAP(a, 1, 3);
    SWAP(a, 1, 2);
}

And the report will use the labels:

$ frama-c -wp sort.c -then -report
[kernel] Parsing sort.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 34 goals scheduled
[wp] [Timeout] typed_SWAP_ensures_leq (Qed 6ms) (Alt-Ergo 10s)
[wp] [Timeout] typed_sortNetwork_ensures_permutation (Qed 35ms) (Alt-Ergo 10s)
[wp] [Timeout] typed_sortNetwork_ensures_permutation_2 (Qed 28ms) (Alt-Ergo 10s)
[wp] Proved goals:   31 / 34
  Qed:              26
  Alt-Ergo 2.4.3:    5 (10ms-4.7s-10s)
  Timeout:           3
[report] Computing properties status...

--------------------------------------------------------------------------------
--- Properties of Function 'SWAP'
--------------------------------------------------------------------------------

[  Valid  ] Pre-condition 'valid_ptrs'
            by Call Preconditions.
[    -    ] Post-condition 'leq'
            tried with Wp.typed.
[  Valid  ] Post-condition 'preserve'
            by Wp.typed.
[  Valid  ] Assigns (file sort.c, line 6)
            by Wp.typed.
[    -    ] Default behavior
            tried with Frama-C kernel.

--------------------------------------------------------------------------------
--- Properties of Function 'sortNetwork'
--------------------------------------------------------------------------------

[  Valid  ] Post-condition 'sorted'
            by Wp.typed.
[    -    ] Post-condition 'permutation'
            tried with Wp.typed.
[    -    ] Post-condition 'permutation'
            tried with Wp.typed.
[  Valid  ] Assigns (file sort.c, line 20)
            by Wp.typed.
[    -    ] Default behavior
            tried with Frama-C kernel.
[  Valid  ] Instance of 'Pre-condition 'valid_ptrs'' at call 'SWAP' (file sort.c, line 28)

            by Wp.typed.
[  Valid  ] Instance of 'Pre-condition 'valid_ptrs'' at call 'SWAP' (file sort.c, line 29)

            by Wp.typed.
[  Valid  ] Instance of 'Pre-condition 'valid_ptrs'' at call 'SWAP' (file sort.c, line 30)

            by Wp.typed.
[  Valid  ] Instance of 'Pre-condition 'valid_ptrs'' at call 'SWAP' (file sort.c, line 31)

            by Wp.typed.
[  Valid  ] Instance of 'Pre-condition 'valid_ptrs'' at call 'SWAP' (file sort.c, line 32)

            by Wp.typed.
[  Valid  ] Instance of 'Pre-condition 'valid_ptrs'' at call 'SWAP' (file sort.c, line 33)

            by Wp.typed.
[  Valid  ] Instance of 'Pre-condition 'valid_ptrs'' at call 'SWAP' (file sort.c, line 34)

            by Wp.typed.
[  Valid  ] Instance of 'Pre-condition 'valid_ptrs'' at call 'SWAP' (file sort.c, line 35)

            by Wp.typed.
[  Valid  ] Instance of 'Pre-condition 'valid_ptrs'' at call 'SWAP' (file sort.c, line 36)

            by Wp.typed.

--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
    14 Completely validated
     5 To be validated
    19 Total
--------------------------------------------------------------------------------

Now you know how to use Frama-C/WP in the command line!

In the old GUI program, I often tweaked some parameters, like which prover to use, how long is the timeout, etc., and I find that you can pretty easily find how to use them from the -wp-help. For example, you can do:

$ frama-c -wp -wp-rte -wp-prover cvc4 -wp-timeout 30  sort.c -then -report

I’m sure there’s a lot more to this, and I’m eager to find out!