Frama-C 中止无效的用户输入

Question

我是 Frama-c 的新手，在尝试打开 C 源文件时遇到了问题。

The error shows as 
"fatal error: event.h: No such file or directory. Compilation terminated".

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)

[kernel] Parsing WorkSpace/bipbuffer.c (with preprocessing)

[kernel] user error: failed to run: gcc -E -C -I.  -dD -D__FRAMAC__  -nostdinc -D__FC_MACHDEP_X86_32 -I/usr/share/frama-c/libc -o '/tmp/bipbuffer.ce6d077.i' '/home/xxx/WorkSpace/bipbuffer.c'    you may set the CPP environment variable to select the proper preprocessor command or use the option "-cpp-command".

[kernel] user error: stopping on file "/home/xxx/WorkSpace/bipbuffer.c" that has errors. Add'-kernel-msg-key pp' for preprocessing command.

所以基本上我试图打开一个 C 源文件，但它返回这样的错误。我还尝试了其他非常简单的 C 文件，如 hello world 和其他切片函数，效果很好。

我以为是因为我没有 'event.h' 的依赖，但在我安装了 libevent 依赖后它仍然返回这些错误。我不确定是否需要为 frama-c 手动设置一些依赖路径

这是我要打开的 C 文件的一部分(来源链接:https://memcached.org/):

#include "stdio.h"
#include <stdlib.h>

/* for memcpy */
#include <string.h>

#include "bipbuffer.h"

static size_t bipbuf_sizeof(const unsigned int size)
{
    return sizeof(bipbuf_t) + size;
}

int bipbuf_unused(const bipbuf_t* me)
{
    if (1 == me->b_inuse)
        /* distance between region B and region A */
        return me->a_start - me->b_end;
    else
        return me->size - me->a_end;
}
......

谢谢，

Answer 1

使用 C 源代码的编译器和其他工具需要知道在哪里可以找到头文件。它们会自动查找一些标准位置，但 Frama-C 的位置比普通编译器少(并且不同)。

你需要找出event.h的安装位置，然后传递类似-cpp-extra-args "-I/path/to/directory/"到 Frama-C。仅传递目录名称，不包括名称 event.h 本身。