1

我想切片以下程序：

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。

4

1 回答 1

1

在 C 程序执行期间读取未初始化（不确定）的内存是未定义的行为，或者也可以这样对待。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;
  ...

编辑：

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

您可以编写一个 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-discuss 或 StackOverflow 中提出问题（后者更好，因为 Google 不会以任何有用的方式索引 frama-c-discuss）。

于 2014-05-07T10:27:15.350 回答