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);
}