多个断言的切片

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

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

多个断言的切片

Slicing for multiple asserts

frama-c

program-slicing