[kernel] Update tests

tests/syntax/oracle/check_builtin_bts1440.res.oracle

@@ -2,6 +2,8 @@
 [kernel:file:print-one] 
   result of parsing tests/syntax/check_builtin_bts1440.i:
   /* Generated by Frama-C */
+  void __builtin__Exit(int);
+  
   int __builtin___fprintf_chk(void *, int, char const * , ...);
   
   void *__builtin___memcpy_chk(void *, void const *, unsigned int, unsigned int);
@@ -43,10 +45,18 @@
   int __builtin___vsprintf_chk(char *, int, unsigned int, char const *,
                                __builtin_va_list);
   
+  int __builtin_abs(int);
+  
   double __builtin_acos(double);
   
   float __builtin_acosf(float);
   
+  double __builtin_acosh(double);
+  
+  float __builtin_acoshf(float);
+  
+  long double __builtin_acoshl(long double);
+  
   long double __builtin_acosl(long double);
   
   void *__builtin_alloca(unsigned int);
@@ -55,6 +65,12 @@
   
   float __builtin_asinf(float);
   
+  double __builtin_asinh(double);
+  
+  float __builtin_asinhf(float);
+  
+  long double __builtin_asinhl(long double);
+  
   long double __builtin_asinl(long double);
   
   double __builtin_atan(double);
@@ -67,6 +83,12 @@
   
   float __builtin_atanf(float);
   
+  double __builtin_atanh(double);
+  
+  float __builtin_atanhf(float);
+  
+  long double __builtin_atanhl(long double);
+  
   long double __builtin_atanl(long double);
   
   unsigned short __builtin_bswap16(unsigned short);
@@ -75,6 +97,14 @@
   
   unsigned long long __builtin_bswap64(unsigned long long);
   
+  void *__builtin_calloc(unsigned int, unsigned int);
+  
+  double __builtin_cbrt(double);
+  
+  float __builtin_cbrtf(float);
+  
+  long double __builtin_cbrtl(long double);
+  
   double __builtin_ceil(double);
   
   float __builtin_ceilf(float);
@@ -83,6 +113,12 @@
   
   int __builtin_constant_p(int);
   
+  double __builtin_copysign(double, double);
+  
+  float __builtin_copysignf(float, float);
+  
+  long double __builtin_copysignl(long double, long double);
+  
   double __builtin_cos(double);
   
   float __builtin_cosf(float);
@@ -95,20 +131,52 @@
   
   long double __builtin_cosl(long double);
   
+  double __builtin_erf(double);
+  
+  double __builtin_erfc(double);
+  
+  float __builtin_erfcf(float);
+  
+  long double __builtin_erfcl(long double);
+  
+  float __builtin_erff(float);
+  
+  long double __builtin_erfl(long double);
+  
+  void __builtin_exit(int);
+  
   double __builtin_exp(double);
   
+  double __builtin_exp2(double);
+  
+  float __builtin_exp2f(float);
+  
+  long double __builtin_exp2l(long double);
+  
   long __builtin_expect(long, long);
   
   float __builtin_expf(float);
   
   long double __builtin_expl(long double);
   
+  double __builtin_expm1(double);
+  
+  float __builtin_expm1f(float);
+  
+  long double __builtin_expm1l(long double);
+  
   double __builtin_fabs(double);
   
   float __builtin_fabsf(float);
   
   long double __builtin_fabsl(long double);
   
+  double __builtin_fdim(double, double);
+  
+  float __builtin_fdimf(float, float);
+  
+  long double __builtin_fdiml(long double, long double);
+  
   int __builtin_ffs(unsigned int);
   
   int __builtin_ffsl(unsigned long);
@@ -121,44 +189,128 @@
   
   long double __builtin_floorl(long double);
   
+  double __builtin_fma(double, double, double);
+  
+  float __builtin_fmaf(float, float, float);
+  
+  long double __builtin_fmal(long double, long double, long double);
+  
+  double __builtin_fmax(double, double);
+  
+  float __builtin_fmaxf(float, float);
+  
+  long double __builtin_fmaxl(long double, long double);
+  
+  double __builtin_fmin(double, double);
+  
+  float __builtin_fminf(float, float);
+  
+  long double __builtin_fminl(long double, long double);
+  
   double __builtin_fmod(double);
   
   float __builtin_fmodf(float);
   
   long double __builtin_fmodl(long double);
   
+  int __builtin_fprintf(void *, char const * , ...);
+  
+  int __builtin_fputs(char const *, void *);
+  
   void *__builtin_frame_address(unsigned int);
   
