Frama-C 26 (Iron): a release with several irons in the fire

Frama-C 26 (Iron) has been released, and as always, it contains several improvements among different plug-ins. In this blog post, we will present some of them, with very short examples. This list of features is based on the main changes since the 25.0 (Manganese) release.

Kernel/Aoraï: ‘calls’ ACSL extension moved from WP to the kernel… and Aoraï now uses it!

The @calls annotation, used to indicate the possible targets of an indirect call via a function pointer, was a WP-exclusive ACSL extension. It is now part of the kernel, which enables other plug-ins, such as Aoraï, to use it.

As a short, albeit contrived example, consider the following code:

// calls.c
/*@ requires a < 16 && b < 16;
    ensures \result == (a + b) % 16; */
unsigned char add4b(unsigned char a, unsigned char b) {
  return (a + b) % 16;
}

/*@ requires a < 16 && b < 16;
    ensures \result == (a * b) % 16; */
unsigned char mul4b(unsigned char a, unsigned char b) {
  return (a * b) % 16;
}

extern int nondet;
int main() {
  unsigned char (*fp)(unsigned char, unsigned char);
  if (nondet) fp = add4b;
  else fp = mul4b;
  unsigned char a = 14;
  unsigned char b = 3;
  /*@ calls add4b, mul4b; */
  return fp(a, b);
}

It contains two functions add4b and mul4b, which are non-deterministically chosen from the main function. In Aoraï, we can specify it in the Ya language using the following file:

// calls.ya
%init: S0;
%accept: Sf;
S0: { CALL(main) } -> S1;
S0: { CALL(main) } -> S2;
S1: { CALL(add4b) } -> Sf;
S2: { CALL(mul4b) } -> Sf;
Sf: -> Sf;

Before Frama-C 26, if we tried to run:

frama-c calls.c -aorai-automata calls.ya

We would get a “unimplemented feature” error message. Now, with Frama-C 26, it works just fine. Note that by default Aoraï will not say anything, since all is fine, but if you want, remove one of the S0:... lines in the calls.ya file and you will get a proper warning.

Eva: new public API; better value reductions

The old Db.Value API, used in them olden Frama-C days, was unintuitive at best and limiting at times. A new API has been under development for quite some time, and it enables derived plug-ins and analyses to get more information, faster, and with a much more readable code.

As an example, here is the difference between a call to the old API and to the new one to evaluate the possible values of an expression expr at a given statement stmt:

-  let r = !Db.Value.eval_expr (Db.Value.get_stmt_state stmt) expr in
+  let r = Eva.Results.(before stmt |> eval_exp expr |> as_cvalue) in

The new API is very flexible: - before stmt selects the program point where the evaluation is performed - here, just before the statement stmt. It could for instance be replaced by after stmt (just after the statement) or at_start_of kf (at the beginning of a function). - Optionally, in_callstack can then be used to restrict the evaluation to a given callstack. - eval_var, eval_lval or eval_expr evaluate the possible values of a variable, an lvalue or an expression respectively. eval_address evaluates the possible addresses of a lvalue. - Finally, functions prefixed by as_ convert the evaluation result into a suitable type: as_ival for an integer interval, as_fval for a floating-point interval, as_cvalue for an abstract value able to represent any scalar type (including pointers), etc.

Many other features are available; you can see the complete API in the Eva.mli file.

The Eva manual also contains an API section which explains more about it.

Better value reductions

Concerning value reductions, here is a minimal example where Frama-C 26 is more precise:

// reduction.c
#include <assert.h>
extern int e;

void main (void) {
  assert (e > 0);
  Frama_C_show_each(e);
}

In Frama-C <= 25, running frama-c reduction.c -eva would result in:

[eva] reduction.c:5: Frama_C_show_each: [-2147483648..2147483647]

Despite the Unknown status from the previous line, no reduction was performed. The user could still do it manually, e.g. adding a //@ admit e > 0; after the assertion, but it was cumbersome.

In Frama-C 26, Eva does reduce the interval of e without extra annotations:

[eva] reduction.c:5: Frama_C_show_each: [1..2147483647]

WP: improved JSON output

To illustrate the difference in the WP JSON report output, we will use the same calls.c file presented in the section related to the Aoraï plug-in. In that file, we have a few annotated functions. We will use the following command:

frama-c calls.c -wp -wp-report-json rep.json

The report in Frama-C 25 was centered around functions, and contained only some general summary information about how many proof obligations there were, which solver proved them, and their status:

