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

Question

有没有办法使用Frama-Cslicing 插件来计算特定 Cassert语句的切片？

例如，给定以下代码：

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

score 5 · Accepted Answer

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

1 回答 1