2

我有一些问题要决定如何告诉Frama-C 使用哪些包含文件。我通常添加选项：

-cpp-extra-args="-I $(frama-c -print-path)/libc"

为了获得 Frama-C 的标准规格。但我经常需要一些不在 Frama-C 库中的东西。

例如，我要分析的源文件之一使用了定义在 中的宏<sys/wait.h>，但因为 Frama-C 有自己的frama-c/libc/sys/wait.h，所以不包括 gcc 文件。不幸的是，Frama-C 没有定义宏，并且定义最终丢失了。当然，我不想更改源文件！

my_libc/sys/wait.h我正在考虑使用包含 Frama-C 文件的文件构建一个本地目录，并且我可以在其中复制 GCC 文件中缺少的内容。

然后我会使用：

-cpp-extra-args="-I my_libc -I $(frama-c -print-path)/libc"

但我对我的解决方案有点担心，因为从 GCC 包含文件中提取定义可能非常棘手......

你怎么看？这似乎是个好主意？您对更好的组织有什么建议吗？

4

1 回答 1

2

This solution seems fine (extracting definitions from gcc's headers can indeed be complicated, but you don't have much choice there: you must provide the macro at some point, and you probably don't want to have the whole header ending up in Frama-C).

I'm no pre-processing expert, but I'm not sure that you'll be able to include both my_libc/sys/wait.h and $FRAMAC_SHARE/libc/sys/wait.h with the -cpp-extra-args option you propose: you end up with two sys/wait.h headers and cpp will always pick the first one. I see two solutions:

  • you define your own standard headers (potentially with copy'n paste from Frama-C's libc), and use only them
  • you define your headers, with #include <libc/sys/wait.h>, and have -cpp-extra-args=... -I$(frama-c -print-path), avoiding confusion on the relative path of the headers.

Note that in both cases, you must provide files for all the headers that are used by your application, even if most of them are merely a redirection to or a copy of the corresponding Frama-C file. But I guess that you should be done with a few shell commands.

于 2012-11-12T13:35:56.507 回答