--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on September 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Patch for OCaml 4.00.0



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>