使用某些基准运行 Frama-C 值分析时，例如susan 在 http://www.eecs.umich.edu/mibench/automotive.tar.gz 中，我们注意到很多 block 被认为是死代码或无法访问。然而，实际上，这些代码是在我们从这些 block 中打印出一些调试信息时执行的。有没有人注意到这个问题？我们如何解决这个问题？
最佳答案
您的代码有一个不在 Pascal 列表中的特性，它解释了死代码的某些部分。相当多的函数是这样声明的
f(int x, int y);
返回类型完全缺失。 C 标准指示此类函数应返回 int，而 Frama-C 遵循此约定。当解析这些函数时，它表明它们从不在它们的某些路径上返回任何东西
Body of function f falls-through. Adding a return statement.
在返回语句之上，Frama-C 还添加了一个 /*@assert\false; 注释，以指示不返回任何内容的函数的执行路径应该是死代码。在您的代码中，此注释始终为假:这些函数应该返回 void，而不是 int。您应该使用正确的返回类型更正您的代码。
关于frama-c - 为什么在 Frama-C 值分析中无法访问代码？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/20171197/