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: Wed, 1 Aug 2012 21:43:20 +0800
  • In-reply-to: <CAL2=XaeQZukEGSY=yRZ=zbph0ZWF58o34KDAb_OMvEe3zo1WSw@mail.gmail.com>
  • References: <CAL2=Xae4+_d5vn7Ra0mF7CYHSG2N0MOGM=mNKOU5zPwM=z+6PQ@mail.gmail.com> <5011444E.5050502@cea.fr> <CAL2=Xae9S7FN1BvmeQUaGjeEmh-vz=Gx5JK=UEJyCsvQJjQcuA@mail.gmail.com> <3725558F-7179-42C8-803E-54FC6B93F235@cea.fr> <CAL2=XaeQZukEGSY=yRZ=zbph0ZWF58o34KDAb_OMvEe3zo1WSw@mail.gmail.com>
Hi,

Sorry that I made a mistake. I tried adding prefix and actually it did no
work.
Here is the information after I added prefix:

$ 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 am wondering whether you know the reasons. Thanks in advance!

Best,
Haihao

On Sat, Jul 28, 2012 at 12:38 PM, haihao shen <haihaoshen at gmail.com> wrote:

> Thanks Benjamin and Virgile. It works well with --prefix Windows dir.
>
>
> On Fri, Jul 27, 2012 at 8:50 PM, MONATE Benjamin 205998 <
> Benjamin.MONATE at cea.fr> wrote:
>
>>
>>
>> Benjamin Monate
>> CEA LIST
>> Head of Software Safety Laboratory
>>
>> Le 27 juil. 2012 ? 02:59, "haihao shen" <haihaoshen at gmail.com> a ?crit :
>>
>> > Hi Julien,
>> >
>> > $ frama-c.byte -print-plugin-path
>> > /usr/local/lib/frama-c/plugins
>> >
>>
>> This is not a valid Win32 path.
>> Before compiling Frama-C you should add a correct prefix to Frama-C.
>> For example:
>> ./configure --prefix C:/Frama-C/
>> Avoid path with spaces and use forward slashes.
>> This is supposed to be explained in the INSTALL file.
>> Best regards,
>> Benjamin.
>>
>> _______________________________________________
>> Frama-c-discuss mailing list
>> Frama-c-discuss at lists.gforge.inria.fr
>> 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/20120801/db9fe5f2/attachment.html>