Frama-C 中止无效的用户输入
Frama-C aborted Invalid user input
我是 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 源文件，但是 return 出现了这样的错误。我还尝试了其他非常简单的 C 文件，如 hello world 和其他切片函数，效果很好。
我以为是因为我没有'event.h'的依赖，但是我安装了libevent依赖后还是return这些错误。我不确定是否需要为 frama-c
手动设置一些依赖项路径
这是我要打开的 C 文件的一部分（来源 link：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;
}
......
谢谢，
使用 C 源代码的编译器和其他工具需要知道在哪里可以找到头文件。有一些标准的地方，它们会自动查找，但 Frama-C 比普通编译器少（并且不同）。
您需要找出 event.h 的安装位置，然后将 -cpp-extra-args "-I /path/to/directory/" 之类的内容传递给 Frama-C。仅传递目录名称，不包括名称 event.h 本身。
除了 Isabelle Newbie 的回答之外，我想指出 Frama-C 的 Chlorine 版本，其测试版已 recently announced, features a new option -json-compilation-database that attempts to read the arguments to be passed to the pre-processor from a compilation database。
这样的数据库可以直接由cmake生成，但是有基于make的项目的解决方案，比如你提到的那个，特别是bear，它拦截了make 启动的用于构建数据库的命令。
这里有一个关于如何继续的详细总结，使用 Frama-C 17 Chlorine 的新 -json-compilation-database 选项，加上一个额外的脚本 list_files.py（不在测试版中，但将在最终 17 版本中提供，并且可以下载 here):
使用Frama-C、运行./configure获取要分析的源文件，如果可能的话尽量禁用来自外部库的可选依赖；例如，一些代码库包括基于 libraries/system 功能可用性的可选依赖项，但具有后备选项（求助于标准 C 库或 POSIX 函数）。您提供的 Frama-C 越多，分析它的机会就越大，因此如果这些外部库不是必需的，排除它们可能有助于获得更多的 "POSIXy" 代码，这应该会有所帮助。这通常在 config.h 文件中可见，在通常名为 HAVE_*.
编译并安装 Build EAR 或一些等效工具以获得 compile_commands.json 文件。
运行 bear make（或带有标记 CMAKE_EXPORT_COMPILE_COMMANDS 的 cmake）以获取 compile_commands.json 文件。
运行前面提到的list_files.py在包含compile_commands.json的目录中获取编译时使用的C源列表
运行 Frama-C（17 氯或更新），给它在上一步中找到的来源列表，加上选项 -json-compilation-database . 来解析 compile_commands.json 并希望获得适当的预处理标志。
理想情况下，这应该足够了，但在实践中，这很少足够。特别是由于存在外部库和非 C99，non-POSIX 函数，始终需要以下步骤。
6.包含外部库
到这一步，Frama-C会抱怨缺少event.h。您必须自己包含此库的 headers。 注意：直接从您的 /usr/include 复制 headers 不 可能有效，因为有多个 architecture-specific 定义，尤其是诸如此类的文件如 bits/*.h.。
相反，请考虑下载外部库并准备它们（例如至少 运行ning ./configure）。然后通过 -cpp-extra-args="-I <path/to/your/sources/for/libevent.h>/include".
手动添加额外的包含目录
7.包含缺失 non-POSIX headers
其他一些 headers 可能会丢失，特别是 GNU- 或 BSD-specific 来源（例如 sysexits.h）。获取这些 headers 并在必要时添加它们。本例中的错误消息来自预处理器 (gcc)，类似于：
memcached.c:51:10: fatal error: sysexits.h: No such file or directory
#include <sysexits.h>
^~~~~~~~~~~~
compilation terminated.
8。缺少 non-POSIX 类型和常量的定义
此时，所有必需的 headers 应该都可用，但使用 Frama-C 解析可能仍然会失败。这是由于使用了 non-POSIX 类型定义（例如 caddr_t、struct ling）、non-POSIX 常量（例如 MAXPATHLEN、SOCK_NONBLOCK、NI_MAXSERV).错误消息通常类似于以下内容：
[kernel] memcached.c:3261: Failure: Cannot resolve variable MAXPATHLEN
常量通常很容易手动提供，方法是搜索 /usr/include 中可用的内容。
另一方面，类型定义可能需要在正确的地方使用一些 copy-pasting，尤其是当它们依赖于其他也缺失的类型时。此步骤很难自动化，但一旦您习惯了一些特定的错误消息，就会相对简单。
例如，以下错误消息与缺少类型定义 (caddr_t) 有关：
[kernel] Parsing memcached.c (with preprocessing)
[kernel] memcached.c:1074:
syntax error:
Location: line 1074, between columns 38 and 47, before or at token: c
1072 *hdr++ = 0;
1073 *hdr++ = 0;
1074 assert((void *) hdr == (caddr_t)c->msglist[i].msg_iov[0].iov_base + UDP_HEADER_SIZE);
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
1075 }
1076
请注意 c 之前的标记是 (caddr_t)，它从未被定义（它通常被定义为 void * 或 char *）。
以下错误消息与 不完整 类型有关，即 struct 在某处使用但从未定义：
[kernel] memcached.c:5811: User Error:
variable `ling' has initializer but incomplete type
表示变量ling的类型struct linger（non-POSIX）从未定义过。在这种情况下，我们可以从 /usr/include/bits/socket.h:
复制它
struct linger
{
int l_onoff; /* Nonzero to linger on close. */
int l_linger; /* Time to linger. */
};
注意：如果 Frama-C 的 libc 中缺少 POSIX constants/definitions，请考虑通知其开发人员，或在 [=156= 中提出拉取请求]的Github.
9.修复不兼容和缺失的函数原型
在上一步之后解析很可能会成功，但它可能仍然由于不兼容的函数原型而失败。例如，您可能会得到：
[kernel] User Error: Incompatible declaration for usleep:
different integer types int and unsigned int
First declaration was at assoc.c:238
Current declaration is at items.c:1573
这是之前发出的警告的结果：
[kernel:typing:implicit-function-declaration] slabs.c:1150: Warning:
Calling undeclared function usleep. Old style K&R code?
表示函数usleep被调用，但它没有原型，因此Frama-C使用"implicit int"的pre-C99约定：它生成这样一个原型，但在代码的后面，发现了 usleep 的实际声明，它的类型是 not int。因此错误。
为防止出现这种情况，您需要确保正确包含 usleep 的原型。由于它是 而不是 POSIX.1-2008，您需要 define/undefine 适当的宏（参见 unistd.h），或者添加您自己的原型.
最后，这应该允许 Frama-C 解析文件并构建 AST。
但是，还缺少几个原型；我们很幸运none 与实际声明冲突。理想情况下，当没有更多消息（例如 implicit-function-declaration 和类似警告。
时，您会认为解析阶段已完成。
memcached 中缺少的一些原型，例如 getsubopt，是 POSIX，应该集成到 Frama-C 的标准库中。其他人可能会制作 non-standard 存根的小型库的一部分，以供其他软件重复使用。
贡献成果以供将来重用
此类开源库的解析阶段的成功结束足以考虑将它们集成到 this repository of open source case studies 中，这样未来的用户就可以开始他们的分析，而无需重做所有这些步骤。 （存储库面向 Eva，但不完全是：解析对所有 Frama-C plug-ins。）
我是 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 源文件，但是 return 出现了这样的错误。我还尝试了其他非常简单的 C 文件，如 hello world 和其他切片函数，效果很好。
我以为是因为我没有'event.h'的依赖，但是我安装了libevent依赖后还是return这些错误。我不确定是否需要为 frama-c
手动设置一些依赖项路径这是我要打开的 C 文件的一部分（来源 link：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;
}
......
谢谢，
使用 C 源代码的编译器和其他工具需要知道在哪里可以找到头文件。有一些标准的地方，它们会自动查找，但 Frama-C 比普通编译器少（并且不同）。
您需要找出 event.h 的安装位置，然后将 -cpp-extra-args "-I /path/to/directory/" 之类的内容传递给 Frama-C。仅传递目录名称，不包括名称 event.h 本身。
除了 Isabelle Newbie 的回答之外，我想指出 Frama-C 的 Chlorine 版本，其测试版已 recently announced, features a new option -json-compilation-database that attempts to read the arguments to be passed to the pre-processor from a compilation database。
这样的数据库可以直接由cmake生成，但是有基于make的项目的解决方案，比如你提到的那个，特别是bear，它拦截了make 启动的用于构建数据库的命令。
这里有一个关于如何继续的详细总结，使用 Frama-C 17 Chlorine 的新 -json-compilation-database 选项，加上一个额外的脚本 list_files.py（不在测试版中，但将在最终 17 版本中提供，并且可以下载 here):
使用Frama-C、运行
./configure获取要分析的源文件，如果可能的话尽量禁用来自外部库的可选依赖；例如，一些代码库包括基于 libraries/system 功能可用性的可选依赖项，但具有后备选项（求助于标准 C 库或 POSIX 函数）。您提供的 Frama-C 越多，分析它的机会就越大，因此如果这些外部库不是必需的，排除它们可能有助于获得更多的 "POSIXy" 代码，这应该会有所帮助。这通常在config.h文件中可见，在通常名为HAVE_*. 的宏中
编译并安装 Build EAR 或一些等效工具以获得
compile_commands.json文件。运行
bear make（或带有标记CMAKE_EXPORT_COMPILE_COMMANDS的 cmake）以获取compile_commands.json文件。运行前面提到的
list_files.py在包含compile_commands.json的目录中获取编译时使用的C源列表运行 Frama-C（17 氯或更新），给它在上一步中找到的来源列表，加上选项
-json-compilation-database .来解析compile_commands.json并希望获得适当的预处理标志。
理想情况下，这应该足够了，但在实践中，这很少足够。特别是由于存在外部库和非 C99，non-POSIX 函数，始终需要以下步骤。
6.包含外部库
到这一步，Frama-C会抱怨缺少event.h。您必须自己包含此库的 headers。 注意：直接从您的 /usr/include 复制 headers 不 可能有效，因为有多个 architecture-specific 定义，尤其是诸如此类的文件如 bits/*.h.。
相反，请考虑下载外部库并准备它们（例如至少 运行ning ./configure）。然后通过 -cpp-extra-args="-I <path/to/your/sources/for/libevent.h>/include".
7.包含缺失 non-POSIX headers
其他一些 headers 可能会丢失，特别是 GNU- 或 BSD-specific 来源（例如 sysexits.h）。获取这些 headers 并在必要时添加它们。本例中的错误消息来自预处理器 (gcc)，类似于：
memcached.c:51:10: fatal error: sysexits.h: No such file or directory
#include <sysexits.h>
^~~~~~~~~~~~
compilation terminated.
8。缺少 non-POSIX 类型和常量的定义
此时，所有必需的 headers 应该都可用，但使用 Frama-C 解析可能仍然会失败。这是由于使用了 non-POSIX 类型定义（例如 caddr_t、struct ling）、non-POSIX 常量（例如 MAXPATHLEN、SOCK_NONBLOCK、NI_MAXSERV).错误消息通常类似于以下内容：
[kernel] memcached.c:3261: Failure: Cannot resolve variable MAXPATHLEN
常量通常很容易手动提供，方法是搜索 /usr/include 中可用的内容。
另一方面，类型定义可能需要在正确的地方使用一些 copy-pasting，尤其是当它们依赖于其他也缺失的类型时。此步骤很难自动化，但一旦您习惯了一些特定的错误消息，就会相对简单。
例如，以下错误消息与缺少类型定义 (caddr_t) 有关：
[kernel] Parsing memcached.c (with preprocessing)
[kernel] memcached.c:1074:
syntax error:
Location: line 1074, between columns 38 and 47, before or at token: c
1072 *hdr++ = 0;
1073 *hdr++ = 0;
1074 assert((void *) hdr == (caddr_t)c->msglist[i].msg_iov[0].iov_base + UDP_HEADER_SIZE);
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
1075 }
1076
请注意 c 之前的标记是 (caddr_t)，它从未被定义（它通常被定义为 void * 或 char *）。
以下错误消息与 不完整 类型有关，即 struct 在某处使用但从未定义：
[kernel] memcached.c:5811: User Error:
variable `ling' has initializer but incomplete type
表示变量ling的类型struct linger（non-POSIX）从未定义过。在这种情况下，我们可以从 /usr/include/bits/socket.h:
struct linger
{
int l_onoff; /* Nonzero to linger on close. */
int l_linger; /* Time to linger. */
};
注意：如果 Frama-C 的 libc 中缺少 POSIX constants/definitions，请考虑通知其开发人员，或在 [=156= 中提出拉取请求]的Github.
9.修复不兼容和缺失的函数原型
在上一步之后解析很可能会成功，但它可能仍然由于不兼容的函数原型而失败。例如，您可能会得到：
[kernel] User Error: Incompatible declaration for usleep:
different integer types int and unsigned int
First declaration was at assoc.c:238
Current declaration is at items.c:1573
这是之前发出的警告的结果：
[kernel:typing:implicit-function-declaration] slabs.c:1150: Warning:
Calling undeclared function usleep. Old style K&R code?
表示函数usleep被调用，但它没有原型，因此Frama-C使用"implicit int"的pre-C99约定：它生成这样一个原型，但在代码的后面，发现了 usleep 的实际声明，它的类型是 not int。因此错误。
为防止出现这种情况，您需要确保正确包含 usleep 的原型。由于它是 而不是 POSIX.1-2008，您需要 define/undefine 适当的宏（参见 unistd.h），或者添加您自己的原型.
最后，这应该允许 Frama-C 解析文件并构建 AST。
但是，还缺少几个原型；我们很幸运none 与实际声明冲突。理想情况下，当没有更多消息（例如 implicit-function-declaration 和类似警告。
memcached 中缺少的一些原型，例如 getsubopt，是 POSIX，应该集成到 Frama-C 的标准库中。其他人可能会制作 non-standard 存根的小型库的一部分，以供其他软件重复使用。
贡献成果以供将来重用
此类开源库的解析阶段的成功结束足以考虑将它们集成到 this repository of open source case studies 中，这样未来的用户就可以开始他们的分析，而无需重做所有这些步骤。 （存储库面向 Eva，但不完全是：解析对所有 Frama-C plug-ins。）