frama-c - 对多个断言进行切片

Question

是否可以使用Frama-C's 切片插件来切片多个断言？

例如，给出以下代码：

#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

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

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