frama-cprogram-slicing

Frama-C: Get slice for C assert statement


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

Solution

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