--- layout: fc_discuss_archives title: Message 42 from Frama-C-discuss on October 2008 ---
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