frama-c - 为什么 Frama-C 价值分析中的代码无法访问？

Question

当使用一些基准运行 Frama-C 值分析时，例如susan在 中http://www.eecs.umich.edu/mibench/automotive.tar.gz，我们注意到很多块被认为是死代码或无法访问。然而，在实践中，这些代码是在我们从这些块中打印出一些调试信息时执行的。有没有人注意到这个问题？我们如何解决这个问题？

Answer 1

您的代码有一个不在 Pascal 列表中的特性，它解释了死代码的某些部分。相当多的函数是这样声明的

 f(int x, int y);

返回类型完全丢失。C 标准表明这样的函数应该返回int，并且 Frama-C 遵循这个约定。解析这些函数时，它表明它们在某些路径上永远不会返回任何内容

Body of function f falls-through. Adding a return statement.

在 return 语句的顶部，Frama-C 还添加了一个/*@ assert \false;注解，指示不返回任何内容的函数的执行路径应该是死代码。在您的代码中，此注释始终为 false：这些函数应该返回void，而不是int。您应该使用良好的返回类型更正您的代码。

Answer 2

Frama-C的价值分析结果中出现死码归结为两个方面，甚至这两个方面也只是人的意图问题，从分析者的角度来看是无法区分的。

1. 每次达到特定语句时都会确定地发生真正的错误。例如，后面的代码y = 0; x = 100 / y;无法访问，因为程序每次都停在除法处。一些应该是运行时错误的错误并不总是停止执行，例如，写入无效地址。认为自己很幸运，他们在 Frama-C 的价值分析中做到了，而不是相反。
2. 缺乏分析上下文的配置，包括没有提供信息丰富的 main() 函数，该函数使用内置函数设置程序输入的变化范围Frama_C_interval()，缺少既没有提供规范也没有提供替换代码的库函数，汇编代码在 C 程序中，缺少-absolute-valid-range一个合适的选项，...