Frama-C 中的 Sparecode 分析

Question

抱歉，如果这在某个地方有详细说明，我尝试在 Frama-C 的不同文档中搜索但没有成功。

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

Answer 1

诚然，sparecode page on Frama-C's website is a bit terse. However, this is partly due to the fact that there's not much to parameterize in this plug-in. Mainly, it is a specialized form of the slicing plug-in，其中标准是 "preserve the state at the end of the program"。

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

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

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

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

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

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

Frama-C 中的 Sparecode 分析

Sparecode analysis in Frama-C

frama-c