如何指示WP不要分析死代码或无法访问的代码

Question

在以下代码上运行命令

frama-c test.c -rte -eva -eva-slevel 1 then -wp

时，我得到以下结果：

• Frama-c 24：没有错误
• Frama-c 25/26：无法访问和死亡

  test

  函数中的溢出

int test(int a, int b)
{
  return a+b;
}

int main(void)
{
  return 0
}

从版本 25 开始，WP 似乎正在尝试证明 RTE 插件添加的所有注释，即使是在死代码或无法访问的代码中。 我没有找到任何 WP 选项来取消选择无法访问的属性。

有没有办法告诉 WP 不要选择无效或无法访问的属性？

Answer 1

WP 目标选择

命令行的简单方法是使用

-wp-fct

或

-wp-skip-fct

而不仅仅是

-wp

。因此，在您的示例中，运行以下任一命令（我删除了

-rte

之前的

-eva

并将其与 WP 调用放在一起）：

frama-c test.c -eva -eva-slevel 1 -then -wp-rte -wp -wp-fct main
frama-c test.c -eva -eva-slevel 1 -then -wp-rte -wp -wp-skip-fct test

根据文档：

• -wp

  为所有（选定的）财产生成证明义务。

• -wp-fct <f1 ,...,fn >

  选择功能注释

  f1 ,...,fn

  （默认为所有功能）。

• -wp-skip-fct <f1 ,...,fn >

  忽略函数

  f1 ,...,fn

  （默认为无）。