Frama-C Aluminium "Unbound Modul GMenu"

Question

Auf Fedora 21 habe ich die Frama-C Aluminium Distribution von der Quelle kompiliert, nachdem ich alle Voraussetzungen installiert hatte. Meine Version von OCaml ist 4.02.3. Frama-C und die Frama-C GUI funktionieren gut. Ich versuche, Abschnitt 2.3, "Das ViewCfg-Plug-In" von Frama-C Plug-In Development Guide zu folgen. in Abschnitt 2.3.4, "Erweitern des Frama-C GUI" Allerdings, nachdem ich die GUI-Erweiterung Code und führen Sie es mit dem "-load-Skript" Option hinzufügen, erhalte ich die folgende Meldung:

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

Zeilen 86-87 lesen:

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

Ich googelte "ungebundenes Modul gmenu", aber nichts nützliches gefunden. Diesen Fehler habe ich auch nie bei der Verwendung der Neon- und Natriumversionen von Frama-C kennengelernt. Interessanterweise, wenn ich diesen Abschnitt überspringe und Abschnitt 2.3.5, "Dateien teilen und ein Makefile schreiben" befolge, bekomme ich nicht mehr die Nachricht "Unbound Modul GMenu", und das Beispiel funktioniert gut.

Wenn ich raten musste, wenn ich die Option "-load-script" verwende, kann Frama-C (oder meine Version von OCaml, was auch immer der Fall sein mag) die Gtk-Bibliotheken aus irgendeinem Grund nicht finden. Aber wenn ich make verwende, kann OCaml die Gtk-Bibliotheken finden. Gibt es möglicherweise etwas falsch mit der Art, wie ich Frama-C und/oder die Gtk-Bibliotheken installiert habe? Wie kann ich das überprüfen, oder noch wichtiger, wie kann ich das beheben?

Answer 1

Ihre Frama-C-Installation ist wahrscheinlich in Ordnung. Was Sie beobachten, ist ein Fehler, der bei der Umstellung auf OCamlfind eingeführt wurde. Wir werden es für Frama-C Silicium reparieren.

Im Fall, dass Sie wirklich ein Skript verwenden, hier ist der Patch, den Sie zu den Quellen des Frama-C anwenden muß: unbekannte Option ':

--- 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() ;