5

I created my own Frama-C plugin by following the instructions of the Frama-C Development Guide (https://frama-c.com/download/frama-c-plugin-development-guide.pdf).

However, I need to use the Mutex module provided by the Ocaml manual (http://caml.inria.fr/pub/docs/manual-ocaml/libref/Mutex.html) in my .ml files. To use this module, I need a particular command line:

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

(as explained here: OCaml Mutex module cannot be found).

To compile my files I use the Makefile that builds the plugin (Plugin Development Guide page 33). So I'm trying to link these .cma files and the -thread option to this Makefile...and I did not succeed. How can I load this Mutex module?

What I tried:

  1. I looked in the file automatically generated by Frama-C: .Makefile.plugin.generated if there was a variable to call and modify in my Makefile (the same kind as the variable PLUGIN_CMO to call my .ml files) but I did not find such a variable.

I tried with some variables that are defined in the generated .Makefile.plugin.generated this way:

I wrote the following lines in my Makefile:

PLUBIN_EXTRA_BYTE = unix.cma threads.cma

or TARGET_TOP_CMA = unix.cma threads.cma

and for the thread option: 

PLUGIN_OFLAGS = -thread

or PLUGIN_LINK_BFLAGS= -thread

or PLUGIN_BFLAGS= -thread

But never was the Mutex module recognized and I don't know exactly if it is a good solution...

  1. Finally, I tested using the Olddynlink module provided by 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) and his value loadfile, but it did not work either:

I wrote:

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

in the .ml file concerned.

But always the same error: Unbound module Mutex.

Gifi
  • 53
  • 4

1 Answers1

4

Section 5.2.3 of the plugin development guide gives the list of variables that can be used to customize the Makefile. Notably, if you want to link against an external library, you can use PLUGIN_EXTRA_BYTE and PLUGIN_EXTRA_OPT, as well as PLUGIN_LINK_BFLAGS and PLUGIN_LINK_OFLAGS to add the -thread option. Here is a Makefile that should work (of course, you need to complete it depending on your actual source files).

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

Note that in theory, you should only have to use the PLUGIN_REQUIRES variable, and let ocamlfind take care of everything but threads seems to be a bit peculiar in this respect.

Virgile
  • 9,724
  • 18
  • 42