Frama-C 铝“未绑定模块 GMenu”

Question

在 Fedora 21 上，我在安装了所有先决条件后从源代码编译了 Frama-C Aluminum 发行版。我的 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 =

我搜索了“未绑定模块 gmenu”，但没有发现任何有用的信息。在使用 Frama-C 的 Neon 和 Sodium 版本时，我也从未遇到过这个错误。有趣的是，如果我跳过该部分并遵循第 2.3.5 节“拆分文件和编写 Makefile”，我将不再收到“未绑定模块 GMenu”消息，并且该示例可以正常工作。

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

Answer 1

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

如果你真的想使用脚本，这里是你需要应用到 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 () ;