--- layout: fc_discuss_archives title: Message 3 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,

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