frama-c - frama-c malloc Neon-20140301 致命错误

Question

是否可以使用 Frama-c 检测内存泄漏或双重释放？我试图测试那个例子但是

#include <string.h>
#include <stdlib.h>

#define FRAMA_C_MALLOC_STACK
#include "/usr/share/frama-c/libc/fc_runtime.c"

int main()
{
  int *x  = malloc(sizeof(int));
  free(x);
  free(x);
  return 0;
}

我得到：

现在我正在使用版本：Neon-20140301 和从 Fluorine-20130601 复制的libc（顺便说一下，为什么从 Neon 版本中删除了 fc_runtime.c 和其他 *.c 文件？）

命令：

frama-c-gui -cpp-command "gcc -C -E -I/usrhare/frama-c/libc/ -nostdinc" -slevel 1000 -val  -val-warn-copy-indeterminate @all main.

使用其他定义 (FRAMA_C_MALLOC_XXXX) 有效，但未检测到任何错误。

更新：其他示例

#include <string.h>
    #include <stdlib.h>

    #define FRAMA_C_MALLOC_STACK
    #include "/usr/share/frama-c/libc/fc_runtime.c"

    int main()
    {
      int *x  = malloc(sizeof(int));
      x[2] = 5;
      return 0;
    }