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