frama-c - 複数のアサートのスライス

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

Option-slice-assert mainは、 function のすべてのアサーションをスライス基準として選択しますmain。実際、そのうちの 1 つだけに関してスライスすることを直接選択することはできません。//@ slice pragma expr b;最初のものまたは2番目のものに頼る必要が//@ slice pragma expr c;あります。

より一般的には、スライス基準は累積的です。指定する基準が多いほど、より多くのコードが保持されます。