--- layout: fc_discuss_archives title: Message 35 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



On 07/11/2013 14:27, Pascal Cuoq wrote:

> could we see what is an example of output of cpp-4.8 that Frama-C dies
> on for a simple C file ?

Attached is the output of a file containing the following single line:

/*@ ; */

In case you wonder, putting an actual ACSL declaration instead of the 
semi-colon does not help.

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

The file above is not strictly compliant, since it is an empty 
translation unit. But adding declarations does not help either.

Best regards,

Guillaume
-------------- next part --------------
# 1 "toto.c"
#define __STDC__ 1
# 1 "toto.c"
#define __STDC_HOSTED__ 1
# 1 "toto.c"
#define __GNUC__ 4
# 1 "toto.c"
#define __GNUC_MINOR__ 8
# 1 "toto.c"
#define __GNUC_PATCHLEVEL__ 2
# 1 "toto.c"
#define __VERSION__ "4.8.2"
# 1 "toto.c"
#define __ATOMIC_RELAXED 0
# 1 "toto.c"
#define __ATOMIC_SEQ_CST 5
# 1 "toto.c"
#define __ATOMIC_ACQUIRE 2
# 1 "toto.c"
#define __ATOMIC_RELEASE 3
# 1 "toto.c"
#define __ATOMIC_ACQ_REL 4
# 1 "toto.c"
#define __ATOMIC_CONSUME 1
# 1 "toto.c"
#define __FINITE_MATH_ONLY__ 0
# 1 "toto.c"
#define _LP64 1
# 1 "toto.c"
#define __LP64__ 1
# 1 "toto.c"
#define __SIZEOF_INT__ 4
# 1 "toto.c"
#define __SIZEOF_LONG__ 8
# 1 "toto.c"
#define __SIZEOF_LONG_LONG__ 8
# 1 "toto.c"
#define __SIZEOF_SHORT__ 2
# 1 "toto.c"
#define __SIZEOF_FLOAT__ 4
# 1 "toto.c"
#define __SIZEOF_DOUBLE__ 8
# 1 "toto.c"
#define __SIZEOF_LONG_DOUBLE__ 16
# 1 "toto.c"
#define __SIZEOF_SIZE_T__ 8
# 1 "toto.c"
#define __CHAR_BIT__ 8
# 1 "toto.c"
#define __BIGGEST_ALIGNMENT__ 16
# 1 "toto.c"
#define __ORDER_LITTLE_ENDIAN__ 1234
# 1 "toto.c"
#define __ORDER_BIG_ENDIAN__ 4321
# 1 "toto.c"
#define __ORDER_PDP_ENDIAN__ 3412
# 1 "toto.c"
#define __BYTE_ORDER__ __ORDER_LITTLE_ENDIAN__
# 1 "toto.c"
#define __FLOAT_WORD_ORDER__ __ORDER_LITTLE_ENDIAN__
# 1 "toto.c"
#define __SIZEOF_POINTER__ 8
# 1 "toto.c"
#define __SIZE_TYPE__ long unsigned int
# 1 "toto.c"
#define __PTRDIFF_TYPE__ long int
# 1 "toto.c"
#define __WCHAR_TYPE__ int
# 1 "toto.c"
#define __WINT_TYPE__ unsigned int
# 1 "toto.c"
#define __INTMAX_TYPE__ long int
# 1 "toto.c"
#define __UINTMAX_TYPE__ long unsigned int
# 1 "toto.c"
#define __CHAR16_TYPE__ short unsigned int
# 1 "toto.c"
#define __CHAR32_TYPE__ unsigned int
# 1 "toto.c"
#define __SIG_ATOMIC_TYPE__ int
# 1 "toto.c"
#define __INT8_TYPE__ signed char
# 1 "toto.c"
#define __INT16_TYPE__ short int
# 1 "toto.c"
#define __INT32_TYPE__ int
# 1 "toto.c"
#define __INT64_TYPE__ long int
# 1 "toto.c"
#define __UINT8_TYPE__ unsigned char
# 1 "toto.c"
#define __UINT16_TYPE__ short unsigned int
# 1 "toto.c"
#define __UINT32_TYPE__ unsigned int
# 1 "toto.c"
#define __UINT64_TYPE__ long unsigned int
# 1 "toto.c"
#define __INT_LEAST8_TYPE__ signed char
# 1 "toto.c"
#define __INT_LEAST16_TYPE__ short int
# 1 "toto.c"
#define __INT_LEAST32_TYPE__ int
# 1 "toto.c"
#define __INT_LEAST64_TYPE__ long int
# 1 "toto.c"
#define __UINT_LEAST8_TYPE__ unsigned char
# 1 "toto.c"
#define __UINT_LEAST16_TYPE__ short unsigned int
# 1 "toto.c"
#define __UINT_LEAST32_TYPE__ unsigned int
# 1 "toto.c"
#define __UINT_LEAST64_TYPE__ long unsigned int
# 1 "toto.c"
#define __INT_FAST8_TYPE__ signed char
# 1 "toto.c"
#define __INT_FAST16_TYPE__ long int
# 1 "toto.c"
#define __INT_FAST32_TYPE__ long int
# 1 "toto.c"
#define __INT_FAST64_TYPE__ long int
# 1 "toto.c"
#define __UINT_FAST8_TYPE__ unsigned char
# 1 "toto.c"
#define __UINT_FAST16_TYPE__ long unsigned int
# 1 "toto.c"
#define __UINT_FAST32_TYPE__ long unsigned int
# 1 "toto.c"
#define __UINT_FAST64_TYPE__ long unsigned int
# 1 "toto.c"
#define __INTPTR_TYPE__ long int
# 1 "toto.c"
#define __UINTPTR_TYPE__ long unsigned int
# 1 "toto.c"
#define __GXX_ABI_VERSION 1002
# 1 "toto.c"
#define __SCHAR_MAX__ 127
# 1 "toto.c"
#define __SHRT_MAX__ 32767
# 1 "toto.c"
#define __INT_MAX__ 2147483647
# 1 "toto.c"
#define __LONG_MAX__ 9223372036854775807L
# 1 "toto.c"
#define __LONG_LONG_MAX__ 9223372036854775807LL
# 1 "toto.c"
#define __WCHAR_MAX__ 2147483647
# 1 "toto.c"
#define __WCHAR_MIN__ (-__WCHAR_MAX__ - 1)
# 1 "toto.c"
#define __WINT_MAX__ 4294967295U
# 1 "toto.c"
#define __WINT_MIN__ 0U
# 1 "toto.c"
#define __PTRDIFF_MAX__ 9223372036854775807L
# 1 "toto.c"
#define __SIZE_MAX__ 18446744073709551615UL
# 1 "toto.c"
#define __INTMAX_MAX__ 9223372036854775807L
# 1 "toto.c"
#define __INTMAX_C(c) c ## L
# 1 "toto.c"
#define __UINTMAX_MAX__ 18446744073709551615UL
# 1 "toto.c"
#define __UINTMAX_C(c) c ## UL
# 1 "toto.c"
#define __SIG_ATOMIC_MAX__ 2147483647
# 1 "toto.c"
#define __SIG_ATOMIC_MIN__ (-__SIG_ATOMIC_MAX__ - 1)
# 1 "toto.c"
#define __INT8_MAX__ 127
# 1 "toto.c"
#define __INT16_MAX__ 32767
# 1 "toto.c"
#define __INT32_MAX__ 2147483647
# 1 "toto.c"
#define __INT64_MAX__ 9223372036854775807L
# 1 "toto.c"
#define __UINT8_MAX__ 255
# 1 "toto.c"
#define __UINT16_MAX__ 65535
# 1 "toto.c"
#define __UINT32_MAX__ 4294967295U
# 1 "toto.c"
#define __UINT64_MAX__ 18446744073709551615UL
# 1 "toto.c"
#define __INT_LEAST8_MAX__ 127
# 1 "toto.c"
#define __INT8_C(c) c
# 1 "toto.c"
#define __INT_LEAST16_MAX__ 32767
# 1 "toto.c"
#define __INT16_C(c) c
# 1 "toto.c"
#define __INT_LEAST32_MAX__ 2147483647
# 1 "toto.c"
#define __INT32_C(c) c
# 1 "toto.c"
#define __INT_LEAST64_MAX__ 9223372036854775807L
# 1 "toto.c"
#define __INT64_C(c) c ## L
# 1 "toto.c"
#define __UINT_LEAST8_MAX__ 255
# 1 "toto.c"
#define __UINT8_C(c) c
# 1 "toto.c"
#define __UINT_LEAST16_MAX__ 65535
# 1 "toto.c"
#define __UINT16_C(c) c
# 1 "toto.c"
#define __UINT_LEAST32_MAX__ 4294967295U
# 1 "toto.c"
#define __UINT32_C(c) c ## U
# 1 "toto.c"
#define __UINT_LEAST64_MAX__ 18446744073709551615UL
# 1 "toto.c"
#define __UINT64_C(c) c ## UL
# 1 "toto.c"
#define __INT_FAST8_MAX__ 127
# 1 "toto.c"
#define __INT_FAST16_MAX__ 9223372036854775807L
# 1 "toto.c"
#define __INT_FAST32_MAX__ 9223372036854775807L
# 1 "toto.c"
#define __INT_FAST64_MAX__ 9223372036854775807L
# 1 "toto.c"
#define __UINT_FAST8_MAX__ 255
# 1 "toto.c"
#define __UINT_FAST16_MAX__ 18446744073709551615UL
# 1 "toto.c"
#define __UINT_FAST32_MAX__ 18446744073709551615UL
# 1 "toto.c"
#define __UINT_FAST64_MAX__ 18446744073709551615UL
# 1 "toto.c"
#define __INTPTR_MAX__ 9223372036854775807L
# 1 "toto.c"
#define __UINTPTR_MAX__ 18446744073709551615UL
# 1 "toto.c"
#define __FLT_EVAL_METHOD__ 0
# 1 "toto.c"
#define __DEC_EVAL_METHOD__ 2
# 1 "toto.c"
#define __FLT_RADIX__ 2
# 1 "toto.c"
#define __FLT_MANT_DIG__ 24
# 1 "toto.c"
#define __FLT_DIG__ 6
# 1 "toto.c"
#define __FLT_MIN_EXP__ (-125)
# 1 "toto.c"
#define __FLT_MIN_10_EXP__ (-37)
# 1 "toto.c"
#define __FLT_MAX_EXP__ 128
# 1 "toto.c"
#define __FLT_MAX_10_EXP__ 38
# 1 "toto.c"
#define __FLT_DECIMAL_DIG__ 9
# 1 "toto.c"
#define __FLT_MAX__ 3.40282346638528859812e+38F
# 1 "toto.c"
#define __FLT_MIN__ 1.17549435082228750797e-38F
# 1 "toto.c"
#define __FLT_EPSILON__ 1.19209289550781250000e-7F
# 1 "toto.c"
#define __FLT_DENORM_MIN__ 1.40129846432481707092e-45F
# 1 "toto.c"
#define __FLT_HAS_DENORM__ 1
# 1 "toto.c"
#define __FLT_HAS_INFINITY__ 1
# 1 "toto.c"
#define __FLT_HAS_QUIET_NAN__ 1
# 1 "toto.c"
#define __DBL_MANT_DIG__ 53
# 1 "toto.c"
#define __DBL_DIG__ 15
# 1 "toto.c"
#define __DBL_MIN_EXP__ (-1021)
# 1 "toto.c"
#define __DBL_MIN_10_EXP__ (-307)
# 1 "toto.c"
#define __DBL_MAX_EXP__ 1024
# 1 "toto.c"
#define __DBL_MAX_10_EXP__ 308
# 1 "toto.c"
#define __DBL_DECIMAL_DIG__ 17
# 1 "toto.c"
#define __DBL_MAX__ ((double)1.79769313486231570815e+308L)
# 1 "toto.c"
#define __DBL_MIN__ ((double)2.22507385850720138309e-308L)
# 1 "toto.c"
#define __DBL_EPSILON__ ((double)2.22044604925031308085e-16L)
# 1 "toto.c"
#define __DBL_DENORM_MIN__ ((double)4.94065645841246544177e-324L)
# 1 "toto.c"
#define __DBL_HAS_DENORM__ 1
# 1 "toto.c"
#define __DBL_HAS_INFINITY__ 1
# 1 "toto.c"
#define __DBL_HAS_QUIET_NAN__ 1
# 1 "toto.c"
#define __LDBL_MANT_DIG__ 64
# 1 "toto.c"
#define __LDBL_DIG__ 18
# 1 "toto.c"
#define __LDBL_MIN_EXP__ (-16381)
# 1 "toto.c"
#define __LDBL_MIN_10_EXP__ (-4931)
# 1 "toto.c"
#define __LDBL_MAX_EXP__ 16384
# 1 "toto.c"
#define __LDBL_MAX_10_EXP__ 4932
# 1 "toto.c"
#define __DECIMAL_DIG__ 21
# 1 "toto.c"
#define __LDBL_MAX__ 1.18973149535723176502e+4932L
# 1 "toto.c"
#define __LDBL_MIN__ 3.36210314311209350626e-4932L
# 1 "toto.c"
#define __LDBL_EPSILON__ 1.08420217248550443401e-19L
# 1 "toto.c"
#define __LDBL_DENORM_MIN__ 3.64519953188247460253e-4951L
# 1 "toto.c"
#define __LDBL_HAS_DENORM__ 1
# 1 "toto.c"
#define __LDBL_HAS_INFINITY__ 1
# 1 "toto.c"
#define __LDBL_HAS_QUIET_NAN__ 1
# 1 "toto.c"
#define __DEC32_MANT_DIG__ 7
# 1 "toto.c"
#define __DEC32_MIN_EXP__ (-94)
# 1 "toto.c"
#define __DEC32_MAX_EXP__ 97
# 1 "toto.c"
#define __DEC32_MIN__ 1E-95DF
# 1 "toto.c"
#define __DEC32_MAX__ 9.999999E96DF
# 1 "toto.c"
#define __DEC32_EPSILON__ 1E-6DF
# 1 "toto.c"
#define __DEC32_SUBNORMAL_MIN__ 0.000001E-95DF
# 1 "toto.c"
#define __DEC64_MANT_DIG__ 16
# 1 "toto.c"
#define __DEC64_MIN_EXP__ (-382)
# 1 "toto.c"
#define __DEC64_MAX_EXP__ 385
# 1 "toto.c"
#define __DEC64_MIN__ 1E-383DD
# 1 "toto.c"
#define __DEC64_MAX__ 9.999999999999999E384DD
# 1 "toto.c"
#define __DEC64_EPSILON__ 1E-15DD
# 1 "toto.c"
#define __DEC64_SUBNORMAL_MIN__ 0.000000000000001E-383DD
# 1 "toto.c"
#define __DEC128_MANT_DIG__ 34
# 1 "toto.c"
#define __DEC128_MIN_EXP__ (-6142)
# 1 "toto.c"
#define __DEC128_MAX_EXP__ 6145
# 1 "toto.c"
#define __DEC128_MIN__ 1E-6143DL
# 1 "toto.c"
#define __DEC128_MAX__ 9.999999999999999999999999999999999E6144DL
# 1 "toto.c"
#define __DEC128_EPSILON__ 1E-33DL
# 1 "toto.c"
#define __DEC128_SUBNORMAL_MIN__ 0.000000000000000000000000000000001E-6143DL
# 1 "toto.c"
#define __REGISTER_PREFIX__ 
# 1 "toto.c"
#define __USER_LABEL_PREFIX__ 
# 1 "toto.c"
#define __GNUC_GNU_INLINE__ 1
# 1 "toto.c"
#define __NO_INLINE__ 1
# 1 "toto.c"
#define __GCC_HAVE_SYNC_COMPARE_AND_SWAP_1 1
# 1 "toto.c"
#define __GCC_HAVE_SYNC_COMPARE_AND_SWAP_2 1
# 1 "toto.c"
#define __GCC_HAVE_SYNC_COMPARE_AND_SWAP_4 1
# 1 "toto.c"
#define __GCC_HAVE_SYNC_COMPARE_AND_SWAP_8 1
# 1 "toto.c"
#define __GCC_ATOMIC_BOOL_LOCK_FREE 2
# 1 "toto.c"
#define __GCC_ATOMIC_CHAR_LOCK_FREE 2
# 1 "toto.c"
#define __GCC_ATOMIC_CHAR16_T_LOCK_FREE 2
# 1 "toto.c"
#define __GCC_ATOMIC_CHAR32_T_LOCK_FREE 2
# 1 "toto.c"
#define __GCC_ATOMIC_WCHAR_T_LOCK_FREE 2
# 1 "toto.c"
#define __GCC_ATOMIC_SHORT_LOCK_FREE 2
# 1 "toto.c"
#define __GCC_ATOMIC_INT_LOCK_FREE 2
# 1 "toto.c"
#define __GCC_ATOMIC_LONG_LOCK_FREE 2
# 1 "toto.c"
#define __GCC_ATOMIC_LLONG_LOCK_FREE 2
# 1 "toto.c"
#define __GCC_ATOMIC_TEST_AND_SET_TRUEVAL 1
# 1 "toto.c"
#define __GCC_ATOMIC_POINTER_LOCK_FREE 2
# 1 "toto.c"
#define __GCC_HAVE_DWARF2_CFI_ASM 1
# 1 "toto.c"
#define __PRAGMA_REDEFINE_EXTNAME 1
# 1 "toto.c"
#define __SIZEOF_INT128__ 16
# 1 "toto.c"
#define __SIZEOF_WCHAR_T__ 4
# 1 "toto.c"
#define __SIZEOF_WINT_T__ 4
# 1 "toto.c"
#define __SIZEOF_PTRDIFF_T__ 8
# 1 "toto.c"
#define __amd64 1
# 1 "toto.c"
#define __amd64__ 1
# 1 "toto.c"
#define __x86_64 1
# 1 "toto.c"
#define __x86_64__ 1
# 1 "toto.c"
#define __ATOMIC_HLE_ACQUIRE 65536
# 1 "toto.c"
#define __ATOMIC_HLE_RELEASE 131072
# 1 "toto.c"
#define __k8 1
# 1 "toto.c"
#define __k8__ 1
# 1 "toto.c"
#define __code_model_small__ 1
# 1 "toto.c"
#define __MMX__ 1
# 1 "toto.c"
#define __SSE__ 1
# 1 "toto.c"
#define __SSE2__ 1
# 1 "toto.c"
#define __FXSR__ 1
# 1 "toto.c"
#define __SSE_MATH__ 1
# 1 "toto.c"
#define __SSE2_MATH__ 1
# 1 "toto.c"
#define __gnu_linux__ 1
# 1 "toto.c"
#define __linux 1
# 1 "toto.c"
#define __linux__ 1
# 1 "toto.c"
#define linux 1
# 1 "toto.c"
#define __unix 1
# 1 "toto.c"
#define __unix__ 1
# 1 "toto.c"
#define unix 1
# 1 "toto.c"
#define __ELF__ 1
# 1 "toto.c"
#define __DECIMAL_BID_FORMAT__ 1
# 1 "<command-line>"
# 1 "/usr/include/stdc-predef.h" 1 3 4
/* Copyright (C) 1991-2012 Free Software Foundation, Inc.
   This file is part of the GNU C Library.

   The GNU C Library is free software; you can redistribute it and/or
   modify it under the terms of the GNU Lesser General Public
   License as published by the Free Software Foundation; either
   version 2.1 of the License, or (at your option) any later version.

   The GNU C Library is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
   Lesser General Public License for more details.

   You should have received a copy of the GNU Lesser General Public
   License along with the GNU C Library; if not, see
   <http://www.gnu.org/licenses/>.  */


