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