用 malloc 编程：为什么 Eva 不能证明 \valid(p)？

Question

如何使用 Frama-C 验证此 C 程序？

#include <stdlib.h>

int main(void)
{
  char *p = malloc(2);
  char s[2];
  p[0] = 0;
  s[0] = 0;
  return 0;
}

当我在上面运行 Frama-C 17（氯）时，更具体地说是 Eva 插件，我得到：

$ frama-c -val t.c
[kernel] Parsing t.c (with preprocessing)
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
  __fc_heap_status ∈ [--..--]
  __fc_random_counter ∈ [--..--]
  __fc_rand_max ∈ {32767}
  __fc_mblen_state ∈ [--..--]
  __fc_mbtowc_state ∈ [--..--]
  __fc_wctomb_state ∈ [--..--]
[value] t.c:5: allocating variable __malloc_main_l5
[value:alarm] t.c:7: Warning: out of bounds write. assert \valid(p + 0);
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main:
  __fc_heap_status ∈ [--..--]
  p ∈ {{ &__malloc_main_l5[0] }}
  s[0] ∈ {0}
   [1] ∈ UNINITIALIZED
  __retres ∈ {0}
  __malloc_main_l5[0] ∈ {0}
          [1] ∈ UNINITIALIZED

显然 Eva 插件知道分配的块的大小分配。它正确地推断出对 s[0] 的写入是有效的（例如，如果我尝试写入 s[3]，它会检测到错误）。

但是我怎么能告诉它完成 \valid(p+0) 目标呢？

WP插件也试过了，但是说不支持分配

Answer 1

问题是 默认情况下，在 Eva 中，malloc 可能会失败 。为避免这种情况，请选择以下一项：

使用选项 -no-val-alloc-returns-null，假设 malloc 永远不会失败；
修补代码以添加测试，例如if (!p) exit(1);

详细解释

在 malloc 之后有 2 次可能的执行的事实在命令行中不会立即可见。 GUI 在检查此类情况时有时会有所帮助，但我们也可以在调用 malloc:

之后添加对 Frama_C_show_each(p) 的调用

  char *p = malloc(2);
  Frama_C_show_each_p(p);
  ...

现在，在运行 frama-c -val 之后，我们得到以下行：

[value] mall.c:6: Frama_C_show_each_p: {{ NULL ; &__malloc_main_l5 }}

分析考虑了两种不同的可能性（malloc 失败并返回 NULL；或 malloc 成功并返回一个新碱基）。

报警Warning: out of bounds write. assert \valid(p + 0);是指第一种情况，属性无效。对该分支的分析停止，这使得更难看出发生了什么，因为之后我们只有一个分支，正如我们预期的那样。

用 malloc 编程：为什么 Eva 不能证明 \valid(p)？

Program with malloc: why can't Eva prove \valid(p)?

frama-c

详细解释