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>