--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on June 2011 ---
Hello, If there is no issue with other plug-ins, then the issue probably comes from your own code ;-). One potential problem I can see is that you mask the kernel module Datatype somewhere. A good trick to check this hypothesis is to add the single line "module D = Datatype" to your broken code and to compile it with the option -i of the bytecode compiler (aka ocamlc). That shows you the inferred signature of your .ml: if your module D does not have the expected signature (should be equivalent to the one manually written in src/type/datatype.mli), then the kernel module Datatype is hidden. That could be done by an "open M" or "include M" statement where M is a module definition containing a module Datatype itself. Hope this helps, Julien Signoles -------- Message d'origine-------- De: frama-c-discuss-bounces at lists.gforge.inria.fr de la part de ??? Date: dim. 19/06/2011 12:31 ?: frama-c-discuss at lists.gforge.inria.fr Objet : Re: [Frama-c-discuss] Unbound value Datatype.func in register.ml Hello, Datatype.func is defined in file src/type/datatype.ml and there is no problem in other plugins. For example, file "register.ml" in plugin "occurrence" contains codes let () = Db.register (Db.Journalize ("Occurrence.get", Datatype.func Varinfo.ty (Datatype.list (Datatype.pair Kinstr.ty Lval.ty)))) Db.Occurrence.get get; Db.register (Db.Journalize ("Occurrence.print_all", Datatype.func Datatype.unit Datatype.unit)) (* pb: print_all should take a formatter as argument *) Db.Occurrence.print_all print_all; Db.Occurrence.self := Occurrences.self My development environment is: OS--Ubuntu 11.04 OCaml--3.11.2 Frama-C--frama-c-Carbon-20110201 The files are: function_analysis.ml do my analysis loop_parameters.ml some paras LoopInvariant.ml defines some features and val LoopInvariant.mli empty register.ml register plugin and methods and also, added codes below in src/kernel/db.ml module LoopInvariant = struct let run = mk_fun "LoopInvariant.run" let theMain = mk_fun "LoopInvariant.theMain" end in src/kernel/db.mli (** loop invariant plugin. By liu*) module LoopInvariant : sig val run:(Format.formatter -> unit) ref val theMain:(unit -> unit) ref end I changeed file config.in and added a section: # Loop Invariant check_plugin(loopInvariant,src/loop_invariant,[support for loopInv plugin],yes,no) then executed command: autoconf ./configure now I got file "Makefile" and I added such section: # Loop Invariant PLUGIN_ENABLE:=$(ENABLE_LoopInvariant) PLUGIN_NAME:=LoopInvariant PLUGIN_DIR:=src/loop_invariant PLUGIN_CMO:= loop_parameters function_analysis register LoopInvariant PLUGIN_NO_TEST:=yes PLUGIN_HAS_MLI:=yes include share/Makefile.plugin then executed command: sudo make and it emitted the error: Unbound value Datatype.func in register.ml if I committed the following codes in "register.ml", it just workd.So can you help me? Best regards to you.