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
- Subject: [Frama-c-discuss] Unbound value Datatype.func in register.ml
- From: njucslzh0714 at gmail.com (刘自恒)
- Date: Sun, 19 Jun 2011 18:31:34 +0800
- In-reply-to: <BANLkTik56TF8f-EQH5_pb_fgiPnqK3VpLg@mail.gmail.com>
- References: <BANLkTik56TF8f-EQH5_pb_fgiPnqK3VpLg@mail.gmail.com>
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>
- Follow-Ups:
- [Frama-c-discuss] Unbound value Datatype.func in register.ml
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] Unbound value Datatype.func in register.ml
- From: njucslzh0714 at gmail.com (刘自恒)
- [Frama-c-discuss] RE : Unbound value Datatype.func in register.ml
- From: julien.signoles at cea.fr (SIGNOLES Julien)
- [Frama-c-discuss] Unbound value Datatype.func in register.ml
- References:
- [Frama-c-discuss] Unbound value Datatype.func in register.ml
- From: njucslzh0714 at gmail.com (刘自恒)
- [Frama-c-discuss] Unbound value Datatype.func in register.ml
- Prev by Date: [Frama-c-discuss] Mailing-list administrivia
- Next by Date: [Frama-c-discuss] Unbound value Datatype.func in register.ml
- Previous by thread: [Frama-c-discuss] Unbound value Datatype.func in register.ml
- Next by thread: [Frama-c-discuss] Unbound value Datatype.func in register.ml
- Index(es):