Frama-C 中的备用代码分析

Question

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

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

Answer 1

诚然，Frama-C 网站上的sparecode page 有点简洁。然而，这部分是由于在这个插件中没有太多参数化的事实。主要是slicing plug-in的一种特殊形式，其准则是“在程序结束时保持状态”。

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

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

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

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

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

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