如何编译一个有C源代码的Frama-C插件？

Question

我创建了一个使用 .c 源代码的 Frama-C 插件，我想编译它，但是当添加

PLUGIN_EXTRA_OPT = file

对于我的插件的Makefile，我在运行 make之后得到以下错误：

Packing      Myplugin.cmx
file.c:1:24: fatal error: caml/alloc.h: No such file or directory
 #include <caml/alloc.h>
                        ^
compilation terminated.

添加 VERBOSEMAKE=yes 提供了一些关于错误原因的附加信息：

...
gcc     file.c   -o file
file.c:1:24: fatal error: caml/alloc.h: No such file or directory
...

似乎由于某种原因正在调用 GCC，而不是 ocamlc。

如何让 make 正确编译我的 .c 源代码？

Answer 1

在这种情况下，PLUGIN_EXTRA_OPT 变量的正确语法是包含 .o 扩展名：

PLUGIN_EXTRA_OPT = file.o

通过这样做，Make 应用正确的规则并使用 ocamlc 构建 file.o，然后将其作为构建插件的 ocamlopt 命令的附加参数包括在内.cmx 文件。

之前的错误是由于 Make 对不存在的 file 目标应用了隐式规则，如运行 make -d:

所示

...
Considering target file `file'.
 File `file' does not exist.
 Looking for an implicit rule for `file'.
 Trying pattern rule with stem `file'.
 Trying implicit prerequisite `file.c'.
 Found an implicit rule for `file'.
...

如何编译一个有C源代码的Frama-C插件？

How to compile a Frama-C plug-in having a C source?

frama-c