Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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.