如何 link .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 页）。所以我试图 link 这些 .cma 文件和这个 Makefile 的 -thread 选项...但我没有成功。 如何加载这个 Mutex 模块？

我试过的：

我查看了Frama-C自动生成的文件：.Makefile.plugin.generated我的Makefile中是否有调用和修改的变量（与变量 PLUGIN_CMO 来调用我的 .ml 文件）但我没有找到这样的变量。

我尝试使用在生成的 中定义的一些变量，Makefile.plugin.generated 这样：

我在 Makefile 中写了以下几行：

PLUBIN_EXTRA_BYTE = unix.cma threads.cma

或TARGET_TOP_CMA = unix.cma threads.cma

并且对于 thread 选项：

PLUGIN_OFLAGS = -thread

或PLUGIN_LINK_BFLAGS= -thread

或PLUGIN_BFLAGS= -thread

但是 Mutex 模块从来没有被识别过，我不知道它是否是一个好的解决方案...

最后，我使用Frama-C (http://arvidj.eu/frama/frama-c-Aluminium-20160501_api/frama-c-api/html/FCDynlink.OldDynlink.html#VALloadfile) with the value loadfile or using the Dynlink module (http://caml.inria.fr/pub/docs/manual-ocaml/libref/Dynlink.html#VALloadfile)提供的Olddynlink模块和他的值loadfile[进行了测试=81=]，但也没有用：

我写了：

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

在相关的 .ml 文件中。

但总是出现同样的错误：Unbound module Mutex。

Answer 1

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

如何 link .cma 文件到我自己的 Frama_C 插件？

How to link .cma files to my own Frama_C plugin?

ocaml

makefile

frama-c