gpt4 book ai didi

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

转载 作者:行者123 更新时间:2023-12-04 19:27:50 26 4
gpt4 key购买 nike

我按照 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 .

    最佳答案

    插件开发指南的第 5.2.3 节给出了可用于自定义 Makefile 的变量列表。值得注意的是,如果要链接到外部库,可以使用 PLUGIN_EXTRA_BYTEPLUGIN_EXTRA_OPT ,以及 PLUGIN_LINK_BFLAGSPLUGIN_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/

    26 4 0
    Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
    广告合作:1813099741@qq.com 6ren.com