ocaml - Frama-C 铝 "Unbound module GMenu"

Question

在 Fedora 21 上，我在安装了所有先决条件后从源代码编译了 Frama-C Aluminium 发行版。我的 OCaml 版本是 4.02.3。 Frama-C 和 Frama-C GUI 工作正常。我正在尝试遵循 Frama-C Plug-In Development Guide 的第 2.3 节“ViewCfg 插件” 。但是，在第 2.3.4 节“扩展 Frama-C GUI”中，在添加 GUI 扩展代码并使用“-load-script”选项运行它后，我收到以下消息:

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

第 86-87 行:

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

我用谷歌搜索“unbound module gmenu”，但没有找到任何有用的东西。我在使用 Frama-C 的 Neon 和 Sodium 版本时也从未遇到过这个错误。有趣的是，如果我跳过该部分并遵循第 2.3.5 节“拆分文件并编写 Makefile”，我将不再收到“Unbound module GMenu”消息，并且该示例工作正常。

如果我不得不猜测，当我使用“-load-script”选项时，Frama-C(或我的 OCaml 版本，无论是什么情况)显然由于某种原因无法找到 Gtk 库。但如果我使用 make，OCaml 可以找到 Gtk 库。我安装 Frama-C 和/或 Gtk 库的方式可能有问题吗？我该如何检查这个问题，或更重要的是，如何解决这个问题？

Answer 1

您的 Frama-C 安装可能没问题。您观察到的是我们过渡到 OCamlfind 时引入的错误。我们将修复 Frama-C 硅的问题。

如果您确实想使用脚本，这里是您需要应用于 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 () ;