[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel:file] result of parsing ./share/libc/__fc_builtin_for_normalization.i:
              /* Generated by Frama-C */
              int __builtin___fprintf_chk(void *, int, char const * , ...);
              
              void *__builtin___memcpy_chk(void *, void const *, unsigned int, unsigned int);
              
              void *__builtin___memmove_chk(void *, void const *, unsigned int,
                                            unsigned int);
              
              void *__builtin___mempcpy_chk(void *, void const *, unsigned int,
                                            unsigned int);
              
              void *__builtin___memset_chk(void *, int, unsigned int, unsigned int);
              
              int __builtin___printf_chk(int, char const * , ...);
              
              int __builtin___snprintf_chk(char *, unsigned int, int, unsigned int,
                                           char const * , ...);
              
              int __builtin___sprintf_chk(char *, int, unsigned int, char const * , ...);
              
              char *__builtin___stpcpy_chk(char *, char const *, unsigned int);
              
              char *__builtin___strcat_chk(char *, char const *, unsigned int);
              
              char *__builtin___strcpy_chk(char *, char const *, unsigned int);
              
              char *__builtin___strncat_chk(char *, char const *, unsigned int,
                                            unsigned int);
              
              char *__builtin___strncpy_chk(char *, char const *, unsigned int,
                                            unsigned int);
              
              int __builtin___vfprintf_chk(void *, int, char const *, __builtin_va_list);
              
              int __builtin___vprintf_chk(int, char const *, __builtin_va_list);
              
              int __builtin___vsnprintf_chk(char *, unsigned int, int, unsigned int,
                                            char const *, __builtin_va_list);
              
              int __builtin___vsprintf_chk(char *, int, unsigned int, char const *,
                                           __builtin_va_list);
              
              double __builtin_acos(double);
              
              float __builtin_acosf(float);
              
              long double __builtin_acosl(long double);
              
              void *__builtin_alloca(unsigned int);
              
              double __builtin_asin(double);
              
              float __builtin_asinf(float);
              
              long double __builtin_asinl(long double);
              
              double __builtin_atan(double);
              
              double __builtin_atan2(double, double);
              
              float __builtin_atan2f(float, float);
              
              long double __builtin_atan2l(long double, long double);
              
              float __builtin_atanf(float);
              
              long double __builtin_atanl(long double);
              
              unsigned short __builtin_bswap16(unsigned short);
              
              unsigned int __builtin_bswap32(unsigned int);
              
              unsigned long long __builtin_bswap64(unsigned long long);
              
              double __builtin_ceil(double);
              
              float __builtin_ceilf(float);
              
              long double __builtin_ceill(long double);
              
              int __builtin_clz(unsigned int);
              
              int __builtin_clzl(unsigned long);
              
              int __builtin_clzll(unsigned long long);
              
              int __builtin_constant_p(int);
              
              double __builtin_cos(double);
              
              float __builtin_cosf(float);
              
              double __builtin_cosh(double);
              
              float __builtin_coshf(float);
              
              long double __builtin_coshl(long double);
              
              long double __builtin_cosl(long double);
              
              int __builtin_ctz(unsigned int);
              
              int __builtin_ctzl(unsigned long);
              
              int __builtin_ctzll(unsigned long long);
              
              double __builtin_exp(double);
              
              long __builtin_expect(long, long);
              
              float __builtin_expf(float);
              
              long double __builtin_expl(long double);
              
              double __builtin_fabs(double);
              
              float __builtin_fabsf(float);
              
              long double __builtin_fabsl(long double);
              
              int __builtin_ffs(unsigned int);
              
              int __builtin_ffsl(unsigned long);
              
              int __builtin_ffsll(unsigned long long);
              
              double __builtin_floor(double);
              
              float __builtin_floorf(float);
              
              long double __builtin_floorl(long double);
              
              double __builtin_fmod(double);
              
              float __builtin_fmodf(float);
              
              long double __builtin_fmodl(long double);
              
              void *__builtin_frame_address(unsigned int);
              
              double __builtin_frexp(double, int *);
              
              float __builtin_frexpf(float, int *);
              
              long double __builtin_frexpl(long double, int *);
              
              double __builtin_huge_val(void);
              
              float __builtin_huge_valf(void);
              
              long double __builtin_huge_vall(void);
              
              void __builtin_ia32_lfence(void);
              
              void __builtin_ia32_mfence(void);
              
              void __builtin_ia32_sfence(void);
              
              double __builtin_inf(void);
              
              float __builtin_inff(void);
              
              long double __builtin_infl(void);
              
              double __builtin_ldexp(double, int);
              
              float __builtin_ldexpf(float, int);
              
              long double __builtin_ldexpl(long double, int);
              
              double __builtin_log(double);
              
              double __builtin_log10(double);
              
              float __builtin_log10f(float);
              
              long double __builtin_log10l(long double);
              
              float __builtin_logf(float);
              
              long double __builtin_logl(long double);
              
              void *__builtin_memcpy(void *, void const *, unsigned int);
              
              void *__builtin_mempcpy(void *, void const *, unsigned int);
              
              void *__builtin_memset(void *, int, int);
              
              float __builtin_modff(float, float *);
              
              long double __builtin_modfl(long double, long double *);
              
              double __builtin_nan(char const *);
              
              float __builtin_nanf(char const *);
              
              long double __builtin_nanl(char const *);
              
              double __builtin_nans(char const *);
              
              float __builtin_nansf(char const *);
              
              long double __builtin_nansl(char const *);
              
              __builtin_va_list __builtin_next_arg(void);
              
              unsigned int __builtin_object_size(void *, int);
              
              int __builtin_parity(unsigned int);
              
              int __builtin_parityl(unsigned long);
              
              int __builtin_parityll(unsigned long long);
              
              int __builtin_popcount(unsigned int);
              
              int __builtin_popcountl(unsigned long);
              
              int __builtin_popcountll(unsigned long long);
              
              double __builtin_powi(double, int);
              
              float __builtin_powif(float, int);
              
              long double __builtin_powil(long double, int);
              
              void __builtin_prefetch(void const * , ...);
              
              void __builtin_return(void const *);
              
              void *__builtin_return_address(unsigned int);
              
              double __builtin_sin(double);
              
              float __builtin_sinf(float);
              
              double __builtin_sinh(double);
              
              float __builtin_sinhf(float);
              
              long double __builtin_sinhl(long double);
              
              long double __builtin_sinl(long double);
              
              double __builtin_sqrt(double);
              
              float __builtin_sqrtf(float);
              
              long double __builtin_sqrtl(long double);
              
              void __builtin_stdarg_start(__builtin_va_list);
              
              char *__builtin_stpcpy(char *, char const *);
              
              char *__builtin_strchr(char *, int);
              
              int __builtin_strcmp(char const *, char const *);
              
              char *__builtin_strcpy(char *, char const *);
              
              unsigned int __builtin_strcspn(char const *, char const *);
              
              char *__builtin_strncat(char *, char const *, unsigned int);
              
              int __builtin_strncmp(char const *, char const *, unsigned int);
              
              char *__builtin_strncpy(char *, char const *, unsigned int);
              
              char *__builtin_strpbrk(char const *, char const *);
              
              unsigned int __builtin_strspn(char const *, char const *);
              
              double __builtin_tan(double);
              
              float __builtin_tanf(float);
              
              double __builtin_tanh(double);
              
              float __builtin_tanhf(float);
              
              long double __builtin_tanhl(long double);
              
              long double __builtin_tanl(long double);
              
              int __builtin_types_compatible_p(unsigned int, unsigned int);
              
              void __builtin_unreachable(void);
              
              void __builtin_va_arg(__builtin_va_list, unsigned int, void *);
              
              void __builtin_va_copy(__builtin_va_list, __builtin_va_list);
              
              void __builtin_va_end(__builtin_va_list);
              
              void __builtin_va_start(__builtin_va_list);
              
              void __builtin_varargs_start(__builtin_va_list);
              
              short __sync_add_and_fetch_int16_t(short *, short , ...);
              
              int __sync_add_and_fetch_int32_t(int *, int , ...);
              
              long long __sync_add_and_fetch_int64_t(long long *, long long , ...);
              
              signed char __sync_add_and_fetch_int8_t(signed char *, signed char , ...);
              
              unsigned short __sync_add_and_fetch_uint16_t(unsigned short *, unsigned short
                                                           , ...);
              
              unsigned int __sync_add_and_fetch_uint32_t(unsigned int *, unsigned int , ...);
              
              unsigned long long __sync_add_and_fetch_uint64_t(unsigned long long *,
                                                               unsigned long long , ...);
              
              unsigned char __sync_add_and_fetch_uint8_t(unsigned char *, unsigned char
                                                         , ...);
              
              short __sync_and_and_fetch_int16_t(short *, short , ...);
              
              int __sync_and_and_fetch_int32_t(int *, int , ...);
              
              long long __sync_and_and_fetch_int64_t(long long *, long long , ...);
              
              signed char __sync_and_and_fetch_int8_t(signed char *, signed char , ...);
              
              unsigned short __sync_and_and_fetch_uint16_t(unsigned short *, unsigned short
                                                           , ...);
              
              unsigned int __sync_and_and_fetch_uint32_t(unsigned int *, unsigned int , ...);
              
              unsigned long long __sync_and_and_fetch_uint64_t(unsigned long long *,
                                                               unsigned long long , ...);
              
              unsigned char __sync_and_and_fetch_uint8_t(unsigned char *, unsigned char
                                                         , ...);
              
              int __sync_bool_compare_and_swap_int16_t(short *, short, short , ...);
              
              int __sync_bool_compare_and_swap_int32_t(int *, int, int , ...);
              
              int __sync_bool_compare_and_swap_int64_t(long long *, long long, long long
                                                       , ...);
              
              int __sync_bool_compare_and_swap_int8_t(signed char *, signed char,
                                                      signed char , ...);
              
              int __sync_bool_compare_and_swap_uint16_t(unsigned short *, unsigned short,
                                                        unsigned short , ...);
              
              int __sync_bool_compare_and_swap_uint32_t(unsigned int *, unsigned int,
                                                        unsigned int , ...);
              
              int __sync_bool_compare_and_swap_uint64_t(unsigned long long *,
                                                        unsigned long long,
                                                        unsigned long long , ...);
              
              int __sync_bool_compare_and_swap_uint8_t(unsigned char *, unsigned char,
                                                       unsigned char , ...);
              
              short __sync_fetch_and_add_int16_t(short *, short , ...);
              
              int __sync_fetch_and_add_int32_t(int *, int , ...);
              
              long long __sync_fetch_and_add_int64_t(long long *, long long , ...);
              
              signed char __sync_fetch_and_add_int8_t(signed char *, signed char , ...);
              
              unsigned short __sync_fetch_and_add_uint16_t(unsigned short *, unsigned short
                                                           , ...);
              
              unsigned int __sync_fetch_and_add_uint32_t(unsigned int *, unsigned int , ...);
              
              unsigned long long __sync_fetch_and_add_uint64_t(unsigned long long *,
                                                               unsigned long long , ...);
              
              unsigned char __sync_fetch_and_add_uint8_t(unsigned char *, unsigned char
                                                         , ...);
              
              short __sync_fetch_and_and_int16_t(short *, short , ...);
              
              int __sync_fetch_and_and_int32_t(int *, int , ...);
              
              long long __sync_fetch_and_and_int64_t(long long *, long long , ...);
              
              signed char __sync_fetch_and_and_int8_t(signed char *, signed char , ...);
              
              unsigned short __sync_fetch_and_and_uint16_t(unsigned short *, unsigned short
                                                           , ...);
              
              unsigned int __sync_fetch_and_and_uint32_t(unsigned int *, unsigned int , ...);
              
              unsigned long long __sync_fetch_and_and_uint64_t(unsigned long long *,
                                                               unsigned long long , ...);
              
              unsigned char __sync_fetch_and_and_uint8_t(unsigned char *, unsigned char
                                                         , ...);
              
              short __sync_fetch_and_nand_int16_t(short *, short , ...);
              
              int __sync_fetch_and_nand_int32_t(int *, int , ...);
              
              long long __sync_fetch_and_nand_int64_t(long long *, long long , ...);
              
              signed char __sync_fetch_and_nand_int8_t(signed char *, signed char , ...);
              
              unsigned short __sync_fetch_and_nand_uint16_t(unsigned short *,
                                                            unsigned short , ...);
              
              unsigned int __sync_fetch_and_nand_uint32_t(unsigned int *, unsigned int
                                                          , ...);
              
              unsigned long long __sync_fetch_and_nand_uint64_t(unsigned long long *,
                                                                unsigned long long , ...);
              
              unsigned char __sync_fetch_and_nand_uint8_t(unsigned char *, unsigned char
                                                          , ...);
              
              short __sync_fetch_and_or_int16_t(short *, short , ...);
              
              int __sync_fetch_and_or_int32_t(int *, int , ...);
              
              long long __sync_fetch_and_or_int64_t(long long *, long long , ...);
              
              signed char __sync_fetch_and_or_int8_t(signed char *, signed char , ...);
              
              unsigned short __sync_fetch_and_or_uint16_t(unsigned short *, unsigned short
                                                          , ...);
              
              unsigned int __sync_fetch_and_or_uint32_t(unsigned int *, unsigned int , ...);
              
              unsigned long long __sync_fetch_and_or_uint64_t(unsigned long long *,
                                                              unsigned long long , ...);
              
              unsigned char __sync_fetch_and_or_uint8_t(unsigned char *, unsigned char
                                                        , ...);
              
              short __sync_fetch_and_sub_int16_t(short *, short , ...);
              
              int __sync_fetch_and_sub_int32_t(int *, int , ...);
              
              long long __sync_fetch_and_sub_int64_t(long long *, long long , ...);
              
              signed char __sync_fetch_and_sub_int8_t(signed char *, signed char , ...);
              
              unsigned short __sync_fetch_and_sub_uint16_t(unsigned short *, unsigned short
                                                           , ...);
              
              unsigned int __sync_fetch_and_sub_uint32_t(unsigned int *, unsigned int , ...);
              
              unsigned long long __sync_fetch_and_sub_uint64_t(unsigned long long *,
                                                               unsigned long long , ...);
              
              unsigned char __sync_fetch_and_sub_uint8_t(unsigned char *, unsigned char
                                                         , ...);
              
              short __sync_fetch_and_xor_int16_t(short *, short , ...);
              
              int __sync_fetch_and_xor_int32_t(int *, int , ...);
              
              long long __sync_fetch_and_xor_int64_t(long long *, long long , ...);
              
              signed char __sync_fetch_and_xor_int8_t(signed char *, signed char , ...);
              
              unsigned short __sync_fetch_and_xor_uint16_t(unsigned short *, unsigned short
                                                           , ...);
              
              unsigned int __sync_fetch_and_xor_uint32_t(unsigned int *, unsigned int , ...);
              
              unsigned long long __sync_fetch_and_xor_uint64_t(unsigned long long *,
                                                               unsigned long long , ...);
              
              unsigned char __sync_fetch_and_xor_uint8_t(unsigned char *, unsigned char
                                                         , ...);
              
              void __sync_lock_release_int16_t(short * , ...);
              
              void __sync_lock_release_int32_t(int * , ...);
              
              void __sync_lock_release_int64_t(long long * , ...);
              
              void __sync_lock_release_int8_t(signed char * , ...);
              
              void __sync_lock_release_uint16_t(unsigned short * , ...);
              
              void __sync_lock_release_uint32_t(unsigned int * , ...);
              
              void __sync_lock_release_uint64_t(unsigned long long * , ...);
              
              void __sync_lock_release_uint8_t(unsigned char * , ...);
              
              short __sync_lock_test_and_set_int16_t(short *, short , ...);
              
              int __sync_lock_test_and_set_int32_t(int *, int , ...);
              
              long long __sync_lock_test_and_set_int64_t(long long *, long long , ...);
              
              signed char __sync_lock_test_and_set_int8_t(signed char *, signed char , ...);
              
              unsigned short __sync_lock_test_and_set_uint16_t(unsigned short *,
                                                               unsigned short , ...);
              
              unsigned int __sync_lock_test_and_set_uint32_t(unsigned int *, unsigned int
                                                             , ...);
              
              unsigned long long __sync_lock_test_and_set_uint64_t(unsigned long long *,
                                                                   unsigned long long , ...);
              
              unsigned char __sync_lock_test_and_set_uint8_t(unsigned char *, unsigned char
                                                             , ...);
              
              short __sync_nand_and_fetch_int16_t(short *, short , ...);
              
              int __sync_nand_and_fetch_int32_t(int *, int , ...);
              
              long long __sync_nand_and_fetch_int64_t(long long *, long long , ...);
              
              signed char __sync_nand_and_fetch_int8_t(signed char *, signed char , ...);
              
              unsigned short __sync_nand_and_fetch_uint16_t(unsigned short *,
                                                            unsigned short , ...);
              
              unsigned int __sync_nand_and_fetch_uint32_t(unsigned int *, unsigned int
                                                          , ...);
              
              unsigned long long __sync_nand_and_fetch_uint64_t(unsigned long long *,
                                                                unsigned long long , ...);
              
              unsigned char __sync_nand_and_fetch_uint8_t(unsigned char *, unsigned char
                                                          , ...);
              
              short __sync_or_and_fetch_int16_t(short *, short , ...);
              
              int __sync_or_and_fetch_int32_t(int *, int , ...);
              
              long long __sync_or_and_fetch_int64_t(long long *, long long , ...);
              
              signed char __sync_or_and_fetch_int8_t(signed char *, signed char , ...);
              
              unsigned short __sync_or_and_fetch_uint16_t(unsigned short *, unsigned short
                                                          , ...);
              
              unsigned int __sync_or_and_fetch_uint32_t(unsigned int *, unsigned int , ...);
              
              unsigned long long __sync_or_and_fetch_uint64_t(unsigned long long *,
                                                              unsigned long long , ...);
              
              unsigned char __sync_or_and_fetch_uint8_t(unsigned char *, unsigned char
                                                        , ...);
              
              short __sync_sub_and_fetch_int16_t(short *, short , ...);
              
              int __sync_sub_and_fetch_int32_t(int *, int , ...);
              
              long long __sync_sub_and_fetch_int64_t(long long *, long long , ...);
              
              signed char __sync_sub_and_fetch_int8_t(signed char *, signed char , ...);
              
              unsigned short __sync_sub_and_fetch_uint16_t(unsigned short *, unsigned short
                                                           , ...);
              
              unsigned int __sync_sub_and_fetch_uint32_t(unsigned int *, unsigned int , ...);
              
              unsigned long long __sync_sub_and_fetch_uint64_t(unsigned long long *,
                                                               unsigned long long , ...);
              
              unsigned char __sync_sub_and_fetch_uint8_t(unsigned char *, unsigned char
                                                         , ...);
              
              void __sync_synchronize(...);
              
              short __sync_val_compare_and_swap_int16_t(short *, short, short , ...);
              
              int __sync_val_compare_and_swap_int32_t(int *, int, int , ...);
              
              long long __sync_val_compare_and_swap_int64_t(long long *, long long,
                                                            long long , ...);
              
              signed char __sync_val_compare_and_swap_int8_t(signed char *, signed char,
                                                             signed char , ...);
              
              unsigned short __sync_val_compare_and_swap_uint16_t(unsigned short *,
                                                                  unsigned short,
                                                                  unsigned short , ...);
              
              unsigned int __sync_val_compare_and_swap_uint32_t(unsigned int *,
                                                                unsigned int, unsigned int
                                                                , ...);
              
              unsigned long long __sync_val_compare_and_swap_uint64_t(unsigned long long *,
                                                                      unsigned long long,
                                                                      unsigned long long
                                                                      , ...);
              
              unsigned char __sync_val_compare_and_swap_uint8_t(unsigned char *,
                                                                unsigned char,
                                                                unsigned char , ...);
              
              short __sync_xor_and_fetch_int16_t(short *, short , ...);
              
              int __sync_xor_and_fetch_int32_t(int *, int , ...);
              
              long long __sync_xor_and_fetch_int64_t(long long *, long long , ...);
              
              signed char __sync_xor_and_fetch_int8_t(signed char *, signed char , ...);
              
              unsigned short __sync_xor_and_fetch_uint16_t(unsigned short *, unsigned short
                                                           , ...);
              
              unsigned int __sync_xor_and_fetch_uint32_t(unsigned int *, unsigned int , ...);
              
              unsigned long long __sync_xor_and_fetch_uint64_t(unsigned long long *,
                                                               unsigned long long , ...);
              
              unsigned char __sync_xor_and_fetch_uint8_t(unsigned char *, unsigned char
                                                         , ...);
