frama-c - Frama-C 中的备用代码分析

Question

抱歉，如果这在某处有详细说明，我尝试在 Frama-C 的不同文档中搜索，但没有运气。

我正在尝试在我的代码中消除死代码，但我不了解该工具的结果。是否有任何文件/文档可以解释此插件的工作原理？我只知道它使用了价值分析的结果。

标签： frama-c

Answer 1

诚然， Frama-C 网站上的备用代码页面有点简洁。然而，这部分是由于在这个插件中没有太多参数化的事实。主要是切片插件的一种特殊形式，其标准是“保留程序结束时的状态”。

更一般地，切片包括删除对用户给定标准没有贡献的指令（例如，给定点的整个程序状态、ACSL 注释的有效性状态，或者只是程序到达特定指令的事实）。

为了计算这样的切片，切片，因此备用代码，确实依赖于 Eva 的结果，主要是为了获得程序中每个点所涉及的各种内存位置之间的依赖关系的过度近似（与 Eva 一样）（你可能想看看处理依赖关系的Eva 手册的第 7 章。非常粗略地说，切片将包含在标准中涉及的内存位置的依赖关系的传递闭包（在存在指针和分支的情况下，这个概念“传递闭包”的正式定义变得有点复杂，但本质就在那里）。

现在，关于死代码，有两点值得注意：

• 如前所述，Eva 提供了程序行为的过度近似。对于切片，这意味着某些语句可能会被保留，即使它们在任何具体轨迹中对切片标准没有贡献，但由于过度近似而在抽象轨迹中似乎这样做。另一方面，如果一个陈述不包括在内，那么它肯定对标准没有贡献。
• 对于备用代码，不参与程序的最终状态并不意味着代码已经死了，而只是它的所有副作用都被进一步的指令所掩盖。最简单的例子如下：

int x;
int main() {
  x = 1;
  x = 2; 
}

在这里，x=1对程序的最终状态没有影响，只会x=2被保留。