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

Hello,

Mehdi Dogguy a ?crit :
> 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)
> [?]

The configure is right: /usr/lib/ocaml/dynlink.cmxa does not exist for 
your platform. So dynlink does not properly work in native (i.e. with 
ocamlopt) but I have understood that you have no native compiler: that's ok.

I don't understand your issue: in all cases, Dynlink (dynlink.cma) is 
available and linked against the bytecode (frama-c.byte). If I follow 
your instructions, the compilation succeeds for building the bytecode 
binary but fails for building the native binary. This failure is quite 
normal (as Pascal already answers). I have a local patch on my machine 
in order to be able to compile with ocamlopt >= 3.11 without 
dynlink.cmxa, but is it really necessary? I'm not sure...

So have you any reproducible issue with the bytecode (e.g. a dynamic 
plug-in like Jessie does not work) or have you any wanted feature wish 
for supporting a non-yet-available platform?

Best regards,
Julien Signoles
-- 
Researcher-engineer
CEA LIST, Software Reliability Lab
91191 Gif-Sur-Yvette Cedex
tel:(+33)1.69.08.82.98  fax:(+33)1.69.08.83.95  Julien.Signoles at cea.fr