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]

RE : [Frama-c-discuss] Re: [Why-discuss] Questions about Frama-C


  • Subject: RE : [Frama-c-discuss] Re: [Why-discuss] Questions about Frama-C
  • From: Benjamin.MONATE at cea.fr (MONATE Benjamin 205998)
  • Date: Sat Oct 11 00:01:35 2008
  • References: <004001c9292c$497e17b0$dc7a4710$@com><14791e30810080546o649e9b90la53e59cc741c882f@mail.gmail.com><006301c9294c$73712ce0$5a5386a0$@com><14791e30810080710w4adeb6c2j8eaef9ec4a1c21a3@mail.gmail.com><18a245bf0810091113q717fd014x3e8197341157d870@mail.gmail.com><14791e30810091153xb5bcf37r6ff3201a78d0e4f3@mail.gmail.com><18a245bf0810100930r58f1ae2cx65990ff1700bf57e@mail.gmail.com><14791e30810100944w21bdb6c7p4cbe17a322fa3ebe@mail.gmail.com><18a245bf0810100954g118da20aq69990be685381a5b@mail.gmail.com> <14791e30810101002o557f1bcbl9e3082811d4fb5e5@mail.gmail.com>

Hi,

You gave an incorrect preprocessing command line. Look at the warning emitted by cl.

In the manual section 3 you have this example:
frama-c-gui -val -cpp-command 'CL.exe /C /E %1 > %2' x.c
Does this work on your example ?


Benjamin Monate



-------- Message d'origine--------
De: frama-c-discuss-bounces@lists.gforge.inria.fr de la part de Yannick Moy
Date: ven. 10/10/2008 19:02
?: Satrajit Roy; frama-c-discuss
Objet : [Frama-c-discuss] Re: [Why-discuss] Questions about Frama-C
 
I answer to the list as well, so that somebody more knowledgable about the
GUI on windows can help. So you do not get a GUI opening with the source
file?

Yannick

On Fri, Oct 10, 2008 at 6:54 PM, Satrajit Roy <satrajit.roy@gmail.com>wrote:

> Well, I would expect to see 'x.c' showing up in some way shape or form
> somewhere in the gui window, or do I need to enable plug-ins at the gui
> command line as well.
>
> I was hoping that I could choose the plug-ins in the gui once the source
> files get parsed and analyzed correctly.
>
> By the way, I apologize, the command line was for frama-c-gui.
>
> On Fri, Oct 10, 2008 at 12:44 PM, Yannick Moy <yannick.moy@gmail.com>wrote:
>
>> Hi,
>>
>> You seem to get the normal behavior of Frama-C. It parses your code and
>> annotations, and it returns, unless a plugin is selected, like value
>> analysis with option -val.
>> If you want to perform deductive verification on your code using the
>> Jessie plugin, you should call it with option -jessie-analysis. Is that what
>> you want?
>>
>> Yannick
>>
>>
>> On Fri, Oct 10, 2008 at 6:30 PM, Satrajit Roy <satrajit.roy@gmail.com>wrote:
>>
>>>  Well, I still cannot get Frama-C to analyze src/win-iconv.c.
>>> Here is the command line I use to bring up Frama-C:
>>> C:\Documents and Settings\sroy>frama-c -msvc -cpp-command "cl /P" x.c
>>> [preprocessing] running cl /P x.c
>>> Microsoft (R) 32-bit C/C++ Optimizing Compiler Version 15.00.21022.08 for
>>> 80x86
>>> Copyright (C) Microsoft Corporation.  All rights reserved.
>>> cl : Command line warning D9035 : option 'o' has been deprecated and will
>>> be removed in a future release
>>> x.c
>>> Parsing
>>> Cleaning unused parts
>>> Symbolic link
>>> Starting semantical analysis
>>> What am I doing wrong?
>>>
>>> On Thu, Oct 9, 2008 at 2:53 PM, Yannick Moy <yannick.moy@gmail.com>wrote:
>>>
>>>> Hi,
>>>>
>>>> Frama-C uses by default cpp to preprocess source files, but you may
>>>> change this by setting option -cpp-command. Otherwise, Frama-C relies on CIL
>>>> to link source files and generate a unique abstract syntax tree to analyse.
>>>>
>>>> HTH,
>>>> Yannick
>>>>
>>>>
>>>> On Thu, Oct 9, 2008 at 8:13 PM, Satrajit Roy <satrajit.roy@gmail.com>wrote:
>>>>
>>>>>  Hi,
>>>>>
>>>>> I just downloaded Frama-C on my Windows box and it seems that it uses
>>>>> 'gcc' by default and I couldn't find any way to change it to use 'Visual
>>>>> C'. Is there a way to make Frama C use Vsiual C?
>>>>>
>>>>> Thanks in advance
>>>>>
>>>>
>>>>
>>>>
>>>> --
>>>> Yannick
>>>>
>>>
>>>
>>
>>
>> --
>> Yannick
>>
>
>


-- 
Yannick