Frama-C: Get slice for C assert statement

Viewed 237

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;
}
1 Answers
Related