--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] preprocessor problems with jessie



Pascal Cuoq <pascal.cuoq at gmail.com> writes:

> Hello John, Guillaume,

Hello,

> could we see what is an example of output of cpp-4.8 that Frama-C dies on for a simple C file ?
>
> John, if you end up being the one doing the exercise, special
> assignment : what is a minimal C99-compliant C file as per ?gcc
> -std=c99 -pedantic? that Frama-C dies on the output of cpp-4.8 of, and
> the output of cpp-4.8 on this file?

I have the same problem using a fresh install of Frama-C + Jessie via
Opam on Debian unstable or Ubuntu 13.04. Of course they both use gcc
4.8.

A simple function like

/*@ @*/
void func() { }

fails with jessie and passes (of course) gcc -std=c99 -pedantic. The
output of gcc -C -E -I. -dD func.c is attached. The output of frama-c on
this example is also attached.

The problem is that some definitions like __STDC_IEC_559__ appear in
both /usr/include/YOUR-ARCH/bits/predefs.h and
/usr/include/stdc-predef.h files from libc6-dev in Debian.

libc6-dev version in Debian stable is 2.11.3 and does not contain
stdc-predef.h while since testing livc6-dev version is 2.17 and
contains stdc-predef.h.

I hope this "report" will be useful.

Christophe

--
Christophe Garion          ISAE/DMIA - SUPAERO/IN
garion at isae.fr             10 avenue Edouard Belin
T?l : (33)5 61 33 80 57    BP 54032
Fax : (33)5 61 33 83 45    31055 Toulouse Cedex 4

-------------- next part --------------
A non-text attachment was scrubbed...
Name: func-preproc.c
Type: text/x-csrc
Size: 13475 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131107/ca38b5f0/attachment-0001.c>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: frama-c-func-output.txt
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131107/ca38b5f0/attachment-0001.txt>