Frama-C:获取 C 断言语句的切片

Frama-C: Get slice for C assert statement

有没有办法使用 Frama-C 的切片插件来计算特定 C assert 语句的切片?

例如,给定以下代码:

int main() {
    double a=3;
    double b=4;
    double c=123;

    assert(b>=0);

    double d=a/b;
    c=a;

    return 0;
}

我想为 assert(b>=0); 获取以下切片:

int main() {
    double b=4;

    assert(b>=0);

    return 0;
}

如果您可以将断言重写为 ACSL 断言,则可以使用选项 -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;
}

(在这种情况下,除法也将被删除,因为它不影响断言。)

void main(void)
{
  double b;
  b = (double)4;
  /*@ assert b ≥ 0; */ ;
  return;
}

或者,您也可以使用 -slice-calls assert.

分割对 assert 函数的调用
void main(void)
{
  double b;
  b = (double)4;
  assert(b >= (double)0);
  return;
}

如果要对特定断言进行切片(如果函数中有多个断言),则必须使用切片编译指示或程序化 API(不推荐)。