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

Question

有没有一种方法可以使用Frama-Cslicing插件为特定的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断言，则可以使用option -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;
}

另外，您也可以使用来分割对assert函数的调用-slice-calls assert。

void main(void)
{
  double b;
  b = (double)4;
  assert(b >= (double)0);
  return;
}

如果要切片特定的断言（如果函数中有多个断言），则必须使用切片编译指示或编程API（不建议使用）。