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: Julien.Signoles at cea.fr (Julien Signoles)
  • Date: Wed, 12 Sep 2012 09:47:39 +0200
  • In-reply-to: <CAHCOHQ=2oga_xUSywBo8ZEAgfAG-n0_qkbakC103dgiExrhLOw@mail.gmail.com>
  • References: <CAHCOHQ=2oga_xUSywBo8ZEAgfAG-n0_qkbakC103dgiExrhLOw@mail.gmail.com>
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