Is there a way to use Frama-C
's slicing plugin to compute slices for a specific C assert
statement?
For example, given the following code:
int main() {
double a=3;
double b=4;
double c=123;
assert(b>=0);
double d=a/b;
c=a;
return 0;
}
I would like to get the following slice for assert(b>=0);
:
int main() {
double b=4;
assert(b>=0);
return 0;
}
If you can rewrite your assert as an ACSL assertion, you can use option
-slice-assert main
.(In this case, the division will also be removed, as it does not influence the assertion.)
Alternatively, you can also slice on the calls to the
assert
function, using-slice-calls assert
.If you want to slice on a particular assertion (if there are more than one in the function), you will have to use a slicing pragma, or the programmatic API (not recommended).