--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on November 2013 ---
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>