Frama-C Aluminum "Unbound module GMenu"

Question

On Fedora 21, I compiled the Frama-C Aluminum distribution from source after installing all its prerequisites. My version of OCaml is 4.02.3. Frama-C and the Frama-C GUI work fine. I am trying to follow section 2.3, "The ViewCfg plug-in" of the Frama-C Plug-In Development Guide. However, in section 2.3.4, "Extending the Frama-C GUI", after I add the GUI extension code and run it using the "-load-script" option, I get the following message:

File "cfg_print.ml", line 87, characters 19-43:
Error: Unbound module GMenu
[kernel] user error: compilation of 'cfg_print.ml' failed

Lines 86-87 read:

let cfg_selector
    (popup_factory:GMenu.menu GMenu.factory) main_ui ~button:_ localizable =

I googled "unbound module gmenu" but didn't find anything useful. I also never ran into this error while using the Neon and Sodium versions of Frama-C. Interestingly, if I skip that section and follow section 2.3.5, "Splitting files and writing a Makefile", I no longer get the "Unbound module GMenu" message, and the example works fine.

If I had to guess, when I use the "-load-script" option, Frama-C (or my version of OCaml, whatever the case may be) apparently cannot find the Gtk libraries for some reason. But if I use make, OCaml can find the Gtk libraries. Is there something possibly wrong with the way I installed Frama-C and/or the Gtk libraries? How can I check this, or more importantly, how can I fix this?

byako byako · Accepted Answer · 2016-07-31T17:31:52

Your Frama-C installation is probably ok. What you observe is a bug that was introduced when we transitioned to OCamlfind. We will fix it for Frama-C Silicium.

In case you really want to use a script, here is the patch that you need to apply to the sources of Frama-C:

--- a/src/kernel_services/plugin_entry_points/dynamic.ml
+++ b/src/kernel_services/plugin_entry_points/dynamic.ml
@@ -236,7 +236,7 @@ let load_script base =
     else
       Format.fprintf fmt "%s -c" Config.ocamlc ;
     Format.fprintf fmt " -w Ly -warn-error A -I %s" Config.libdir ;
-    if !Config.is_gui then Format.pp_print_string fmt " -I +lablgtk" ;
+    if !Config.is_gui then Format.pp_print_string fmt " -package lablgtk2" ;
     List.iter (fun p -> Format.fprintf fmt " -I %s" p) !load_path ;
     Format.fprintf fmt " %s.ml" base ;
     Format.pp_print_flush fmt () ;

Frama-C Aluminum "Unbound module GMenu"

1 Answers