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を使用しています (なぜ fc_runtime.c と他の *.c ファイルが Neon リリースから削除されているのですか?)

指図：

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;
    }