--- layout: fc_discuss_archives title: Message 55 from Frama-C-discuss on July 2012 ---
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>