Как связать файлы .cma с моим собственным плагином Frama_C? - PullRequest
Новая
       39

Как связать файлы .cma с моим собственным плагином Frama_C?

0 голосов
/ 06 июня 2018

Я создал свой собственный плагин Frama-C, следуя инструкциям Руководства по разработке Frama-C (https://frama -c.com / download / frama-c-plugin-development-guide.pdf ).

Однако мне нужно использовать модуль Mutex , предоставленный руководством Ocaml (http://caml.inria.fr/pub/docs/manual-ocaml/libref/Mutex.html) в моих файлах .ml. Чтобы использовать этот модуль, мне нужна определенная командная строка:

ocamlc -thread unix.cma threads.cma myfiles.ml

(как объяснено здесь: Не найден модуль OCaml Mutex ).

Чтобы скомпилировать мойя использую Makefile, который создает плагин ( Руководство по разработке плагинов стр. 33). Поэтому я пытаюсь связать эти файлы .cma и параметр -thread с этим Makefile ...и у меня ничего не получилось. Как мне загрузить этот модуль Mutex?

Что я пробовал:

  1. Я посмотрел в файле, автоматически сгенерированном 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 распознан, и я точно не знаю, хорошее ли это решение ...

Наконец, я протестировал с использованием модуля Olddynlink , предоставленного Frama-C (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 Dynlink loadfile "unix.cma";; loadfile "threads.cma";;

в соответствующем .ml-файле.

Но всегда одна и та же ошибка: Unbound module Mutex.

1 Ответ

0 голосов
/ 06 июня 2018

В разделе 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 кажется немного странным в этом отношении.

...