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] Dynamic Plugin Enabled in Linux but Failed in Windows

  • Subject: [Frama-c-discuss] Dynamic Plugin Enabled in Linux but Failed in Windows
  • From: haihaoshen at gmail.com (haihao shen)
  • Date: Fri, 27 Jul 2012 08:59:11 +0800
  • In-reply-to: <5011444E.5050502@cea.fr>
  • References: <CAL2=Xae4+_d5vn7Ra0mF7CYHSG2N0MOGM=mNKOU5zPwM=z+6PQ@mail.gmail.com> <5011444E.5050502@cea.fr>
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>