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

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"
/*@ ; */