c - 切片器:读取不确定的值后继续探索路径

我想切分以下程序：

int main() {
  int j;
  if (j) {
ERROR:
    /*@ slice pragma ctrl; */
    goto ERROR;
  }
  return 0;
}

目前，Frama-C在读取j后停止探索路径，导致ERROR标签被切掉：

$ frama-c test.c -slice-pragma main -then-on 'Slicing export' -print
[...]
test.c:3:[kernel] warning: accessing uninitialized left-value: assert \initialized(&j);
test.c:3:[kernel] warning: completely indeterminate value in j.
[...]

有没有办法将readingj视为读取未指定的值？
我更愿意以编程方式（在Frama-C内部）完成这项工作，而不修改分析的源代码。
我在运行Frama-C霓虹灯。

最佳答案

在执行C程序期间读取未初始化（不确定）内存是未定义的行为or might as well be treated as such。C程序的切片器不需要保留导致未定义行为的执行。因此，由于程序的所有执行都会导致未定义的行为，实际上Frama-C的切片插件生成的任何切片都是正确的切片。如果您编写了if (1 / 0) {，则可以获得相同的行为。基于我链接到的博客文章中给出的原因，两者之间没有太大区别。
作为解决方案，只需使用内置的j初始化Frama_C_interval()，其规范在文件__fc_builtin.h中提供：

#include <__fc_builtin.h>
...
int j = Frama_C_interval(0, 1);

如果这对您来说更简单，例如，您可以将j设置为未知值，如下所示：

volatile int u;

int main() {
  int j = u;
  ...

编辑：
在与托马斯私下讨论之后，我补充了以下建议：
您可以编写一个Frama-C插件，将一个C程序转换为一个等价的C程序，在该程序中初始化每个局部变量。我建议对语句执行其他初始化：

Frama_C_make_unknown(&x, sizeof x);

其中，Frama_C_make_unknown是一个函数，您可以在它的初始源代码中创建一个包含规范的原型（因此必须避免添加它的困难：）

extern int Frama_C_entropy_source;

/*@ requires \valid(p + (0 .. l-1));
    assigns p[0 .. l-1] \from Frama_C_entropy_source;
    assigns Frama_C_entropy_source \from Frama_C_entropy_source;
    ensures \initialized(p + (0 .. l-1));
*/
void Frama_C_make_unknown(char *p, size_t l);

经过这样的转换后，切片插件将按您的预期工作。如果您在制作这样一个转换插件时遇到困难，可以在frama-c-discus或StackOverflow中询问有关该插件的问题（后者更好，因为Google没有以任何有用的方式索引frama-c-discus）。

关于c - 切片器:读取不确定的值后继续探索路径，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/23513354/