--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on June 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] RE : Unbound value Datatype.func in register.ml



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.