小编Gif*_*ifi的帖子

我按照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";; …