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


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 de la part de ???
Date: dim. 19/06/2011 12:31
?: frama-c-discuss at
Objet : Re: [Frama-c-discuss] Unbound value Datatype.func in
Datatype.func is defined in file src/type/ and there is no problem in other plugins. For example, file "" in plugin "occurrence" contains codes 

let () =
      Varinfo.ty (Datatype.list (Datatype.pair Kinstr.ty Lval.ty))))
       ("Occurrence.print_all", Datatype.func Datatype.unit Datatype.unit))
    (* pb: print_all should take a formatter as argument *)
  Db.Occurrence.self := Occurrences.self

My development environment is:
OS--Ubuntu 11.04
The files are:          do my analysis           some paras                 defines some features and val
         LoopInvariant.mli               empty                        register plugin and methods
and also, added codes below in src/kernel/

module LoopInvariant = struct
let run = mk_fun "" 
let theMain = mk_fun "LoopInvariant.theMain"

in src/kernel/db.mli

(** loop invariant plugin. By liu*)
module LoopInvariant : sig
val run:(Format.formatter -> unit) ref
val theMain:(unit -> unit) ref

I changeed file and added a section:

# Loop Invariant
check_plugin(loopInvariant,src/loop_invariant,[support for loopInv plugin],yes,no)

then executed command:
now I got file "Makefile" and I added such section:

# Loop Invariant
PLUGIN_CMO:= loop_parameters function_analysis register LoopInvariant
include share/Makefile.plugin

then executed command:
sudo make
and it emitted the error:
Unbound value Datatype.func in

if I committed the following codes in "", it just workd.So can you help me?

Best regards to you.