Which Frama-C version is best suited to develop a slicing plugin?

Question

I want to explore Frama-C to apply Assertion-based Slicing (using ACSL notation). I have found that there are several different versions of Frama-C with some different features. My question is which version is best suited to develop a a slicing plugin to Frama-C and to manipulate the AST created by Frama-C.

Answer 1

There already is a slicing plug-in in Frama-C (in all versions).

This plug-in uses the results of the value analysis plug-in, which assumes the properties written inside ACSL assertions (after having attempted to verify them).

So, depending on what you call “assertion-based slicing” (and be aware that the article that comes up first in Google is behind a paywall), what you propose to do may already exists as a Frama-C plug-in (and one that works pretty well as of the last two or three Frama-C versions).

To answer your question anyway, the best version to use is the latest one, which is Fluorine 20130601 as of this writing.

---

Example of existing slicing features in Frama-C:

$ cat t.c
int f(unsigned int x)
{
  int y;
  /*@ assert x == 0 ; */
  if (x)
    y = 9;
  else
    y = 10;
  return y;
}

$ frama-c -sparecode t.c -main f 
...
t.c:4:[value] Assertion got status unknown.
...
/* Generated by Frama-C */
int f(unsigned int x)
{
  int y;
  /*@ assert x ≡ 0; */
  ;
  y = 10;
  return (y);
}

Is the above what you have in mind when you speak of “assertion-based slicing”?

Note: Frama-C's option -sparecode is a slicing option for the criterion “preserve all results of the program”. It still removes any statement that is without consequences, such as y=3; in y=3; y=4;, and being based on Frama-C's value analysis, it removes anything that is considered unreachable or without consequences because of the value analysis' results.

Another example to illustrate:

$ cat t.c
int f(unsigned int x)
{
  int y;
  int a, b;
  int *p[2] = {&a, &b};
  /*@ assert x == 0 ; */  
  a = 100;
  b = 200;
  if (x)
    y = 9;
  else
    y = 10;
  return y + *(p[x]);
}

$ frama-c -sparecode t.c -main f 
...
t.c:6:[value] Assertion got status unknown.
...
/* Generated by Frama-C */
int f(unsigned int x)
{
  int __retres;
  int y;
  int a;
  int *p[2];
  p[0] = & a;
  /*@ assert x ≡ 0; */
  ;
  a = 100;
  y = 10;
  __retres = y + *(p[x]);
  return (__retres);
}