Frama-C: Get slice for C assert statement

Question

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

Answer 1

If you can rewrite your assert as an ACSL assertion, you can use option -slice-assert main.

int main() {
    double a=3;
    double b=4;
    double c=123;

    //@ assert(b>=0);

    double d=a/b;
    c=a;

    return 0;
}

(In this case, the division will also be removed, as it does not influence the assertion.)

void main(void)
{
  double b;
  b = (double)4;
  /*@ assert b ≥ 0; */ ;
  return;
}

Alternatively, you can also slice on the calls to the assert function, using -slice-calls assert.

void main(void)
{
  double b;
  b = (double)4;
  assert(b >= (double)0);
  return;
}

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).