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

[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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110619/18bebef5/attachment.htm>