From 85bc2a666d1e83720eac8b8cc0ecaaf3d1bc23a6 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Thu, 5 Nov 2020 18:18:08 +0100
Subject: [PATCH] [kernel] Update tests
---
.../oracle/check_builtin_bts1440.res.oracle | 306 +++++++++++++++++-
1 file changed, 305 insertions(+), 1 deletion(-)
diff --git a/tests/syntax/oracle/check_builtin_bts1440.res.oracle b/tests/syntax/oracle/check_builtin_bts1440.res.oracle
index 091c7d8002d..510a8f2b3ab 100644
--- a/tests/syntax/oracle/check_builtin_bts1440.res.oracle
+++ b/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 , ...);
--
GitLab