Frama-C 铝 "Unbound module GMenu"

Question

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

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 节 "Splitting files and writing a Makefile" 进行操作，我将不再收到 "Unbound module GMenu" 消息，并且该示例工作正常。

如果我不得不猜测，当我使用“-load-script”选项时，Frama-C（或我的 OCaml 版本，无论如何）显然出于某种原因找不到 Gtk 库。但是如果我使用 make，OCaml 可以找到 Gtk 库。我安装 Frama-C and/or 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 () ;

Frama-C 铝 "Unbound module GMenu"

Frama-C Aluminum "Unbound module GMenu"

ocaml

frama-c