如何让Frama-C的WP不分析不可达/死代码？版本差异求助

问题场景 #

执行命令 frama-c test.c -rte -eva -eva-slevel 1 then -wp 后，不同版本Frama-C的表现存在差异：

• Frama-C 24：无错误提示
• Frama-C 25/26：在未被调用、不可达的test函数中检测到溢出问题

测试代码示例：

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

int main(void)
{
  return 0;
}

问题根源：自Frama-C 25版本起，WP插件会尝试证明RTE插件生成的所有注解，即便这些注解位于不可达或死代码区域，而此前版本会自动忽略这类代码的注解验证。

解决方案 #

方案1：让WP复用EVA的不可达分析结果 #

添加 -wp-use-eva 选项，使WP基于EVA的分析标记，自动跳过不可达代码位置的注解证明。修改后的完整命令为：

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

方案2：RTE阶段直接跳过死代码的注解生成 #

使用 -rte-dead-code skip 选项，让RTE插件不为不可达/死代码生成任何注解，从根源避免WP处理这类不必要的验证任务。命令如下：

frama-c test.c -rte -rte-dead-code skip -eva -eva-slevel 1 then -wp

两种方案均可解决问题，可根据需求选择：方案1保留RTE的注解生成，仅在WP层面过滤；方案2直接减少不必要的注解生成，提升整体分析效率。

内容的提问来源于stack exchange，提问作者baronju