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] Compilation of Beryllium 20090901 without dynlink

Hi!

> AFAICS, there is another issue which hasn't been fixed yet: Dynlink  
> is not
> properly activated when there is no `ocamlc -where`/dynlink.cmxa but  
> only
> `ocamlc -where`/dynlink.cma and I don't see any fix for that in the  
> patch.
>
> The test is simple:
> - Move `ocamlc -where`/dynlink.cmxa to `ocamlc -where`/ 
> dynlink.cmxa.old
> - Test presence of `ocamlc -where`/dynlink.cma (Just to be sure)
> - Run ? ./configure ? and you'll get:
> [?]
> checking for /usr/lib/ocaml/dynlink.cmxa... no
> configure: WARNING: native dynlink unavailable (ocaml 3.11 or higher  
> required)
> [?]

We used Mac OS X PPC as our "exotic platform" and there,
dynlink.cmxa exists ... and does not work. Which is a different
situation from the one you are asking us to reproduce.

 From your bug-report, it seems you are concerned by platforms on
which OCaml is only available as a bytecode compiler.
Do we agree that a "cleaner", if longer, way to reproduce the problem
is for us to compile & install only the bytecode version of
OCaml and to try to compile Frama-C in these conditions ?

I tried to reproduce the problem that you mention by following
the steps you indicate, but "make byte" in frama-c-Beryllium-20090901
worked fine. The compilation
failed for the native version, but I'm not sure what to conclude from
that since after following your instruction, my installation of OCaml
was inconsistent -- ocamlopt.opt available and missing dynlink.cmxa.

Pascal