如何将.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模块).

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

---

我尝试了什么:

---

1. 我查看了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模块从来没有得到认可,我也不确切知道它是否是一个很好的解决方案......

---

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

我写:

open Dynlink loadfile "unix.cma";; loadfile "threads.cma";;

在.ml文件中.

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

Answer 1

插件开发指南的 5.2.3 节给出了可用于自定义 Makefile 的变量列表。值得注意的是，如果您想链接外部库，您可以使用PLUGIN_EXTRA_BYTEandPLUGIN_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在这方面似乎有点特殊。