--- layout: fc_discuss_archives title: Message 55 from Frama-C-discuss on July 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Dynamic Plugin Enabled in Linux but Failed in Windows



Hi Julien,

$ frama-c.byte -print-plugin-path
/usr/local/lib/frama-c/plugins

$ ls `frama-c.byte -print-plugin-path `
Aorai.cmi  Aorai.cmxs  MyPlugin.cmxs             Security_slicing.cmo   gui
Aorai.cmo  MyPlugin.cmo    Security_slicing.cmi  Security_slicing.cmxs

$ frama-c.byte -help
Usage: C:\MinGW\msys\1.0\local\bin\frama-c.byte.exe [options and files...]
`C:\MinGW\msys\1.0\local\bin\frama-c.byte.exe -kernel-help' provides a
descripti
on of the general options of frama-c

***** LIST OF AVAILABLE PLUG-INS

dominators          Compute dominators and postdominators of statements;
                    use -dominators-help for specific options.
from analysis       functional dependencies;
                    use -from-help for specific options.
impact              impact analysis (experimental);
                    use -impact-help for specific options.
inout               operational, imperative and all kinds of
                    inputs/outputs;
                    use -inout-help for specific options.
metrics             syntactic metrics;
                    use -metrics-help for specific options.
occurrence          automatically computes where variables are used;
                    use -occurrence-help for specific options.
pdg                 Program Dependence Graph;
                    use -pdg-help for specific options.
postdominators      computing postdominators of statements;
                    use -postdominators-help for specific options.
report              Properties Status Report (experimental);
                    use -report-help for specific options.
rte annotation      generates annotations for runtime error checking and
                    preconditions at call sites;
                    use -rte-help for specific options.
scope               data dependencies higher level functions;
                    use -scope-help for specific options.
semantic callgraph  semantic stratified callgraph;
                    use -scg-help for specific options.
semantic constant folding  propagates constants semantically;
                    use -scf-help for specific options.
slicing             code slicer;
                    use -slicing-help for specific options.
sparecode           code cleaner;
                    use -sparecode-help for specific options.
syntactic callgraph  syntactic stratified callgraph;
                    use -cg-help for specific options.
users               function callees;
                    use -users-help for specific options.
value analysis      automatically computes variation domains for the
                    variables of the program;
                    use -value-help for specific options.


I found the plugin exists in /usr/local/lib/frama-c/plugins, but not exists
in help info.

Thanks,
Haihao

On Thu, Jul 26, 2012 at 9:21 PM, Julien Signoles <Julien.Signoles at cea.fr>wrote:

> Hello,
>
>
> On 07/23/2012 04:30 PM, haihao shen wrote:
>
>> I experimented a frama-c dynamic plugin with the following content in
>> makefile:
>>
>> # Frama-c should be properly installed with "make install"
>> # before any use of this makefile
>>
>> FRAMAC_SHARE :=$(shell frama-c.byte -print-path)
>> FRAMAC_LIBDIR :=$(shell frama-c.byte -print-libpath)
>> PLUGIN_DIR ?= .
>> PLUGIN_NAME := MyPlugin
>> PLUGIN_CMI :=
>> PLUGIN_CMO := register
>> include $(FRAMAC_SHARE)/Makefile.**dynamic
>>
>
> Looks ok.
>
>
>  It is okay in Ubuntu when I first make && make install frama-c, and then
>> make && make install my plugin. I confirmed by the help message from
>> frama-c -help.
>>
>> However, when I used the same code under Windows + MinGW and same make
>> && make install process, my plugin is not enabled.
>>
>> Does anyone encounter such kind of issue or know hoe to fix it?
>>
>
> I'm not aware of specific issues about dynamic plug-in installation under
> Windows+MinGw. What is the result of the following commands after
> installing your plug-in?
>
> $ frama-c.byte -print-plugin-path
> $ ls `frama-c.byte -print-plugin-path `
> $ frama-c.byte -help
>
> --
> Julien
>
> ______________________________**_________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.**inria.fr<Frama-c-discuss at lists.gforge.inria.fr>
> http://lists.gforge.inria.fr/**cgi-bin/mailman/listinfo/**frama-c-discuss<http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120727/f09c4e4f/attachment-0001.html>