{ "wp:global": { "qed": { "total": 19, "valid": 19 },
                 "Alt-Ergo:2.2.0": { "total": 2, "valid": 2, "rank": 11 },
                 "wp:main": { "total": 21, "valid": 21, "rank": 11 } },
  "wp:functions": { "add4b": { "add4b_assigns": { "qed": { "total": 1,
                                                           "valid": 1 },
  ...
}

In Frama-C 26, however, the report is structured around proof goals, and contains more detail about each of them, including the property they relate to, which provers were used, time needed to prove them, etc:

[ { "goal": "typed_add4b_ensures", "property": "add4b_ensures",
    "file": "/frama-c-26/calls.c", "line": 3,
    "function": "add4b", "smoke": false, "passed": true, "verdict": "valid",
    "provers": [ { "prover": "qed", "time": 0.002317, "success": 0 },
                 { "prover": "Alt-Ergo:2.2.0", "time": 0.0097, "success": 1 } ],
    "proved": 1 },
  { "goal": "typed_add4b_assigns", "property": "add4b_assigns",
    "file": "/frama-c-26/calls.c", "line": 4,
    "function": "add4b", "smoke": false, "passed": true, "verdict": "valid",
    "provers": [ { "prover": "qed", "time": 0., "success": 1 } ],
    "proved": 1 },
  ...
]

Summary information from the previous report (such as the total number of goals) can be easily computed from the new data.

E-ACSL: functions returning rationals

The E-ACSL instrumentation of functions returning rational numbers was not handled by Frama-C < 26.

Note that floating-point values (excluding NaNs) are rationals, as well as real functions returning floating-point values; which means the impact was significative. Here is a very minimal example of a program with such a function:

// rational.c
/*@ logic real over(real a, real b) = a/b; */

void main(){
  /*@ assert over(1., 2.) == 0.5; */;
}

With Frama-C 26, running e-acsl-gcc.sh rational.c produces an a.out.frama.c with the expected instrumentation:

...
__gen_e_acsl_over(& __gen_e_acsl_over_2,1.,2.);
__gmpq_init(__gen_e_acsl__2);
__gmpq_set_d(__gen_e_acsl__2,0.5);
__gen_e_acsl_eq = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_over_2),
                             (__e_acsl_mpq_struct const *)(__gen_e_acsl__2));
__e_acsl_assert_register_mpq(& __gen_e_acsl_assert_data,"over(1., 2.)",
                             (__e_acsl_mpq_struct const *)(__gen_e_acsl_over_2));
...

Dive: display of tainted values

The Dive plug-in (Eva-derived, and Ivette-based) is used to help understand the origin of alarms after an analysis with Eva. Its graph-based view provides visualization around precise and imprecise values, as well as between locations and dependencies.

In Frama-C 26, Dive also shows taint-related information, when the Taint domain is enabled (option -eva-domains taint). The screenshot below illustrates this:

In the screenshot, the node tainted represents a tainted (via a //@ taints annotation) location with a violet outline; then some locations which are directly by it (t, both in function taint_call and in taint_basic, as well as x), and a location (y) which is indirectly tainted by it. The code below has been used to produce the screenshot; you can copy it into a file and then run ivette -eva <file> to play with it.

#include <__fc_builtin.h>
volatile int nondet;
int tainted;

void taint_basic(int t) {
  int u, w, x, y = 0;
  int buf[2] = { 0, 1 };
  // Basic direct dependency: 't' is tainted ==> 'x' is (data-)tainted
  x = t + y + 1;
  // Data-dependency overapprox: 'u' may take 't' in else-branch ==>
  // 'u' is (data-)tainted
  if (nondet) u = 1;
  else u = t;
  // Basic control-dependency: 't' is tainted ==> 'w' is (control-)tainted
  if (t > 1) w = 1;
  else w = 2;
  // Indirect dependency: 't' is tainted ==> 'buf[t]' is (control-)tainted
  buf[t] = buf[1] + 1;
}

void taint_call(int t) {
  if (t >= 0)
    taint_basic(t); // call depends on tainted 't' ==>
                    // all left-values appearing in taint_basic are
                    // control-tainted
}

// Taints global variable 'tainted'
void taints (void) {
  tainted = Frama_C_interval(0, 10);
  //@ taint tainted;
}

int main(void) {
  taints();
  taint_basic(tainted);
  tainted = 0;
  taints();
  taint_call(tainted);
  return 0;
}

Ivette: easier installation

Finally, an important feature of this release is a simplified way to install Ivette, the new and experimental Frama-C GUI: after installing Frama-C 26 via opam, you can simply run ivette once to download and install Ivette. Note that this still requires having node and yarn installed, as mentioned in this blog post.

In the long term, Ivette will be distributed pre-packaged; this installation method was provided with Frama-C 26 mostly to make it easier for users, which no longer need to manually download Frama-C’s source archive (or clone it from the public Git repository).

Conclusion

As always, a new Frama-C release brings many improvements, both minor and major, as well as many bug fixes; we hope this post, containing several code examples and a longer description of some chosen new features, will allow for easier experimentation and faster adoption. Do not hesitate to give us feedback about this, whether you prefer it or find it redundant. Strike while the iron is hot!