--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on November 2013 ---
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" /*@ ; */