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] problem with pre-processing


Le 11/04/2011 15:24, SENE, Sali a ?crit :
> Thank you Pascal it solve the problem.
> I have another question: does Frama-c support pointer on function?

Frama-C User Manual, Section 2.3, page 12: "Frama-C analyses C programs. 
The C Source Code is assumed to follow the C 99 ISO Standard. [...] 
Furthermore, each analyzer may define the subsets of C [...] that it 
understands, as well as introduces specific limitations and hypotheses".

If you are using the value analysis plug-in, its specific limitations 
and hypotheses are explained in Chapter 4 "Limitations and 
Specificities" of the Value Analysis manual. As this chapter says 
nothing special about function pointers, they are fully supported by 
this plug-in.

Julien Signoles
CEA LIST, Laboratoire de S?ret? des Logiciels
point courrier 94, 91191 Gif-Sur-Yvette Cedex
tel:(+33)  fax:(+33)  Julien.Signoles at