Is it possible to use Frama-C
's slicing plugin to slice for more than one assertion?
E.g. given the following code:
#include "assert.h"
int main() {
double a=3;
double b=4;
b=a+b;
double c=123;
//@ assert(b>=0);
double d=a/b;
c=a;
//@ assert(c==0);
if (a<b)
a=c;
return 0;
}
I would like to get the slice for both assertions.
Option -slice-assert main
will choose as slicing criterion all the assertions of function main
. In fact, you can't directly choose to slice with respect to only one of them. You'd have to resort to //@ slice pragma expr b;
for the first one or //@ slice pragma expr c;
for the second one.
More generally, slicing criteria are cumulative: the more criteria you give, the more code will be kept.