Search code examples
frama-cprogram-slicing

Slicing for multiple asserts

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.

Solution

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