3

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;
}
Paddre
  • 798
  • 1
  • 9
  • 19

1 Answers1

5

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

byako
  • 3,372
  • 2
  • 21
  • 36
  • I need to slice for a particular statement in the code (thus I assume that there are multiple ones). So I thought about developing a Frama-C plugin which does the job. Would you recommend doing that? Or is that what you meant by "`programmatic API (not recommended)`"? Alternatively I could preprocess the Frama-C-preprocessed code using regular expressions. – Paddre Mar 20 '16 at 16:36
  • Also I guess that if there is more than one assert statements in the code and I want to slice on a particular one, it would suffice to convert that statement into an ACSL assertion, wouldn't it? – Paddre Mar 20 '16 at 16:59
  • For this kind of thing, perhaps you should use a slicing pragma as described in http://frama-c.com/slicing.html. Basically, just write `/*@ slice pragma stmt; */`, and use option `-slice-pragma`. – byako Mar 27 '16 at 11:47