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] Windows Install

  • Subject: [Frama-c-discuss] Windows Install
  • From: benjamin.monate at cea.fr (Benjamin Monate)
  • Date: Fri, 02 Oct 2009 20:49:34 +0200
  • In-reply-to: <000c01ca438e$7134c060$539e4120$@com>
  • References: <000c01ca438e$7134c060$539e4120$@com>
Hello,

Doug Wendelboe a ?crit :
> We are considering Frama-C to perform code verification for a biomedical 
> device. In the US the FDA guidelines for Verification & Validation (V&V) 
> fall under FDA regulations 21-CFR.

Nice project! I hope Frama-C will help you. I would really like to hear 
your conclusions about Frama-C at some point.

> Our organization uses the Windows OS 
> exclusively L. Although I unofficially use Linux when I can. Anyways, I 
> am having some simple startup configuration problems in starting up 
> Frama-C and trying out the example ?first.c? as shown on the website. I 
> see there are ample instructions for installing on Linux, but has anyone 
> written down instructions and dependencies for a Windows installation?

If you do not need to build Frama-C yourself on Widows then there is 
only one source of information: 
http://www.frama-c.cea.fr/windows_beryllium-20090902.html

> It appears that I need to tell Frama-C where my gcc installation is 
> located. Is this in a config file? Or is it a pathing setup problem? 
> Thanks for any help it getting us started.

The most simple solution is to have gcc or any kind preprocessor in your 
path.

If you cannot change your path, you may set the CPP environement 
variable to something like "c:/Program/gcc/gcc-bin.exe -CC -E -I."
In any case, if you need specific preprocessing options, you will have 
to use this variable (or its command line couter part -cpp-command".
See section 5.1.1 in the manual of the Value Analysis at 
http://www.frama-c.cea.fr/download/value-analysis-Beryllium.pdf
Note that the last example of this section uses CL.exe as preprocessor.

I hope you will succeed in your project, do not hesitate to ask further 
questions on this list.
-- 
| Benjamin Monate         | mailto:benjamin.monate at cea.fr     |
| Head of Software Safety Lab.  CEA-LIST/DRT/DTSI/SOL/LSL     |