--- layout: fc_discuss_archives title: Message 42 from Frama-C-discuss on October 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



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