#define _STDC_PREDEF_H 1

/* This header is separate from features.h so that the compiler can
   include it implicitly at the start of every compilation.  It must
   not itself include <features.h> or any other header that includes
   <features.h> because the implicit include comes before any feature
   test macros that may be defined in a source file before it first
   explicitly includes a system header.  GCC knows the name of this
   header in order to preinclude it.  */

/* Define __STDC_IEC_559__ and other similar macros.  */
# 1 "/usr/include/x86_64-linux-gnu/bits/predefs.h" 1 3 4
/* Copyright (C) 2005 Free Software Foundation, Inc.
   This file is part of the GNU C Library.

   The GNU C Library is free software; you can redistribute it and/or
   modify it under the terms of the GNU Lesser General Public
   License as published by the Free Software Foundation; either
   version 2.1 of the License, or (at your option) any later version.

   The GNU C Library is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
   Lesser General Public License for more details.

   You should have received a copy of the GNU Lesser General Public
   License along with the GNU C Library; if not, write to the Free
   Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA
   02111-1307 USA.  */


#define _PREDEFS_H 





/* We do support the IEC 559 math functionality, real and complex.  */
#define __STDC_IEC_559__ 1
#define __STDC_IEC_559_COMPLEX__ 1
# 31 "/usr/include/stdc-predef.h" 2 3 4

/* wchar_t uses ISO/IEC 10646 (2nd ed., published 2011-03-15) /
   Unicode 6.0.  */
#define __STDC_ISO_10646__ 201103L

/* We do not support C11 <threads.h>.  */
#define __STDC_NO_THREADS__ 1
# 1 "<command-line>" 2
# 1 "toto.c"
/*@ ; */