makefile - 如何将 .cma 文件链接到我自己的 Frama_C 插件？

Question

我按照 Frama-C 开发指南 (https://frama-c.com/download/frama-c-plugin-development-guide.pdf) 的说明创建了自己的 Frama-C 插件。

但是，我需要在我的 .ml 文件中使用 Ocaml 手册 (http://caml.inria.fr/pub/docs/manual-ocaml/libref/Mutex.html) 提供的 Mutex 模块。要使用这个模块，我需要一个特定的命令行:

ocamlc -thread unix.cma threads.cma myfiles.ml

(如此处所述:OCaml Mutex module cannot be found)。

为了编译我的文件，我使用了构建插件的 Makefile(插件开发指南第 33 页)。所以我试图将这些 .cma 文件和 -thread 选项链接到这个 Makefile ......但我没有成功。 如何加载这个 Mutex 模块？

我试过的:

我查看了 Frama-C 自动生成的文件:.Makefile.plugin.generated 如果我的 Makefile 中有一个要调用和修改的变量(与调用我的 .ml 文件的变量 PLUGIN_CMO 相同)但我没有找到这样的变量。

我尝试了以这种方式在生成的 .Makefile.plugin.generated 中定义的一些变量:

我在 Makefile 中写了以下几行:
PLUBIN_EXTRA_BYTE = unix.cma threads.cma
或 TARGET_TOP_CMA = unix.cma threads.cma
对于线程选项:

PLUGIN_OFLAGS = -thread

或 PLUGIN_LINK_BFLAGS= -thread
或 PLUGIN_BFLAGS= -thread
但是 Mutex 模块从未被认可，我不知道它是否是一个好的解决方案......

最后，我使用 Frama-C 提供的 Olddynlink 模块( http://arvidj.eu/frama/frama-c-Aluminium-20160501_api/frama-c-api/html/FCDynlink.OldDynlink.html#VALloadfile )和值 loadfile 或使用 Dynlink 模块( http://caml.inria.fr/pub/docs/manual-ocaml/libref/Dynlink.html#VALloadfile )和他的值加载文件进行了测试，但它也不起作用:

我写:
open Dynlink loadfile "unix.cma";; loadfile "threads.cma";;
在有关的 .ml 文件中。

但总是同样的错误:Unbound module Mutex .

Answer 1

插件开发指南的第 5.2.3 节给出了可用于自定义 Makefile 的变量列表。值得注意的是，如果要链接到外部库，可以使用 PLUGIN_EXTRA_BYTE和 PLUGIN_EXTRA_OPT ，以及 PLUGIN_LINK_BFLAGS和 PLUGIN_LINK_OFLAGS添加 -thread选项。这是 Makefile这应该可以工作(当然，您需要根据您的实际源文件来完成它)。

ifndef FRAMAC_SHARE
FRAMAC_SHARE:=$(shell frama-c-config -print-share-path)
endif

PLUGIN_NAME:=Test_mutex
PLUGIN_BFLAGS:=-thread
PLUGIN_OFLAGS:=-thread
PLUGIN_EXTRA_BYTE:=$(shell ocamlfind query threads)/threads/threads.cma
PLUGIN_EXTRA_OPT:=$(shell ocamlfind query threads)/threads/threads.cmxa
PLUGIN_LINK_BFLAGS:=-thread
PLUGIN_LINK_OFLAGS:=-thread
PLUGIN_CMO:= # list of modules of the plugin
include $(FRAMAC_SHARE)/Makefile.dynamic

请注意，理论上，您应该只需要使用 PLUGIN_REQUIRES变量，并让 ocamlfind照顾好一切，除了 threads在这方面似乎有点奇怪。