--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on September 2009 ---
[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