--- layout: fc_discuss_archives title: Message 70 from Frama-C-discuss on April 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Native dynamic plugin



Hello,

>  - First of all, I have a dynamic plugin that i would like to use in
> native mode. I add in my makefile the variable NATIVE set to yes. I do
> "make" and "make install" and it's ok .But I don't know how to launch
> my plugin because when i do "frama-c -help", I don't see my plugin.Can
> anyone help me?

Have you something like the below lines in the code of your plug-in.
=====
let () = 
  Options.add_plugin
    ~name:"hello world"
    ~descr:"Hello world plugin"
    [ (* options of your plug-in if any *) ];
=====

If you don't have such a line, add it and test again: that is this line
that adds the proper lines to "frama-c -help".

If you have such a line, please can you give the results of the
following bash commands (or the equivalent ones according to your
shell):
$ echo $FRAMAC_SHARE
$ echo $FRAMAC_DYN_PATH
$ cd your_plugin_directory; make install VERBOSEMAKE=yes
$ ls `unset FRAMAC_SHARE && frama-c -print-path`/plugins

> - Does exists a plugin that print the tree of my C file like  :
> Instr(Call(Some(Var t....etc   ?

As far as I know, no it doesn't.

Best regards,
Julien Signoles
-- 
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 at cea.fr