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

我按照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.genic，如果我的Makefile中有要调用和修改的变量(与变量PLUGIN_CMO相同，可以调用我的.ml文件)，但是我没有找到这样的变量。

我尝试使用以下方式在生成的.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)和他的值loadfile进行了测试，但是它都不起作用:

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

但是总是相同的错误:Unbound module Mutex。

最佳答案

插件开发指南的第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在这方面似乎有点特殊。

关于makefile - 如何将.cma文件链接到我自己的Frama_C插件？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/50723474/