c - 切片器 : continue exploring path after reading indeterminate value

Question

我想对以下程序进行切片:

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.
[...]

有没有一种方法可以将读取j 视为读取未指定的值？我更愿意以编程方式(在 Frama-C 中)执行此操作，而无需修改分析的源代码。

我正在运行 Frama-C Neon。

Answer 1

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

---

作为解决方案，只需使用 Frama_C_interval() 内置函数初始化 j，其规范在文件 __fc_builtin.h 中提供:

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

---

如果这对您来说更简单，举一个简短的例子，您可以将 j 设置为一个未知值，如下所示:

volatile int u;

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

编辑:

在与 Thomas 私下讨论后，我添加了以下建议:

您可以编写一个 Frama-C 插件，将 C 程序转换为等效的 C 程序，其中每个局部变量都已初始化。我建议使用语句完成额外的初始化:

Frama_C_make_unknown(&x, sizeof x);

其中 Frama_C_make_unknown 是一个函数，您本可以在初始源代码中设法拥有一个带有规范的原型(prototype)(因此必须避免添加它的困难:)

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-discuss 或 StackOverflow 中提问(后者更好，因为 Google 不会以任何有用的方式对 frama-c-discuss 进行索引)。