check_builtin_bts1440.res.oracle

[kernel] Parsing check_builtin_bts1440.i (no preprocessing)
[kernel:file:print-one] 
  result of parsing check_builtin_bts1440.i:
  /* Generated by Frama-C */
  void __builtin__Exit(int __x0);
  
  int __builtin___fprintf_chk(void *__x0, int __x1, char const *__x2 , ...);
  
  void *__builtin___memcpy_chk(void *__x0, void const *__x1, unsigned int __x2,
                               unsigned int __x3);
  
  void *__builtin___memmove_chk(void *__x0, void const *__x1,
                                unsigned int __x2, unsigned int __x3);
  
  void *__builtin___mempcpy_chk(void *__x0, void const *__x1,
                                unsigned int __x2, unsigned int __x3);
  
  void *__builtin___memset_chk(void *__x0, int __x1, unsigned int __x2,
                               unsigned int __x3);
  
  int __builtin___printf_chk(int __x0, char const *__x1 , ...);
  
  int __builtin___snprintf_chk(char *__x0, unsigned int __x1, int __x2,
                               unsigned int __x3, char const *__x4 , ...);
  
  int __builtin___sprintf_chk(char *__x0, int __x1, unsigned int __x2,
                              char const *__x3 , ...);
  
  char *__builtin___stpcpy_chk(char *__x0, char const *__x1, unsigned int __x2);
  
  char *__builtin___strcat_chk(char *__x0, char const *__x1, unsigned int __x2);
  
  char *__builtin___strcpy_chk(char *__x0, char const *__x1, unsigned int __x2);
  
  char *__builtin___strncat_chk(char *__x0, char const *__x1,
                                unsigned int __x2, unsigned int __x3);
  
  char *__builtin___strncpy_chk(char *__x0, char const *__x1,
                                unsigned int __x2, unsigned int __x3);
  
  int __builtin___vfprintf_chk(void *__x0, int __x1, char const *__x2,
                               __builtin_va_list __x3);
  
  int __builtin___vprintf_chk(int __x0, char const *__x1,
                              __builtin_va_list __x2);
  
  int __builtin___vsnprintf_chk(char *__x0, unsigned int __x1, int __x2,
                                unsigned int __x3, char const *__x4,
                                __builtin_va_list __x5);
  
  int __builtin___vsprintf_chk(char *__x0, int __x1, unsigned int __x2,
                               char const *__x3, __builtin_va_list __x4);
  
  int __builtin_abs(int __x0);
  
  double __builtin_acos(double __x0);
  
  float __builtin_acosf(float __x0);
  
  double __builtin_acosh(double __x0);
  
  float __builtin_acoshf(float __x0);
  
  long double __builtin_acoshl(long double __x0);
  
  long double __builtin_acosl(long double __x0);
  
  void *__builtin_alloca(unsigned int __x0);
  
  double __builtin_asin(double __x0);
  
  float __builtin_asinf(float __x0);
  
  double __builtin_asinh(double __x0);
  
  float __builtin_asinhf(float __x0);
  
  long double __builtin_asinhl(long double __x0);
  
  long double __builtin_asinl(long double __x0);
  
  double __builtin_atan(double __x0);
  
  double __builtin_atan2(double __x0, double __x1);
  
  float __builtin_atan2f(float __x0, float __x1);
  
  long double __builtin_atan2l(long double __x0, long double __x1);
  
  float __builtin_atanf(float __x0);
  
  double __builtin_atanh(double __x0);
  
  float __builtin_atanhf(float __x0);
  
  long double __builtin_atanhl(long double __x0);
  
  long double __builtin_atanl(long double __x0);
  
  unsigned short __builtin_bswap16(unsigned short __x0);
  
  unsigned int __builtin_bswap32(unsigned int __x0);
  
  unsigned long long __builtin_bswap64(unsigned long long __x0);
  
  void *__builtin_calloc(unsigned int __x0, unsigned int __x1);
  
  double __builtin_cbrt(double __x0);
  
  float __builtin_cbrtf(float __x0);
  
  long double __builtin_cbrtl(long double __x0);
  
  double __builtin_ceil(double __x0);
  
  float __builtin_ceilf(float __x0);
  
  long double __builtin_ceill(long double __x0);
  
  int __builtin_constant_p(int __x0);
  
  double __builtin_copysign(double __x0, double __x1);
  
  float __builtin_copysignf(float __x0, float __x1);
  
  long double __builtin_copysignl(long double __x0, long double __x1);
  
  double __builtin_cos(double __x0);
  
  float __builtin_cosf(float __x0);
  
  double __builtin_cosh(double __x0);
  
  float __builtin_coshf(float __x0);
  
  long double __builtin_coshl(long double __x0);
  
  long double __builtin_cosl(long double __x0);
  
  double __builtin_erf(double __x0);
  
  double __builtin_erfc(double __x0);
  
  float __builtin_erfcf(float __x0);
  
  long double __builtin_erfcl(long double __x0);
  
  float __builtin_erff(float __x0);
  
  long double __builtin_erfl(long double __x0);
  
  void __builtin_exit(int __x0);
  
  double __builtin_exp(double __x0);
  
  double __builtin_exp2(double __x0);
  
  float __builtin_exp2f(float __x0);
  
  long double __builtin_exp2l(long double __x0);
  
  long __builtin_expect(long __x0, long __x1);
  
  float __builtin_expf(float __x0);
  
  long double __builtin_expl(long double __x0);
  
  double __builtin_expm1(double __x0);
  
  float __builtin_expm1f(float __x0);
  
  long double __builtin_expm1l(long double __x0);
  
  double __builtin_fabs(double __x0);
  
  float __builtin_fabsf(float __x0);
  
  long double __builtin_fabsl(long double __x0);
  
  double __builtin_fdim(double __x0, double __x1);
  
  float __builtin_fdimf(float __x0, float __x1);
  
  long double __builtin_fdiml(long double __x0, long double __x1);
  
  int __builtin_ffs(int __x0);
  
  int __builtin_ffsl(long __x0);
  
  int __builtin_ffsll(long long __x0);
  
  double __builtin_floor(double __x0);
  
  float __builtin_floorf(float __x0);
  
  long double __builtin_floorl(long double __x0);
  
  double __builtin_fma(double __x0, double __x1, double __x2);
  
  float __builtin_fmaf(float __x0, float __x1, float __x2);
  
  long double __builtin_fmal(long double __x0, long double __x1,
                             long double __x2);
  
  double __builtin_fmax(double __x0, double __x1);
  
  float __builtin_fmaxf(float __x0, float __x1);
  
  long double __builtin_fmaxl(long double __x0, long double __x1);
  
  double __builtin_fmin(double __x0, double __x1);
  
  float __builtin_fminf(float __x0, float __x1);
  
  long double __builtin_fminl(long double __x0, long double __x1);
  
  double __builtin_fmod(double __x0);
  
  float __builtin_fmodf(float __x0);
  
  long double __builtin_fmodl(long double __x0);
  
  int __builtin_fprintf(void *__x0, char const *__x1 , ...);
  
  int __builtin_fputs(char const *__x0, void *__x1);
  
  void *__builtin_frame_address(unsigned int __x0);
  
  void __builtin_free(void *__x0);
  
  double __builtin_frexp(double __x0, int *__x1);
  
  float __builtin_frexpf(float __x0, int *__x1);
  
  long double __builtin_frexpl(long double __x0, int *__x1);
  
  int __builtin_fscanf(void *__x0, char const *__x1 , ...);
  
  double __builtin_huge_val(void);
  
  float __builtin_huge_valf(void);
  
  long double __builtin_huge_vall(void);
  
  double __builtin_hypot(double __x0, double __x1);
  
  float __builtin_hypotf(float __x0, float __x1);
  
  long double __builtin_hypotl(long double __x0, long double __x1);
  
  void __builtin_ia32_lfence(void);
  
  void __builtin_ia32_mfence(void);
  
  void __builtin_ia32_sfence(void);
  
  double __builtin_ilogb(double __x0);
  
  float __builtin_ilogbf(float __x0);
  
  long double __builtin_ilogbl(long double __x0);
  
  double __builtin_inf(void);
  
  float __builtin_inff(void);
  
  long double __builtin_infl(void);
  
  int __builtin_isalnum(int __x0);
  
  int __builtin_isalpha(int __x0);
  
  int __builtin_isblank(int __x0);
  
  int __builtin_iscntrl(int __x0);
  
  int __builtin_isdigit(int __x0);
  
  int __builtin_isgraph(int __x0);
  
  int __builtin_islower(int __x0);
  
  int __builtin_isprint(int __x0);
  
  int __builtin_ispunct(int __x0);
  
  int __builtin_isspace(int __x0);
  
  int __builtin_isupper(int __x0);
  
  int __builtin_isxdigit(int __x0);
  
  long __builtin_labs(long __x0);
  
  double __builtin_ldexp(double __x0, int __x1);
  
  float __builtin_ldexpf(float __x0, int __x1);
  
  long double __builtin_ldexpl(long double __x0, int __x1);
  
  double __builtin_lgamma(double __x0);
  
  float __builtin_lgammaf(float __x0);
  
  long double __builtin_lgammal(long double __x0);
  
  long long __builtin_llabs(long long __x0);
  
  long long __builtin_llrint(double __x0);
  
  long long __builtin_llrintf(float __x0);
  
  long long __builtin_llrintl(long double __x0);
  
  long long __builtin_llround(double __x0);
  
  long long __builtin_llroundf(float __x0);
  
  long long __builtin_llroundl(long double __x0);
  
  double __builtin_log(double __x0);
  
  double __builtin_log10(double __x0);
  
  float __builtin_log10f(float __x0);
  
  long double __builtin_log10l(long double __x0);
  
  double __builtin_log1p(double __x0);
  
  float __builtin_log1pf(float __x0);
  
  long double __builtin_log1pl(long double __x0);
  
  double __builtin_log2(double __x0);
  
  float __builtin_log2f(float __x0);
  
  long double __builtin_log2l(long double __x0);
  
  double __builtin_logb(double __x0);
  
  float __builtin_logbf(float __x0);
  
  long double __builtin_logbl(long double __x0);
  
  float __builtin_logf(float __x0);
  
  long double __builtin_logl(long double __x0);
  
  long __builtin_lrint(double __x0);
  
  long __builtin_lrintf(float __x0);
  
  long __builtin_lrintl(long double __x0);
  
  long __builtin_lround(double __x0);
  
  long __builtin_lroundf(float __x0);
  
  long __builtin_lroundl(long double __x0);
  
  void *__builtin_malloc(unsigned int __x0);
  
  void *__builtin_memchr(void const *__x0, int __x1, unsigned int __x2);
  
  int __builtin_memcmp(void const *__x0, void const *__x1, unsigned int __x2);
  
  void *__builtin_memcpy(void *__x0, void const *__x1, unsigned int __x2);
  
  void *__builtin_mempcpy(void *__x0, void const *__x1, unsigned int __x2);
  
  void *__builtin_memset(void *__x0, int __x1, unsigned int __x2);
  
  double __builtin_modf(double __x0, double *__x1);
  
  float __builtin_modff(float __x0, float *__x1);
  
  long double __builtin_modfl(long double __x0, long double *__x1);
  
  double __builtin_nan(char const *__x0);
  
  float __builtin_nanf(char const *__x0);
  
  long double __builtin_nanl(char const *__x0);
  
  double __builtin_nans(char const *__x0);
  
  float __builtin_nansf(char const *__x0);
  
  long double __builtin_nansl(char const *__x0);
  
  double __builtin_nearbyint(double __x0);
  
  float __builtin_nearbyintf(float __x0);
  
  long double __builtin_nearbyintl(long double __x0);
  
  __builtin_va_list __builtin_next_arg(void);
  
  double __builtin_nextafter(double __x0, double __x1);
  
  float __builtin_nextafterf(float __x0, float __x1);
  
  long double __builtin_nextafterl(long double __x0, long double __x1);
  
  double __builtin_nexttoward(double __x0, long double __x1);
  
  float __builtin_nexttowardf(float __x0, long double __x1);
  
  long double __builtin_nexttowardl(long double __x0, long double __x1);
  
  unsigned int __builtin_object_size(void *__x0, int __x1);
  
  unsigned int __builtin_offsetof(unsigned int __x0);
  
  int __builtin_parity(unsigned int __x0);
  
  int __builtin_parityl(unsigned long __x0);
  
  int __builtin_parityll(unsigned long long __x0);
  
  double __builtin_pow(double __x0, double __x1);
  
  float __builtin_powf(float __x0, float __x1);
  
  double __builtin_powi(double __x0, int __x1);
  
  float __builtin_powif(float __x0, int __x1);
  
  long double __builtin_powil(long double __x0, int __x1);
  
  long double __builtin_powl(long double __x0, long double __x1);
  
  void __builtin_prefetch(void const *__x0 , ...);
  
  int __builtin_printf(char const *__x0 , ...);
  
  int __builtin_putchar(int __x0);
  
  int __builtin_puts(char const *__x0);
  
  void *__builtin_realloc(void *__x0, unsigned int __x1);
  
  double __builtin_remainder(double __x0, double __x1);
  
  float __builtin_remainderf(float __x0, float __x1);
  
  long double __builtin_remainderl(long double __x0, long double __x1);
  
  double __builtin_remquo(double __x0, double __x1, int *__x2);
  
  float __builtin_remquof(float __x0, float __x1, int *__x2);
  
  long double __builtin_remquol(long double __x0, long double __x1, int *__x2);
  
  void __builtin_return(void const *__x0);
  
  void *__builtin_return_address(unsigned int __x0);
  
  double __builtin_rint(double __x0);
  
  float __builtin_rintf(float __x0);
  
  long double __builtin_rintl(long double __x0);
  
  double __builtin_round(double __x0);
  
  float __builtin_roundf(float __x0);
  
  long double __builtin_roundl(long double __x0);
  
  double __builtin_scalbln(double __x0, long __x1);
  
  float __builtin_scalblnf(float __x0, long __x1);
  
  long double __builtin_scalblnl(long double __x0, long __x1);
  
  double __builtin_scalbn(double __x0, int __x1);
  
  float __builtin_scalbnf(float __x0, int __x1);
  
  long double __builtin_scalbnl(long double __x0, int __x1);
  
  int __builtin_scanf(char const *__x0 , ...);
  
  double __builtin_sin(double __x0);
  
  float __builtin_sinf(float __x0);
  
  double __builtin_sinh(double __x0);
  
  float __builtin_sinhf(float __x0);
  
  long double __builtin_sinhl(long double __x0);
  
  long double __builtin_sinl(long double __x0);
  
  int __builtin_snprintf(char *__x0, unsigned int __x1, char const *__x2 , ...);
  
  int __builtin_sprintf(char *__x0, char const *__x1 , ...);
  
  double __builtin_sqrt(double __x0);
  
  float __builtin_sqrtf(float __x0);
  
  long double __builtin_sqrtl(long double __x0);
  
  int __builtin_sscanf(char const *__x0, char const *__x1 , ...);
  
  void __builtin_stdarg_start(__builtin_va_list __x0);
  
  char *__builtin_stpcpy(char *__x0, char const *__x1);
  
  char *__builtin_strcat(char *__x0, char const *__x1);
  
  char *__builtin_strchr(char *__x0, int __x1);
  
  int __builtin_strcmp(char const *__x0, char const *__x1);
  
  char *__builtin_strcpy(char *__x0, char const *__x1);
  
  unsigned int __builtin_strcspn(char const *__x0, char const *__x1);
  
  unsigned int __builtin_strlen(char const *__x0);
  
  char *__builtin_strncat(char *__x0, char const *__x1, unsigned int __x2);
  
  int __builtin_strncmp(char const *__x0, char const *__x1, unsigned int __x2);
  
  char *__builtin_strncpy(char *__x0, char const *__x1, unsigned int __x2);
  
  char *__builtin_strpbrk(char const *__x0, char const *__x1);
  
  char *__builtin_strrchr(char const *__x0, int __x1);
  
  unsigned int __builtin_strspn(char const *__x0, char const *__x1);
  
  char *__builtin_strstr(char const *__x0, char const *__x1);
  
  double __builtin_tan(double __x0);
  
  float __builtin_tanf(float __x0);
  
  double __builtin_tanh(double __x0);
  
  float __builtin_tanhf(float __x0);
  
  long double __builtin_tanhl(long double __x0);
  
  long double __builtin_tanl(long double __x0);
  
  double __builtin_tgamma(double __x0);
  
  float __builtin_tgammaf(float __x0);
  
  long double __builtin_tgammal(long double __x0);
  
  int __builtin_tolower(int __x0);
  
  int __builtin_toupper(int __x0);
  
  double __builtin_trunc(double __x0);
  
  float __builtin_truncf(float __x0);
  
  long double __builtin_truncl(long double __x0);
  
  int __builtin_types_compatible_p(unsigned int __x0, unsigned int __x1);
  
  void __builtin_unreachable(void);
  
  void __builtin_va_arg(__builtin_va_list __x0, unsigned int __x1, void *__x2);
  
  void __builtin_va_copy(__builtin_va_list __x0, __builtin_va_list __x1);
  
  void __builtin_va_end(__builtin_va_list __x0);
  
  void __builtin_va_start(__builtin_va_list __x0);
  
  void __builtin_varargs_start(__builtin_va_list __x0);
  
  int __builtin_vfprintf(void *__x0, char const *__x1, __builtin_va_list __x2);
  
  int __builtin_vfscanf(void *__x0, char const *__x1, __builtin_va_list __x2);
  
  int __builtin_vprintf(char const *__x0, __builtin_va_list __x1);
  
  int __builtin_vscanf(char const *__x0, __builtin_va_list __x1);
  
  int __builtin_vsnprintf(char *__x0, unsigned int __x1, char const *__x2,
                          __builtin_va_list __x3);
  
  int __builtin_vsprintf(char *__x0, char const *__x1, __builtin_va_list __x2);
  
  int __builtin_vsscanf(char const *__x0, char const *__x1,
                        __builtin_va_list __x2);
  
  short __sync_add_and_fetch_int16_t(short volatile *__x0, short __x1 , ...);
  
  int __sync_add_and_fetch_int32_t(int volatile *__x0, int __x1 , ...);
  
  long long __sync_add_and_fetch_int64_t(long long volatile *__x0,
                                         long long __x1 , ...);
  
  signed char __sync_add_and_fetch_int8_t(signed char volatile *__x0,
                                          signed char __x1 , ...);
  
  unsigned short __sync_add_and_fetch_uint16_t(unsigned short volatile *__x0,
                                               unsigned short __x1 , ...);
  
  unsigned int __sync_add_and_fetch_uint32_t(unsigned int volatile *__x0,
                                             unsigned int __x1 , ...);
  
  unsigned long long __sync_add_and_fetch_uint64_t(unsigned long long volatile *__x0,
                                                   unsigned long long __x1
                                                   , ...);
  
  unsigned char __sync_add_and_fetch_uint8_t(unsigned char volatile *__x0,
                                             unsigned char __x1 , ...);
  
  short __sync_and_and_fetch_int16_t(short volatile *__x0, short __x1 , ...);
  
  int __sync_and_and_fetch_int32_t(int volatile *__x0, int __x1 , ...);
  
  long long __sync_and_and_fetch_int64_t(long long volatile *__x0,
                                         long long __x1 , ...);
  
  signed char __sync_and_and_fetch_int8_t(signed char volatile *__x0,
                                          signed char __x1 , ...);
  
  unsigned short __sync_and_and_fetch_uint16_t(unsigned short volatile *__x0,
                                               unsigned short __x1 , ...);
  
  unsigned int __sync_and_and_fetch_uint32_t(unsigned int volatile *__x0,
                                             unsigned int __x1 , ...);
  
  unsigned long long __sync_and_and_fetch_uint64_t(unsigned long long volatile *__x0,
                                                   unsigned long long __x1
                                                   , ...);
  
  unsigned char __sync_and_and_fetch_uint8_t(unsigned char volatile *__x0,
                                             unsigned char __x1 , ...);
  
  int __sync_bool_compare_and_swap_int16_t(short volatile *__x0, short __x1,
                                           short __x2 , ...);
  
  int __sync_bool_compare_and_swap_int32_t(int volatile *__x0, int __x1,
                                           int __x2 , ...);
  
  int __sync_bool_compare_and_swap_int64_t(long long volatile *__x0,
                                           long long __x1, long long __x2 , ...);
  
  int __sync_bool_compare_and_swap_int8_t(signed char volatile *__x0,
                                          signed char __x1, signed char __x2
                                          , ...);
  
  int __sync_bool_compare_and_swap_uint16_t(unsigned short volatile *__x0,
                                            unsigned short __x1,
                                            unsigned short __x2 , ...);
  
  int __sync_bool_compare_and_swap_uint32_t(unsigned int volatile *__x0,
                                            unsigned int __x1,
                                            unsigned int __x2 , ...);
  
  int __sync_bool_compare_and_swap_uint64_t(unsigned long long volatile *__x0,
                                            unsigned long long __x1,
                                            unsigned long long __x2 , ...);
  
  int __sync_bool_compare_and_swap_uint8_t(unsigned char volatile *__x0,
                                           unsigned char __x1,
                                           unsigned char __x2 , ...);
  
  short __sync_fetch_and_add_int16_t(short volatile *__x0, short __x1 , ...);
  
  int __sync_fetch_and_add_int32_t(int volatile *__x0, int __x1 , ...);
  
  long long __sync_fetch_and_add_int64_t(long long volatile *__x0,
                                         long long __x1 , ...);
  
  signed char __sync_fetch_and_add_int8_t(signed char volatile *__x0,
                                          signed char __x1 , ...);
  
  unsigned short __sync_fetch_and_add_uint16_t(unsigned short volatile *__x0,
                                               unsigned short __x1 , ...);
  
  unsigned int __sync_fetch_and_add_uint32_t(unsigned int volatile *__x0,
                                             unsigned int __x1 , ...);
  
  unsigned long long __sync_fetch_and_add_uint64_t(unsigned long long volatile *__x0,
                                                   unsigned long long __x1
                                                   , ...);
  
  unsigned char __sync_fetch_and_add_uint8_t(unsigned char volatile *__x0,
                                             unsigned char __x1 , ...);
  
  short __sync_fetch_and_and_int16_t(short volatile *__x0, short __x1 , ...);
  
  int __sync_fetch_and_and_int32_t(int volatile *__x0, int __x1 , ...);
  
  long long __sync_fetch_and_and_int64_t(long long volatile *__x0,
                                         long long __x1 , ...);
  
  signed char __sync_fetch_and_and_int8_t(signed char volatile *__x0,
                                          signed char __x1 , ...);
  
  unsigned short __sync_fetch_and_and_uint16_t(unsigned short volatile *__x0,
                                               unsigned short __x1 , ...);
  
  unsigned int __sync_fetch_and_and_uint32_t(unsigned int volatile *__x0,
                                             unsigned int __x1 , ...);
  
  unsigned long long __sync_fetch_and_and_uint64_t(unsigned long long volatile *__x0,
                                                   unsigned long long __x1
                                                   , ...);
  
  unsigned char __sync_fetch_and_and_uint8_t(unsigned char volatile *__x0,
                                             unsigned char __x1 , ...);
  
  short __sync_fetch_and_nand_int16_t(short volatile *__x0, short __x1 , ...);
  
  int __sync_fetch_and_nand_int32_t(int volatile *__x0, int __x1 , ...);
  
  long long __sync_fetch_and_nand_int64_t(long long volatile *__x0,
                                          long long __x1 , ...);
  
  signed char __sync_fetch_and_nand_int8_t(signed char volatile *__x0,
                                           signed char __x1 , ...);
  
  unsigned short __sync_fetch_and_nand_uint16_t(unsigned short volatile *__x0,
                                                unsigned short __x1 , ...);
  
  unsigned int __sync_fetch_and_nand_uint32_t(unsigned int volatile *__x0,
                                              unsigned int __x1 , ...);
  
  unsigned long long __sync_fetch_and_nand_uint64_t(unsigned long long volatile *__x0,
                                                    unsigned long long __x1
                                                    , ...);
  
  unsigned char __sync_fetch_and_nand_uint8_t(unsigned char volatile *__x0,
                                              unsigned char __x1 , ...);
  
  short __sync_fetch_and_or_int16_t(short volatile *__x0, short __x1 , ...);
  
  int __sync_fetch_and_or_int32_t(int volatile *__x0, int __x1 , ...);
  
  long long __sync_fetch_and_or_int64_t(long long volatile *__x0,
                                        long long __x1 , ...);
  
  signed char __sync_fetch_and_or_int8_t(signed char volatile *__x0,
                                         signed char __x1 , ...);
  
  unsigned short __sync_fetch_and_or_uint16_t(unsigned short volatile *__x0,
                                              unsigned short __x1 , ...);
  
  unsigned int __sync_fetch_and_or_uint32_t(unsigned int volatile *__x0,
                                            unsigned int __x1 , ...);
  
  unsigned long long __sync_fetch_and_or_uint64_t(unsigned long long volatile *__x0,
                                                  unsigned long long __x1 , ...);
  
  unsigned char __sync_fetch_and_or_uint8_t(unsigned char volatile *__x0,
                                            unsigned char __x1 , ...);
  
  short __sync_fetch_and_sub_int16_t(short volatile *__x0, short __x1 , ...);
  
  int __sync_fetch_and_sub_int32_t(int volatile *__x0, int __x1 , ...);
  
  long long __sync_fetch_and_sub_int64_t(long long volatile *__x0,
                                         long long __x1 , ...);
  
  signed char __sync_fetch_and_sub_int8_t(signed char volatile *__x0,
                                          signed char __x1 , ...);
  
  unsigned short __sync_fetch_and_sub_uint16_t(unsigned short volatile *__x0,
                                               unsigned short __x1 , ...);
  
  unsigned int __sync_fetch_and_sub_uint32_t(unsigned int volatile *__x0,
                                             unsigned int __x1 , ...);
  
  unsigned long long __sync_fetch_and_sub_uint64_t(unsigned long long volatile *__x0,
                                                   unsigned long long __x1
                                                   , ...);
  
  unsigned char __sync_fetch_and_sub_uint8_t(unsigned char volatile *__x0,
                                             unsigned char __x1 , ...);
  
  short __sync_fetch_and_xor_int16_t(short volatile *__x0, short __x1 , ...);
  
  int __sync_fetch_and_xor_int32_t(int volatile *__x0, int __x1 , ...);
  
  long long __sync_fetch_and_xor_int64_t(long long volatile *__x0,
                                         long long __x1 , ...);
  
  signed char __sync_fetch_and_xor_int8_t(signed char volatile *__x0,
                                          signed char __x1 , ...);
  
  unsigned short __sync_fetch_and_xor_uint16_t(unsigned short volatile *__x0,
                                               unsigned short __x1 , ...);
  
  unsigned int __sync_fetch_and_xor_uint32_t(unsigned int volatile *__x0,
                                             unsigned int __x1 , ...);
  
  unsigned long long __sync_fetch_and_xor_uint64_t(unsigned long long volatile *__x0,
                                                   unsigned long long __x1
                                                   , ...);
  
  unsigned char __sync_fetch_and_xor_uint8_t(unsigned char volatile *__x0,
                                             unsigned char __x1 , ...);
  
  void __sync_lock_release_int16_t(short volatile *__x0 , ...);
  
  void __sync_lock_release_int32_t(int volatile *__x0 , ...);
  
  void __sync_lock_release_int64_t(long long volatile *__x0 , ...);
  
  void __sync_lock_release_int8_t(signed char volatile *__x0 , ...);
  
  void __sync_lock_release_uint16_t(unsigned short volatile *__x0 , ...);
  
  void __sync_lock_release_uint32_t(unsigned int volatile *__x0 , ...);
  
  void __sync_lock_release_uint64_t(unsigned long long volatile *__x0 , ...);
  
  void __sync_lock_release_uint8_t(unsigned char volatile *__x0 , ...);
  
  short __sync_lock_test_and_set_int16_t(short volatile *__x0, short __x1 , ...);
  
  int __sync_lock_test_and_set_int32_t(int volatile *__x0, int __x1 , ...);
  
  long long __sync_lock_test_and_set_int64_t(long long volatile *__x0,
                                             long long __x1 , ...);
  
  signed char __sync_lock_test_and_set_int8_t(signed char volatile *__x0,
                                              signed char __x1 , ...);
  
  unsigned short __sync_lock_test_and_set_uint16_t(unsigned short volatile *__x0,
                                                   unsigned short __x1 , ...);
  
  unsigned int __sync_lock_test_and_set_uint32_t(unsigned int volatile *__x0,
                                                 unsigned int __x1 , ...);
  
  unsigned long long __sync_lock_test_and_set_uint64_t(unsigned long long volatile *__x0,
                                                       unsigned long long __x1
                                                       , ...);
  
  unsigned char __sync_lock_test_and_set_uint8_t(unsigned char volatile *__x0,
                                                 unsigned char __x1 , ...);
  
  short __sync_nand_and_fetch_int16_t(short volatile *__x0, short __x1 , ...);
  
  int __sync_nand_and_fetch_int32_t(int volatile *__x0, int __x1 , ...);
  
  long long __sync_nand_and_fetch_int64_t(long long volatile *__x0,
                                          long long __x1 , ...);
  
  signed char __sync_nand_and_fetch_int8_t(signed char volatile *__x0,
                                           signed char __x1 , ...);
  
  unsigned short __sync_nand_and_fetch_uint16_t(unsigned short volatile *__x0,
                                                unsigned short __x1 , ...);
  
  unsigned int __sync_nand_and_fetch_uint32_t(unsigned int volatile *__x0,
                                              unsigned int __x1 , ...);
  
  unsigned long long __sync_nand_and_fetch_uint64_t(unsigned long long volatile *__x0,
                                                    unsigned long long __x1
                                                    , ...);
  
  unsigned char __sync_nand_and_fetch_uint8_t(unsigned char volatile *__x0,
                                              unsigned char __x1 , ...);
  
  short __sync_or_and_fetch_int16_t(short volatile *__x0, short __x1 , ...);
  
  int __sync_or_and_fetch_int32_t(int volatile *__x0, int __x1 , ...);
  
  long long __sync_or_and_fetch_int64_t(long long volatile *__x0,
                                        long long __x1 , ...);
  
  signed char __sync_or_and_fetch_int8_t(signed char volatile *__x0,
                                         signed char __x1 , ...);
  
  unsigned short __sync_or_and_fetch_uint16_t(unsigned short volatile *__x0,
                                              unsigned short __x1 , ...);
  
  unsigned int __sync_or_and_fetch_uint32_t(unsigned int volatile *__x0,
                                            unsigned int __x1 , ...);
  
  unsigned long long __sync_or_and_fetch_uint64_t(unsigned long long volatile *__x0,
                                                  unsigned long long __x1 , ...);
  
  unsigned char __sync_or_and_fetch_uint8_t(unsigned char volatile *__x0,
                                            unsigned char __x1 , ...);
  
  short __sync_sub_and_fetch_int16_t(short volatile *__x0, short __x1 , ...);
  
  int __sync_sub_and_fetch_int32_t(int volatile *__x0, int __x1 , ...);
  
  long long __sync_sub_and_fetch_int64_t(long long volatile *__x0,
                                         long long __x1 , ...);
  
  signed char __sync_sub_and_fetch_int8_t(signed char volatile *__x0,
                                          signed char __x1 , ...);
  
  unsigned short __sync_sub_and_fetch_uint16_t(unsigned short volatile *__x0,
                                               unsigned short __x1 , ...);
  
  unsigned int __sync_sub_and_fetch_uint32_t(unsigned int volatile *__x0,
                                             unsigned int __x1 , ...);
  
  unsigned long long __sync_sub_and_fetch_uint64_t(unsigned long long volatile *__x0,
                                                   unsigned long long __x1
                                                   , ...);
  
  unsigned char __sync_sub_and_fetch_uint8_t(unsigned char volatile *__x0,
                                             unsigned char __x1 , ...);
  
  short __sync_val_compare_and_swap_int16_t(short volatile *__x0, short __x1,
                                            short __x2 , ...);
  
  int __sync_val_compare_and_swap_int32_t(int volatile *__x0, int __x1,
                                          int __x2 , ...);
  
  long long __sync_val_compare_and_swap_int64_t(long long volatile *__x0,
                                                long long __x1, long long __x2
                                                , ...);
  
  signed char __sync_val_compare_and_swap_int8_t(signed char volatile *__x0,
                                                 signed char __x1,
                                                 signed char __x2 , ...);
  
  unsigned short __sync_val_compare_and_swap_uint16_t(unsigned short volatile *__x0,
                                                      unsigned short __x1,
                                                      unsigned short __x2 , ...);
  
  unsigned int __sync_val_compare_and_swap_uint32_t(unsigned int volatile *__x0,
                                                    unsigned int __x1,
                                                    unsigned int __x2 , ...);
  
  unsigned long long __sync_val_compare_and_swap_uint64_t(unsigned long long volatile *__x0,
                                                          unsigned long long __x1,
                                                          unsigned long long __x2
                                                          , ...);
  
  unsigned char __sync_val_compare_and_swap_uint8_t(unsigned char volatile *__x0,
                                                    unsigned char __x1,
                                                    unsigned char __x2 , ...);
  
  short __sync_xor_and_fetch_int16_t(short volatile *__x0, short __x1 , ...);
  
  int __sync_xor_and_fetch_int32_t(int volatile *__x0, int __x1 , ...);
  
  long long __sync_xor_and_fetch_int64_t(long long volatile *__x0,
                                         long long __x1 , ...);
  
  signed char __sync_xor_and_fetch_int8_t(signed char volatile *__x0,
                                          signed char __x1 , ...);
  
  unsigned short __sync_xor_and_fetch_uint16_t(unsigned short volatile *__x0,
                                               unsigned short __x1 , ...);
  
  unsigned int __sync_xor_and_fetch_uint32_t(unsigned int volatile *__x0,
                                             unsigned int __x1 , ...);
  
  unsigned long long __sync_xor_and_fetch_uint64_t(unsigned long long volatile *__x0,
                                                   unsigned long long __x1
                                                   , ...);
  
  unsigned char __sync_xor_and_fetch_uint8_t(unsigned char volatile *__x0,
                                             unsigned char __x1 , ...);
  
  int max(int i, int j)
  {
    /* Locals: tmp */
    int tmp;
    ;
    if (i >= j) {
      tmp = i;
    }
    else {
      tmp = j;
    }
    return tmp;
  }
[kernel:file:annotation] Marking properties
/* Generated by Frama-C */
/*@ ensures /* ip:1 */\result ≥ \old(i);
    ensures /* ip:2 */\result ≥ \old(j);
    ensures /* ip:3 */\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 {