--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on December 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Dynamic Plugin



Hello Dillon,

Le mardi 02 d?cembre 2008 ? 10:58 +0100, Pariente Dillon a ?crit :
> Hello,
>  
> Some remarks about dynamic plugin designing, compiling, and launching.
>  
> 1?/ -dlcode in Makefile.template seems to be related to ocaml 3.11
> only, doesn't it?

Yes it is. But it is also related to native compilation only. Dynamic
linking of native code is not available for ocaml < 3.11.

> I'm currently using ocaml 3.10.2. Should I upgrade my ocaml version to
> get dynamic plugin capability? Even for bytecode generation? (plugins
> developper documentation on p.11 seemed to allow ocaml versions <
> 3.11).

If you want to use dynamic plug-ins in native mode, you have to upgrade
your ocaml compiler. But if you want to use only bytecode, then this is
not required.

> 2?/ once commenting in cmx installation (for a bytecode only
> generation) in Makefile.template,

There was a bug with "make install" of Makefile.template in the CVS
version. It is now fixed under CVS. Thank's for your bug report.

> the hello.cmo from the documentation example is copied in FRAMAC_SHARE
> directory.

Actually in FRAMAC_SHARE/plugins.

> But frama-c.byte -hello does not work : -hello option is not known
> (usage page is displayed).

It is worked on my computer. Have you any message just before the usage
page (e.g. "interface mismatch" or something like that) ?

You have to "make install" Frama-C, then "make" in hello_world, and next
"make install" in hello_world.

If you have still any problem, please let me know your compilation
process and your frama-c.byte output.

> Should I use Dynamic options to load dynamically hello.cmo with
> -load-module option? (indeed, it does not seem to work as well!, and
> documentation does not give any hints about this).

No, it is not required. This option may be used if you want to load a
module which does not belong to FRAMAC_DYN_PATH. This variable is set by
default to "lib/plugins; $FRAMAC_SHARE/plugins".

Hope this helps,
Julien

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