对多个断言进行切片

Question

是否可以使用Frama-C 的切片插件对多个断言进行切片？

例如给出以下代码：

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

我想获得两个断言的切片。

Answer 1

选项-slice-assert main 将选择函数main 的所有断言作为切片标准。实际上，您不能直接选择仅针对其中一个进行切片。对于第一个，您必须诉诸 //@ slice pragma expr b;，对于第二个，您必须诉诸 //@ slice pragma expr c;。

更一般地说，切片标准是累积的：您提供的标准越多，保留的代码就越多。