--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on September 2012 ---
Hello, On 09/11/2012 10:09 PM, Jerry James wrote: > I am the current maintainer of the Frama-C package in the Fedora Linux > distribution. Our development branch recently updated to OCaml > 4.00.0. I encountered two problems when trying to build frama-c with > OCaml 4.00.0, and would like someone to look at my proposed solutions > to see if they appear to be correct. The next release of Frama-C, namely Oxygen, will be fully compatible with OCaml 4.00.0. Hopefully it will be release very soon. First, the Hashtbl signature > changed. I patched cil/ocamlutils/inthash.ml(i) to add reset and > stats functions. That is a correct patch. The next version of Frama-C will provide its own signature of Hashtbl, compatible with all supported version of OCaml (included OCaml 4). Additionnaly, module Inthash will disappear (superseded by Datatype.Int.Hashtbl). Second, frama-c would segfault on startup. > module O = > Hashtbl.Make(struct > type t = Obj.t > let equal = (==) > let hash x = > if !use_obj then > (* 0 is correct; trying to do a bit better... *) > let tag = Obj.tag x in > if tag = 0 then > 0 > else if tag = Obj.closure_tag then > (* assumes that the first word of a closure does not change in > any way (even by Gc.compact invokation). *) > Obj.magic (Obj.field x 0) > else > Hashtbl.hash x > else > 0 > end) > > In particular, lines 463-6 appear to be the problem. This is the part > that operates on closures. If I remove that part, frama-c "works", in > the sense that it doesn't segfault on startup anymore. But is that > correct? If not, what should be done here? That is correct again. After discussion with one of the OCaml developer recently, the line [Obj.magic (Obj.field x 0)] above was incorrect and work by chance before OCaml 4. He suggested me a better patch than replacing this line by [0], but it is still untested and it may also be broken with future OCaml optimization. > I have attached the patch I am currently experimenting with for > comment. The patch seems to be correct. A small change to configure.in to accept OCaml 4 is also > necessary. Yes, that's right. Thanks for maintaining Frama-C under Fedora, Best regards, Julien Signoles -- Researcher-engineer CEA LIST, Software Safety Labs tel:(+33)1.69.08.00.18 fax:(+33)1.69.08.83.95 Julien.Signoles at cea.fr