+  void __builtin_free(void *);
+  
   double __builtin_frexp(double, int *);
   
   float __builtin_frexpf(float, int *);
   
   long double __builtin_frexpl(long double, int *);
   
+  int __builtin_fscanf(void *, char const * , ...);
+  
   double __builtin_huge_val(void);
   
   float __builtin_huge_valf(void);
   
   long double __builtin_huge_vall(void);
   
+  double __builtin_hypot(double, double);
+  
+  float __builtin_hypotf(float, float);
+  
+  long double __builtin_hypotl(long double, long double);
+  
   void __builtin_ia32_lfence(void);
   
   void __builtin_ia32_mfence(void);
   
   void __builtin_ia32_sfence(void);
   
+  double __builtin_ilogb(double);
+  
+  float __builtin_ilogbf(float);
+  
+  long double __builtin_ilogbl(long double);
+  
   double __builtin_inf(void);
   
   float __builtin_inff(void);
   
   long double __builtin_infl(void);
   
+  int __builtin_isalnum(int);
+  
+  int __builtin_isalpha(int);
+  
+  int __builtin_isblank(int);
+  
+  int __builtin_iscntrl(int);
+  
+  int __builtin_isdigit(int);
+  
+  int __builtin_isgraph(int);
+  
+  int __builtin_islower(int);
+  
+  int __builtin_isprint(int);
+  
+  int __builtin_ispunct(int);
+  
+  int __builtin_isspace(int);
+  
+  int __builtin_isupper(int);
+  
+  int __builtin_isxdigit(int);
+  
+  long __builtin_labs(long);
+  
   double __builtin_ldexp(double, int);
   
   float __builtin_ldexpf(float, int);
   
   long double __builtin_ldexpl(long double, int);
   
+  double __builtin_lgamma(double);
+  
+  float __builtin_lgammaf(float);
+  
+  long double __builtin_lgammal(long double);
+  
+  long long __builtin_llabs(long long);
+  
+  long long __builtin_llrint(double);
+  
+  long long __builtin_llrintf(float);
+  
+  long long __builtin_llrintl(long double);
+  
+  long long __builtin_llround(double);
+  
+  long long __builtin_llroundf(float);
+  
+  long long __builtin_llroundl(long double);
+  
   double __builtin_log(double);
   
   double __builtin_log10(double);
@@ -167,15 +319,53 @@
   
   long double __builtin_log10l(long double);
   
+  double __builtin_log1p(double);
+  
+  float __builtin_log1pf(float);
+  
+  long double __builtin_log1pl(long double);
+  
+  double __builtin_log2(double);
+  
+  float __builtin_log2f(float);
+  
+  long double __builtin_log2l(long double);
+  
+  double __builtin_logb(double);
+  
+  float __builtin_logbf(float);
+  
+  long double __builtin_logbl(long double);
+  
   float __builtin_logf(float);
   
   long double __builtin_logl(long double);
   
+  long __builtin_lrint(double);
+  
+  long __builtin_lrintf(float);
+  
+  long __builtin_lrintl(long double);
+  
+  long __builtin_lround(double);
+  
+  long __builtin_lroundf(float);
+  
+  long __builtin_lroundl(long double);
+  
+  void *__builtin_malloc(unsigned int);
+  
+  void *__builtin_memchr(void const *, int, unsigned int);
+  
+  int __builtin_memcmp(void const *, void const *, unsigned int);
+  
   void *__builtin_memcpy(void *, void const *, unsigned int);
   
   void *__builtin_mempcpy(void *, void const *, unsigned int);
   
-  void *__builtin_memset(void *, int, int);
+  void *__builtin_memset(void *, int, unsigned int);
+  
+  double __builtin_modf(double, double *);
   
   float __builtin_modff(float, float *);
   
@@ -193,8 +383,26 @@
   
   long double __builtin_nansl(char const *);
   
+  double __builtin_nearbyint(double);
+  
+  float __builtin_nearbyintf(float);
+  
+  long double __builtin_nearbyintl(long double);
+  
   __builtin_va_list __builtin_next_arg(void);
   
+  double __builtin_nextafter(double, double);
+  
+  float __builtin_nextafterf(float, float);
+  
+  long double __builtin_nextafterl(long double, long double);
+  
+  double __builtin_nexttoward(double, long double);
+  
+  float __builtin_nexttowardf(float, long double);
+  
+  long double __builtin_nexttowardl(long double, long double);
+  
   unsigned int __builtin_object_size(void *, int);
   
   unsigned int __builtin_offsetof(unsigned int);
@@ -205,18 +413,70 @@
   
   int __builtin_parityll(unsigned long long);
   
