frama-c malloc Neon-20140301 fatal error

问题:

Is it possible to detect memory leaks or double free with Frama-c? I have tried to test that example But

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

I get :

Now I am using Version: Neon-20140301 and libc copied from Fluorine-20130601 ( btw why fc_runtime.c and other *.c files are deleted from Neon release ? )

command:

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

Using other defines (FRAMA_C_MALLOC_XXXX) works but is not detecting any bugs.

update: Other example

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