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

Question

有没有办法使用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;
}

Answer 1

如果您可以将断言重写为 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（不推荐）。