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] 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