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] 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>