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] Patch for OCaml 4.00.0
- Subject: [Frama-c-discuss] Patch for OCaml 4.00.0
- From: loganjerry at gmail.com (Jerry James)
- Date: Tue, 11 Sep 2012 14:09:25 -0600
Hello, 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. First, the Hashtbl signature changed. I patched cil/ocamlutils/inthash.ml(i) to add reset and stats functions. Second, frama-c would segfault on startup. The backtrace looked like this: src/kernel/journal.ml, line 222: let add ty v var = Type.Obj_tbl.add bindings ty v var (* eta-expansion required *) src/type/type.ml, line 486: O.replace tytbl (Obj.repr k) v OCaml sources: Hashtbl.replace OCaml sources: Hashtbl.replace_bucket Unfortunately, there is no debug information available for Hashtbl, due to the way the ocaml package is built in Fedora. Debugging pointed to this code in src/type/type.ml, module Obj_tbl: 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? I have attached the patch I am currently experimenting with for comment. A small change to configure.in to accept OCaml 4 is also necessary. Thanks and regards, -- Jerry James http://www.jamezone.org/ -------------- next part -------------- A non-text attachment was scrubbed... Name: frama-c-ocaml4.patch Type: application/octet-stream Size: 3129 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120911/eb6bb60f/attachment.obj>
- Prev by Date: [Frama-c-discuss] the meaning of a curve or arc in PDG.
- Next by Date: [Frama-c-discuss] Patch for OCaml 4.00.0
- Previous by thread: [Frama-c-discuss] the meaning of a curve or arc in PDG.
- Next by thread: [Frama-c-discuss] Patch for OCaml 4.00.0