[kernel] Parsing tests/syntax/check_builtin_bts1440.i (no preprocessing)
[kernel:file] result of parsing tests/syntax/check_builtin_bts1440.i:
              /* Generated by Frama-C */
              int __builtin___fprintf_chk(void *, int, char const * , ...);
              
              void *__builtin___memcpy_chk(void *, void const *, unsigned int, unsigned int);
              
              void *__builtin___memmove_chk(void *, void const *, unsigned int,
                                            unsigned int);
              
              void *__builtin___mempcpy_chk(void *, void const *, unsigned int,
                                            unsigned int);
              
              void *__builtin___memset_chk(void *, int, unsigned int, unsigned int);
              
              int __builtin___printf_chk(int, char const * , ...);
              
              int __builtin___snprintf_chk(char *, unsigned int, int, unsigned int,
                                           char const * , ...);
              
              int __builtin___sprintf_chk(char *, int, unsigned int, char const * , ...);
              
              char *__builtin___stpcpy_chk(char *, char const *, unsigned int);
              
              char *__builtin___strcat_chk(char *, char const *, unsigned int);
              
              char *__builtin___strcpy_chk(char *, char const *, unsigned int);
              
              char *__builtin___strncat_chk(char *, char const *, unsigned int,
                                            unsigned int);
              
              char *__builtin___strncpy_chk(char *, char const *, unsigned int,
                                            unsigned int);
              
              int __builtin___vfprintf_chk(void *, int, char const *, __builtin_va_list);
              
              int __builtin___vprintf_chk(int, char const *, __builtin_va_list);
              
              int __builtin___vsnprintf_chk(char *, unsigned int, int, unsigned int,
                                            char const *, __builtin_va_list);
              
              int __builtin___vsprintf_chk(char *, int, unsigned int, char const *,
                                           __builtin_va_list);
              
              double __builtin_acos(double);
              
              float __builtin_acosf(float);
              
              long double __builtin_acosl(long double);
              
              void *__builtin_alloca(unsigned int);
              
              double __builtin_asin(double);
              
              float __builtin_asinf(float);
              
              long double __builtin_asinl(long double);
              
              double __builtin_atan(double);
              
              double __builtin_atan2(double, double);
              
              float __builtin_atan2f(float, float);
              
              long double __builtin_atan2l(long double, long double);
              
              float __builtin_atanf(float);
              
              long double __builtin_atanl(long double);
              
              unsigned short __builtin_bswap16(unsigned short);
              
              unsigned int __builtin_bswap32(unsigned int);
              
              unsigned long long __builtin_bswap64(unsigned long long);
              
              double __builtin_ceil(double);
              
              float __builtin_ceilf(float);
              
              long double __builtin_ceill(long double);
              
              int __builtin_clz(unsigned int);
              
              int __builtin_clzl(unsigned long);
              
              int __builtin_clzll(unsigned long long);
              
              int __builtin_constant_p(int);
              
              double __builtin_cos(double);
              
              float __builtin_cosf(float);
              
              double __builtin_cosh(double);
              
              float __builtin_coshf(float);
              
              long double __builtin_coshl(long double);
              
              long double __builtin_cosl(long double);
              
              int __builtin_ctz(unsigned int);
              
              int __builtin_ctzl(unsigned long);
              
              int __builtin_ctzll(unsigned long long);
              
              double __builtin_exp(double);
              
              long __builtin_expect(long, long);
              
              float __builtin_expf(float);
              
              long double __builtin_expl(long double);
              
              double __builtin_fabs(double);
              
              float __builtin_fabsf(float);
              
              long double __builtin_fabsl(long double);
              
              int __builtin_ffs(unsigned int);
              
              int __builtin_ffsl(unsigned long);
              
              int __builtin_ffsll(unsigned long long);
              
              double __builtin_floor(double);
              
              float __builtin_floorf(float);
              
              long double __builtin_floorl(long double);
              
              double __builtin_fmod(double);
              
              float __builtin_fmodf(float);
              
              long double __builtin_fmodl(long double);
              
              void *__builtin_frame_address(unsigned int);
              
              double __builtin_frexp(double, int *);
              
              float __builtin_frexpf(float, int *);
              
              long double __builtin_frexpl(long double, int *);
              
              double __builtin_huge_val(void);
              
              float __builtin_huge_valf(void);
              
              long double __builtin_huge_vall(void);
              
              void __builtin_ia32_lfence(void);
              
              void __builtin_ia32_mfence(void);
              
              void __builtin_ia32_sfence(void);
              
              double __builtin_inf(void);
              
              float __builtin_inff(void);
              
              long double __builtin_infl(void);
              
              double __builtin_ldexp(double, int);
              
              float __builtin_ldexpf(float, int);
              
              long double __builtin_ldexpl(long double, int);
              
              double __builtin_log(double);
              
              double __builtin_log10(double);
              
              float __builtin_log10f(float);
              
              long double __builtin_log10l(long double);
              
              float __builtin_logf(float);
              
              long double __builtin_logl(long double);
              
              void *__builtin_memcpy(void *, void const *, unsigned int);
              
              void *__builtin_mempcpy(void *, void const *, unsigned int);
              
              void *__builtin_memset(void *, int, int);
              
              float __builtin_modff(float, float *);
              
              long double __builtin_modfl(long double, long double *);
              
              double __builtin_nan(char const *);
              
              float __builtin_nanf(char const *);
              
              long double __builtin_nanl(char const *);
              
              double __builtin_nans(char const *);
              
              float __builtin_nansf(char const *);
              
              long double __builtin_nansl(char const *);
              
              __builtin_va_list __builtin_next_arg(void);
              
              unsigned int __builtin_object_size(void *, int);
              
              int __builtin_parity(unsigned int);
              
              int __builtin_parityl(unsigned long);
              
              int __builtin_parityll(unsigned long long);
              
              int __builtin_popcount(unsigned int);
              
              int __builtin_popcountl(unsigned long);
              
              int __builtin_popcountll(unsigned long long);
              
              double __builtin_powi(double, int);
              
              float __builtin_powif(float, int);
              
              long double __builtin_powil(long double, int);
              
              void __builtin_prefetch(void const * , ...);
              
              void __builtin_return(void const *);
              
              void *__builtin_return_address(unsigned int);
              
              double __builtin_sin(double);
              
              float __builtin_sinf(float);
              
              double __builtin_sinh(double);
              
              float __builtin_sinhf(float);
              
              long double __builtin_sinhl(long double);
              
              long double __builtin_sinl(long double);
              
              double __builtin_sqrt(double);
              
              float __builtin_sqrtf(float);
              
              long double __builtin_sqrtl(long double);
              
              void __builtin_stdarg_start(__builtin_va_list);
              
              char *__builtin_stpcpy(char *, char const *);
              
              char *__builtin_strchr(char *, int);
              
              int __builtin_strcmp(char const *, char const *);
              
              char *__builtin_strcpy(char *, char const *);
              
              unsigned int __builtin_strcspn(char const *, char const *);
              
              char *__builtin_strncat(char *, char const *, unsigned int);
              
              int __builtin_strncmp(char const *, char const *, unsigned int);
              
              char *__builtin_strncpy(char *, char const *, unsigned int);
              
              char *__builtin_strpbrk(char const *, char const *);
              
              unsigned int __builtin_strspn(char const *, char const *);
              
              double __builtin_tan(double);
              
              float __builtin_tanf(float);
              
              double __builtin_tanh(double);
              
              float __builtin_tanhf(float);
              
              long double __builtin_tanhl(long double);
              
              long double __builtin_tanl(long double);
              
              int __builtin_types_compatible_p(unsigned int, unsigned int);
              
              void __builtin_unreachable(void);
              
              void __builtin_va_arg(__builtin_va_list, unsigned int, void *);
              
              void __builtin_va_copy(__builtin_va_list, __builtin_va_list);
              
              void __builtin_va_end(__builtin_va_list);
              
              void __builtin_va_start(__builtin_va_list);
              
              void __builtin_varargs_start(__builtin_va_list);
              
              short __sync_add_and_fetch_int16_t(short *, short , ...);
              
              int __sync_add_and_fetch_int32_t(int *, int , ...);
              
              long long __sync_add_and_fetch_int64_t(long long *, long long , ...);
              
              signed char __sync_add_and_fetch_int8_t(signed char *, signed char , ...);
              
              unsigned short __sync_add_and_fetch_uint16_t(unsigned short *, unsigned short
                                                           , ...);
              
              unsigned int __sync_add_and_fetch_uint32_t(unsigned int *, unsigned int , ...);
              
              unsigned long long __sync_add_and_fetch_uint64_t(unsigned long long *,
                                                               unsigned long long , ...);
              
              unsigned char __sync_add_and_fetch_uint8_t(unsigned char *, unsigned char
                                                         , ...);
              
              short __sync_and_and_fetch_int16_t(short *, short , ...);
              
              int __sync_and_and_fetch_int32_t(int *, int , ...);
              
              long long __sync_and_and_fetch_int64_t(long long *, long long , ...);
              
              signed char __sync_and_and_fetch_int8_t(signed char *, signed char , ...);
              
              unsigned short __sync_and_and_fetch_uint16_t(unsigned short *, unsigned short
                                                           , ...);
              
              unsigned int __sync_and_and_fetch_uint32_t(unsigned int *, unsigned int , ...);
              
              unsigned long long __sync_and_and_fetch_uint64_t(unsigned long long *,
                                                               unsigned long long , ...);
              
              unsigned char __sync_and_and_fetch_uint8_t(unsigned char *, unsigned char
                                                         , ...);
              
              int __sync_bool_compare_and_swap_int16_t(short *, short, short , ...);
              
              int __sync_bool_compare_and_swap_int32_t(int *, int, int , ...);
              
              int __sync_bool_compare_and_swap_int64_t(long long *, long long, long long
                                                       , ...);
              
              int __sync_bool_compare_and_swap_int8_t(signed char *, signed char,
                                                      signed char , ...);
              
              int __sync_bool_compare_and_swap_uint16_t(unsigned short *, unsigned short,
                                                        unsigned short , ...);
              
              int __sync_bool_compare_and_swap_uint32_t(unsigned int *, unsigned int,
                                                        unsigned int , ...);
              
              int __sync_bool_compare_and_swap_uint64_t(unsigned long long *,
                                                        unsigned long long,
                                                        unsigned long long , ...);
              
              int __sync_bool_compare_and_swap_uint8_t(unsigned char *, unsigned char,
                                                       unsigned char , ...);
              
              short __sync_fetch_and_add_int16_t(short *, short , ...);
              
              int __sync_fetch_and_add_int32_t(int *, int , ...);
              
              long long __sync_fetch_and_add_int64_t(long long *, long long , ...);
              
              signed char __sync_fetch_and_add_int8_t(signed char *, signed char , ...);
              
              unsigned short __sync_fetch_and_add_uint16_t(unsigned short *, unsigned short
                                                           , ...);
              
              unsigned int __sync_fetch_and_add_uint32_t(unsigned int *, unsigned int , ...);
              
              unsigned long long __sync_fetch_and_add_uint64_t(unsigned long long *,
                                                               unsigned long long , ...);
              
              unsigned char __sync_fetch_and_add_uint8_t(unsigned char *, unsigned char
                                                         , ...);
              
              short __sync_fetch_and_and_int16_t(short *, short , ...);
              
              int __sync_fetch_and_and_int32_t(int *, int , ...);
              
              long long __sync_fetch_and_and_int64_t(long long *, long long , ...);
              
              signed char __sync_fetch_and_and_int8_t(signed char *, signed char , ...);
              
              unsigned short __sync_fetch_and_and_uint16_t(unsigned short *, unsigned short
                                                           , ...);
              
              unsigned int __sync_fetch_and_and_uint32_t(unsigned int *, unsigned int , ...);
              
              unsigned long long __sync_fetch_and_and_uint64_t(unsigned long long *,
                                                               unsigned long long , ...);
              
              unsigned char __sync_fetch_and_and_uint8_t(unsigned char *, unsigned char
                                                         , ...);
              
              short __sync_fetch_and_nand_int16_t(short *, short , ...);
              
              int __sync_fetch_and_nand_int32_t(int *, int , ...);
              
              long long __sync_fetch_and_nand_int64_t(long long *, long long , ...);
              
              signed char __sync_fetch_and_nand_int8_t(signed char *, signed char , ...);
              
              unsigned short __sync_fetch_and_nand_uint16_t(unsigned short *,
                                                            unsigned short , ...);
              
              unsigned int __sync_fetch_and_nand_uint32_t(unsigned int *, unsigned int
                                                          , ...);
              
              unsigned long long __sync_fetch_and_nand_uint64_t(unsigned long long *,
                                                                unsigned long long , ...);
              
              unsigned char __sync_fetch_and_nand_uint8_t(unsigned char *, unsigned char
                                                          , ...);
              
              short __sync_fetch_and_or_int16_t(short *, short , ...);
              
              int __sync_fetch_and_or_int32_t(int *, int , ...);
              
              long long __sync_fetch_and_or_int64_t(long long *, long long , ...);
              
              signed char __sync_fetch_and_or_int8_t(signed char *, signed char , ...);
              
              unsigned short __sync_fetch_and_or_uint16_t(unsigned short *, unsigned short
                                                          , ...);
              
              unsigned int __sync_fetch_and_or_uint32_t(unsigned int *, unsigned int , ...);
              
              unsigned long long __sync_fetch_and_or_uint64_t(unsigned long long *,
                                                              unsigned long long , ...);
              
              unsigned char __sync_fetch_and_or_uint8_t(unsigned char *, unsigned char
                                                        , ...);
              
              short __sync_fetch_and_sub_int16_t(short *, short , ...);
              
              int __sync_fetch_and_sub_int32_t(int *, int , ...);
              
              long long __sync_fetch_and_sub_int64_t(long long *, long long , ...);
              
              signed char __sync_fetch_and_sub_int8_t(signed char *, signed char , ...);
              
              unsigned short __sync_fetch_and_sub_uint16_t(unsigned short *, unsigned short
                                                           , ...);
              
              unsigned int __sync_fetch_and_sub_uint32_t(unsigned int *, unsigned int , ...);
              
              unsigned long long __sync_fetch_and_sub_uint64_t(unsigned long long *,
                                                               unsigned long long , ...);
              
              unsigned char __sync_fetch_and_sub_uint8_t(unsigned char *, unsigned char
                                                         , ...);
              
              short __sync_fetch_and_xor_int16_t(short *, short , ...);
              
              int __sync_fetch_and_xor_int32_t(int *, int , ...);
              
              long long __sync_fetch_and_xor_int64_t(long long *, long long , ...);
              
              signed char __sync_fetch_and_xor_int8_t(signed char *, signed char , ...);
              
              unsigned short __sync_fetch_and_xor_uint16_t(unsigned short *, unsigned short
                                                           , ...);
              
              unsigned int __sync_fetch_and_xor_uint32_t(unsigned int *, unsigned int , ...);
              
              unsigned long long __sync_fetch_and_xor_uint64_t(unsigned long long *,
                                                               unsigned long long , ...);
              
              unsigned char __sync_fetch_and_xor_uint8_t(unsigned char *, unsigned char
                                                         , ...);
              
              void __sync_lock_release_int16_t(short * , ...);
              
              void __sync_lock_release_int32_t(int * , ...);
              
              void __sync_lock_release_int64_t(long long * , ...);
              
              void __sync_lock_release_int8_t(signed char * , ...);
              
              void __sync_lock_release_uint16_t(unsigned short * , ...);
              
              void __sync_lock_release_uint32_t(unsigned int * , ...);
              
              void __sync_lock_release_uint64_t(unsigned long long * , ...);
              
              void __sync_lock_release_uint8_t(unsigned char * , ...);
              
              short __sync_lock_test_and_set_int16_t(short *, short , ...);
              
              int __sync_lock_test_and_set_int32_t(int *, int , ...);
              
              long long __sync_lock_test_and_set_int64_t(long long *, long long , ...);
              
              signed char __sync_lock_test_and_set_int8_t(signed char *, signed char , ...);
              
              unsigned short __sync_lock_test_and_set_uint16_t(unsigned short *,
                                                               unsigned short , ...);
              
              unsigned int __sync_lock_test_and_set_uint32_t(unsigned int *, unsigned int
                                                             , ...);
              
              unsigned long long __sync_lock_test_and_set_uint64_t(unsigned long long *,
                                                                   unsigned long long , ...);
              
              unsigned char __sync_lock_test_and_set_uint8_t(unsigned char *, unsigned char
                                                             , ...);
              
              short __sync_nand_and_fetch_int16_t(short *, short , ...);
              
              int __sync_nand_and_fetch_int32_t(int *, int , ...);
              
              long long __sync_nand_and_fetch_int64_t(long long *, long long , ...);
              
              signed char __sync_nand_and_fetch_int8_t(signed char *, signed char , ...);
              
              unsigned short __sync_nand_and_fetch_uint16_t(unsigned short *,
                                                            unsigned short , ...);
              
              unsigned int __sync_nand_and_fetch_uint32_t(unsigned int *, unsigned int
                                                          , ...);
              
              unsigned long long __sync_nand_and_fetch_uint64_t(unsigned long long *,
                                                                unsigned long long , ...);
              
              unsigned char __sync_nand_and_fetch_uint8_t(unsigned char *, unsigned char
                                                          , ...);
              
              short __sync_or_and_fetch_int16_t(short *, short , ...);
              
              int __sync_or_and_fetch_int32_t(int *, int , ...);
              
              long long __sync_or_and_fetch_int64_t(long long *, long long , ...);
              
              signed char __sync_or_and_fetch_int8_t(signed char *, signed char , ...);
              
              unsigned short __sync_or_and_fetch_uint16_t(unsigned short *, unsigned short
                                                          , ...);
              
              unsigned int __sync_or_and_fetch_uint32_t(unsigned int *, unsigned int , ...);
              
              unsigned long long __sync_or_and_fetch_uint64_t(unsigned long long *,
                                                              unsigned long long , ...);
              
              unsigned char __sync_or_and_fetch_uint8_t(unsigned char *, unsigned char
                                                        , ...);
              
              short __sync_sub_and_fetch_int16_t(short *, short , ...);
              
              int __sync_sub_and_fetch_int32_t(int *, int , ...);
              
              long long __sync_sub_and_fetch_int64_t(long long *, long long , ...);
              
              signed char __sync_sub_and_fetch_int8_t(signed char *, signed char , ...);
              
              unsigned short __sync_sub_and_fetch_uint16_t(unsigned short *, unsigned short
                                                           , ...);
              
              unsigned int __sync_sub_and_fetch_uint32_t(unsigned int *, unsigned int , ...);
              
              unsigned long long __sync_sub_and_fetch_uint64_t(unsigned long long *,
                                                               unsigned long long , ...);
              
              unsigned char __sync_sub_and_fetch_uint8_t(unsigned char *, unsigned char
                                                         , ...);
              
              void __sync_synchronize(...);
              
              short __sync_val_compare_and_swap_int16_t(short *, short, short , ...);
              
              int __sync_val_compare_and_swap_int32_t(int *, int, int , ...);
              
              long long __sync_val_compare_and_swap_int64_t(long long *, long long,
                                                            long long , ...);
              
              signed char __sync_val_compare_and_swap_int8_t(signed char *, signed char,
                                                             signed char , ...);
              
              unsigned short __sync_val_compare_and_swap_uint16_t(unsigned short *,
                                                                  unsigned short,
                                                                  unsigned short , ...);
              
              unsigned int __sync_val_compare_and_swap_uint32_t(unsigned int *,
                                                                unsigned int, unsigned int
                                                                , ...);
              
              unsigned long long __sync_val_compare_and_swap_uint64_t(unsigned long long *,
                                                                      unsigned long long,
                                                                      unsigned long long
                                                                      , ...);
              
              unsigned char __sync_val_compare_and_swap_uint8_t(unsigned char *,
                                                                unsigned char,
                                                                unsigned char , ...);
              
              short __sync_xor_and_fetch_int16_t(short *, short , ...);
              
              int __sync_xor_and_fetch_int32_t(int *, int , ...);
              
              long long __sync_xor_and_fetch_int64_t(long long *, long long , ...);
              
              signed char __sync_xor_and_fetch_int8_t(signed char *, signed char , ...);
              
              unsigned short __sync_xor_and_fetch_uint16_t(unsigned short *, unsigned short
                                                           , ...);
              
              unsigned int __sync_xor_and_fetch_uint32_t(unsigned int *, unsigned int , ...);
              
              unsigned long long __sync_xor_and_fetch_uint64_t(unsigned long long *,
                                                               unsigned long long , ...);
              
              unsigned char __sync_xor_and_fetch_uint8_t(unsigned char *, unsigned char
                                                         , ...);
              
              int max(int i, int j)
              {
                int tmp;
                
                if (i >= j) tmp = i; else tmp = j;
                return tmp;
              }
[kernel:file:annotation] Marking properties
/* Generated by Frama-C */
/*@ ensures /* ip:6 */\result ≥ \old(i);
    ensures /* ip:7 */\result ≥ \old(j);
    ensures /* ip:8 */\result ≡ \old(i) ∨ \result ≡ \old(j);
 */
int max(int i, int j)
{
  /* Locals: tmp */
  int tmp;
  /* sid:2 */
  if (i >= j) {
    /* sid:3 */
    tmp = i;
  }
  else {
    /* sid:4 */
    tmp = j;
  }
  /* sid:5 */
  return tmp;
}