+  double __builtin_pow(double, double);
+  
+  float __builtin_powf(float, float);
+  
   double __builtin_powi(double, int);
   
   float __builtin_powif(float, int);
   
   long double __builtin_powil(long double, int);
   
+  long double __builtin_powl(long double, long double);
+  
   void __builtin_prefetch(void const * , ...);
   
+  int __builtin_printf(char const * , ...);
+  
+  int __builtin_putchar(int);
+  
+  int __builtin_puts(char const *);
+  
+  void *__builtin_realloc(void *, unsigned int);
+  
+  double __builtin_remainder(double, double);
+  
+  float __builtin_remainderf(float, float);
+  
+  long double __builtin_remainderl(long double, long double);
+  
+  double __builtin_remquo(double, double, int *);
+  
+  float __builtin_remquof(float, float, int *);
+  
+  long double __builtin_remquol(long double, long double, int *);
+  
   void __builtin_return(void const *);
   
   void *__builtin_return_address(unsigned int);
   
+  double __builtin_rint(double);
+  
+  float __builtin_rintf(float);
+  
+  long double __builtin_rintl(long double);
+  
+  double __builtin_round(double);
+  
+  float __builtin_roundf(float);
+  
+  long double __builtin_roundl(long double);
+  
+  double __builtin_scalbln(double, long);
+  
+  float __builtin_scalblnf(float, long);
+  
+  long double __builtin_scalblnl(long double, long);
+  
+  double __builtin_scalbn(double, int);
+  
+  float __builtin_scalbnf(float, int);
+  
+  long double __builtin_scalbnl(long double, int);
+  
+  int __builtin_scanf(char const * , ...);
+  
   double __builtin_sin(double);
   
   float __builtin_sinf(float);
@@ -229,16 +489,24 @@
   
   long double __builtin_sinl(long double);
   
+  int __builtin_snprintf(char *, unsigned int, char const * , ...);
+  
+  int __builtin_sprintf(char *, char const * , ...);
+  
   double __builtin_sqrt(double);
   
   float __builtin_sqrtf(float);
   
   long double __builtin_sqrtl(long double);
   
+  int __builtin_sscanf(char const *, char const * , ...);
+  
   void __builtin_stdarg_start(__builtin_va_list);
   
   char *__builtin_stpcpy(char *, char const *);
   
+  char *__builtin_strcat(char *, char const *);
+  
   char *__builtin_strchr(char *, int);
   
   int __builtin_strcmp(char const *, char const *);
@@ -247,6 +515,8 @@
   
   unsigned int __builtin_strcspn(char const *, char const *);
   
+  unsigned int __builtin_strlen(char const *);
+  
   char *__builtin_strncat(char *, char const *, unsigned int);
   
   int __builtin_strncmp(char const *, char const *, unsigned int);
@@ -255,8 +525,12 @@
   
   char *__builtin_strpbrk(char const *, char const *);
   
+  char *__builtin_strrchr(char const *, int);
+  
   unsigned int __builtin_strspn(char const *, char const *);
   
+  char *__builtin_strstr(char const *, char const *);
+  
   double __builtin_tan(double);
   
   float __builtin_tanf(float);
@@ -269,6 +543,22 @@
   
   long double __builtin_tanl(long double);
   
+  double __builtin_tgamma(double);
+  
+  float __builtin_tgammaf(float);
+  
+  long double __builtin_tgammal(long double);
+  
+  int __builtin_tolower(int);
+  
+  int __builtin_toupper(int);
+  
+  double __builtin_trunc(double);
+  
+  float __builtin_truncf(float);
+  
+  long double __builtin_truncl(long double);
+  
   int __builtin_types_compatible_p(unsigned int, unsigned int);
   
   void __builtin_unreachable(void);
@@ -283,6 +573,20 @@
   
   void __builtin_varargs_start(__builtin_va_list);
   
+  int __builtin_vfprintf(void *, char const *, __builtin_va_list);
+  
+  int __builtin_vfscanf(void *, char const *, __builtin_va_list);
+  
+  int __builtin_vprintf(char const *, __builtin_va_list);
+  
+  int __builtin_vscanf(char const *, __builtin_va_list);
+  
+  int __builtin_vsnprintf(char *, unsigned int, char const *, __builtin_va_list);
+  
+  int __builtin_vsprintf(char *, char const *, __builtin_va_list);
+  
+  int __builtin_vsscanf(char const *, char const *, __builtin_va_list);
+  
   short __sync_add_and_fetch_int16_t(short volatile *, short , ...);
   
   int __sync_add_and_fetch_int32_t(int volatile *, int , ...);