diff --git a/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle index 77d342b3dd8113ce3c181cca5993138243e6bbe4..179380e42d59c545cf1035fe08e04769d45155c8 100644 --- a/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle +++ b/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle @@ -18,7 +18,7 @@ behavior bhv: requires c > 0; requires a ≤ 42; */ -void f(int const a, int, int c, void * const *__va_params) +void f(int const a, int __x1, int c, void * const *__va_params) /*@ ghost (int x) */; int main(void) diff --git a/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle b/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle index c028e9e151d91ac8f3d848668a9ead0863bef9f1..c747e92c44eae658143432e49fcd1574c0fb8988 100644 --- a/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle +++ b/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle @@ -17,7 +17,7 @@ behavior bhv: requires c > 0; requires a ≤ 42; */ -void f(int const a, int, int c, void * const *__va_params); +void f(int const a, int __x1, int c, void * const *__va_params); int main(void) { diff --git a/src/plugins/variadic/tests/declared/oracle/label.res.oracle b/src/plugins/variadic/tests/declared/oracle/label.res.oracle index 427868a9c76ae47b935ff087454c0ef2b589dc3d..2de09b271e78448da9d97031e7d05fce8608b3f8 100644 --- a/src/plugins/variadic/tests/declared/oracle/label.res.oracle +++ b/src/plugins/variadic/tests/declared/oracle/label.res.oracle @@ -13,7 +13,7 @@ __retres ∈ {0} /* Generated by Frama-C */ /*@ assigns \result; - assigns \result \from \nothing; */ + assigns \result \from __x0; */ int f(int, void * const *__va_params); int main(void) diff --git a/src/plugins/variadic/tests/declared/oracle/multi.res.oracle b/src/plugins/variadic/tests/declared/oracle/multi.res.oracle index adcbb2b04d43ce39487600c92e43c8f4c6d65a55..0cf3b24972f4204f3431dceb595d5c56b4b040a7 100644 --- a/src/plugins/variadic/tests/declared/oracle/multi.res.oracle +++ b/src/plugins/variadic/tests/declared/oracle/multi.res.oracle @@ -23,14 +23,14 @@ /* Generated by Frama-C */ /*@ assigns \result; - assigns \result \from a, c; + assigns \result \from a, __x1, c; behavior bhv1: requires c > 0; requires a ≤ 42; ensures \result > 0; */ -int f(int const a, int, int c, void * const *__va_params); +int f(int const a, int __x1, int c, void * const *__va_params); int call1(void) { diff --git a/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle index fa2e63b8a114173eac0d131f2fe7c203d8ef6592..afe3fe0a174a0b03f4b921571d02f921451a87cd 100644 --- a/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle +++ b/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle @@ -14,14 +14,14 @@ /* Generated by Frama-C */ /*@ assigns \result; - assigns \result \from a, c; + assigns \result \from a, __x1, c; behavior bhv: requires c > 0; requires a ≤ 42; ensures \result > 0; */ -int f(int const a, int, int c, void * const *__va_params) +int f(int const a, int __x1, int c, void * const *__va_params) /*@ ghost (int x) */; int main(void) diff --git a/src/plugins/variadic/tests/declared/oracle/simple.res.oracle b/src/plugins/variadic/tests/declared/oracle/simple.res.oracle index 9112e9470077a769eaa504faed32bb9cf3caf757..d1ed1eec99ada14fcdb114282bc3b17bf4a17dd1 100644 --- a/src/plugins/variadic/tests/declared/oracle/simple.res.oracle +++ b/src/plugins/variadic/tests/declared/oracle/simple.res.oracle @@ -13,14 +13,14 @@ /* Generated by Frama-C */ /*@ assigns \result; - assigns \result \from a, c; + assigns \result \from a, __x1, c; behavior bhv: requires c > 0; requires a ≤ 42; ensures \result > 0; */ -int f(int const a, int, int c, void * const *__va_params); +int f(int const a, int __x1, int c, void * const *__va_params); int main(void) { diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle index b647d40caefdab3371fc969f9c085857e3964a42..033244bd8fd3ea79f4f2712c84d403e0f8ceb97a 100644 --- a/tests/libc/oracle/fc_libc.1.res.oracle +++ b/tests/libc/oracle/fc_libc.1.res.oracle @@ -1565,7 +1565,7 @@ extern int execvp(char const *path, char * const *argv); /*@ ensures never_terminates: \false; assigns \nothing; */ -extern __attribute__((__noreturn__)) void _exit(int); +extern __attribute__((__noreturn__)) void _exit(int __x0); /*@ ensures result_ok_child_or_error: @@ -1635,7 +1635,7 @@ extern pid_t getppid(void); /*@ assigns \result; assigns \result \from \nothing; */ -extern pid_t getsid(pid_t); +extern pid_t getsid(pid_t __x0); /*@ assigns \result; assigns \result \from \nothing; */ @@ -7988,7 +7988,7 @@ extern size_t iconv(iconv_t cd, char ** restrict inbuf, /*@ ensures result_zero_or_neg: \result ≡ 0 ∨ \result ≡ -1; assigns __fc_errno; */ -extern int iconv_close(iconv_t); +extern int iconv_close(iconv_t __x0); /*@ assigns \result, __fc_errno; assigns \result \from *(tocode + (..)), *(fromcode + (..)); @@ -8293,16 +8293,16 @@ CODE prioritynames[13] = extern void closelog(void); /*@ assigns \nothing; */ -extern void openlog(char const *, int, int); +extern void openlog(char const *__x0, int __x1, int __x2); /*@ assigns \nothing; */ -extern int setlogmask(int); +extern int setlogmask(int __x0); /*@ assigns \nothing; */ -extern void syslog(int, char const *, void * const *__va_params); +extern void syslog(int __x0, char const *__x1, void * const *__va_params); /*@ assigns \nothing; */ -extern void vsyslog(int, char const *, va_list); +extern void vsyslog(int __x0, char const *__x1, va_list __x2); /*@ assigns \result; assigns \result \from which, who; */ diff --git a/tests/slicing/oracle/unravel-point.0.res.oracle b/tests/slicing/oracle/unravel-point.0.res.oracle index 892a13dfd9ace31ff1d20e9ea6bf2f8dbf31a767..3fda244140018eb16df637b2ed60a6af651656af 100644 --- a/tests/slicing/oracle/unravel-point.0.res.oracle +++ b/tests/slicing/oracle/unravel-point.0.res.oracle @@ -81,13 +81,13 @@ [eva] done for function main [from] ====== DISPLAYING CALLWISE DEPENDENCIES ====== [from] call to printf at tests/slicing/unravel-point.i:36 (by send1): - \result FROM \nothing + \result FROM __x1; "%d\n" [from] call to printf at tests/slicing/unravel-point.i:40 (by send2): - \result FROM \nothing + \result FROM __x1; "%d\n" [from] call to printf at tests/slicing/unravel-point.i:44 (by send3): - \result FROM \nothing + \result FROM __x1; "%d\n" [from] call to printf at tests/slicing/unravel-point.i:48 (by send4): - \result FROM \nothing + \result FROM __x1; "%d\n" [from] call to scanf at tests/slicing/unravel-point.i:59 (by main): input1 FROM \nothing \result FROM ANYTHING(origin:Unknown) diff --git a/tests/slicing/oracle/unravel-point.1.res.oracle b/tests/slicing/oracle/unravel-point.1.res.oracle index 1d4a3d5acbd379698c91599a347b835e0201ffb1..a890fa20e816504cc01ced6ece96931c5f5e85e7 100644 --- a/tests/slicing/oracle/unravel-point.1.res.oracle +++ b/tests/slicing/oracle/unravel-point.1.res.oracle @@ -81,13 +81,13 @@ [eva] done for function main [from] ====== DISPLAYING CALLWISE DEPENDENCIES ====== [from] call to printf at tests/slicing/unravel-point.i:36 (by send1): - \result FROM \nothing + \result FROM __x1; "%d\n" [from] call to printf at tests/slicing/unravel-point.i:40 (by send2): - \result FROM \nothing + \result FROM __x1; "%d\n" [from] call to printf at tests/slicing/unravel-point.i:44 (by send3): - \result FROM \nothing + \result FROM __x1; "%d\n" [from] call to printf at tests/slicing/unravel-point.i:48 (by send4): - \result FROM \nothing + \result FROM __x1; "%d\n" [from] call to scanf at tests/slicing/unravel-point.i:59 (by main): input1 FROM \nothing \result FROM ANYTHING(origin:Unknown) diff --git a/tests/slicing/oracle/unravel-point.2.res.oracle b/tests/slicing/oracle/unravel-point.2.res.oracle index 695f510a073771b8f3c202fd21a709f25b5ce3c3..b9b817c3f6cb242ba295dced6a0482662923ee03 100644 --- a/tests/slicing/oracle/unravel-point.2.res.oracle +++ b/tests/slicing/oracle/unravel-point.2.res.oracle @@ -81,13 +81,13 @@ [eva] done for function main [from] ====== DISPLAYING CALLWISE DEPENDENCIES ====== [from] call to printf at tests/slicing/unravel-point.i:36 (by send1): - \result FROM \nothing + \result FROM __x1; "%d\n" [from] call to printf at tests/slicing/unravel-point.i:40 (by send2): - \result FROM \nothing + \result FROM __x1; "%d\n" [from] call to printf at tests/slicing/unravel-point.i:44 (by send3): - \result FROM \nothing + \result FROM __x1; "%d\n" [from] call to printf at tests/slicing/unravel-point.i:48 (by send4): - \result FROM \nothing + \result FROM __x1; "%d\n" [from] call to scanf at tests/slicing/unravel-point.i:59 (by main): input1 FROM \nothing \result FROM ANYTHING(origin:Unknown) diff --git a/tests/slicing/oracle/unravel-point.3.res.oracle b/tests/slicing/oracle/unravel-point.3.res.oracle index 4f09e01392e10705ddaa3beab3de59944e7d8ea4..97ac7856428adf3214cbe7b0dbc37de08d8b6c8f 100644 --- a/tests/slicing/oracle/unravel-point.3.res.oracle +++ b/tests/slicing/oracle/unravel-point.3.res.oracle @@ -81,13 +81,13 @@ [eva] done for function main [from] ====== DISPLAYING CALLWISE DEPENDENCIES ====== [from] call to printf at tests/slicing/unravel-point.i:36 (by send1): - \result FROM \nothing + \result FROM __x1; "%d\n" [from] call to printf at tests/slicing/unravel-point.i:40 (by send2): - \result FROM \nothing + \result FROM __x1; "%d\n" [from] call to printf at tests/slicing/unravel-point.i:44 (by send3): - \result FROM \nothing + \result FROM __x1; "%d\n" [from] call to printf at tests/slicing/unravel-point.i:48 (by send4): - \result FROM \nothing + \result FROM __x1; "%d\n" [from] call to scanf at tests/slicing/unravel-point.i:59 (by main): input1 FROM \nothing \result FROM ANYTHING(origin:Unknown) diff --git a/tests/slicing/oracle/unravel-point.4.res.oracle b/tests/slicing/oracle/unravel-point.4.res.oracle index 1f8cdc7191b0682e09fcee2d185d1b79f63d7be6..111fe11a744d9eafc4cf108de952f63668306c03 100644 --- a/tests/slicing/oracle/unravel-point.4.res.oracle +++ b/tests/slicing/oracle/unravel-point.4.res.oracle @@ -81,13 +81,13 @@ [eva] done for function main [from] ====== DISPLAYING CALLWISE DEPENDENCIES ====== [from] call to printf at tests/slicing/unravel-point.i:36 (by send1): - \result FROM \nothing + \result FROM __x1; "%d\n" [from] call to printf at tests/slicing/unravel-point.i:40 (by send2): - \result FROM \nothing + \result FROM __x1; "%d\n" [from] call to printf at tests/slicing/unravel-point.i:44 (by send3): - \result FROM \nothing + \result FROM __x1; "%d\n" [from] call to printf at tests/slicing/unravel-point.i:48 (by send4): - \result FROM \nothing + \result FROM __x1; "%d\n" [from] call to scanf at tests/slicing/unravel-point.i:59 (by main): input1 FROM \nothing \result FROM ANYTHING(origin:Unknown) @@ -189,20 +189,20 @@ [eva] done for function main [from] ====== DISPLAYING CALLWISE DEPENDENCIES ====== [from] call to scanf at tests/slicing/unravel-point.i:59 (by main): - input1 FROM input1 (and SELF) - \result FROM input1 + input1 FROM input1; "%d"[bits 0 to 23] (and SELF) + \result FROM input1; "%d"[bits 0 to 23] [from] call to scanf at tests/slicing/unravel-point.i:61 (by main): - input2 FROM input2 (and SELF) - \result FROM input2 + input2 FROM input2; "%d"[bits 0 to 23] (and SELF) + \result FROM input2; "%d"[bits 0 to 23] [from] call to scanf at tests/slicing/unravel-point.i:63 (by main): - input3 FROM input3 (and SELF) - \result FROM input3 + input3 FROM input3; "%d"[bits 0 to 23] (and SELF) + \result FROM input3; "%d"[bits 0 to 23] [from] call to scanf at tests/slicing/unravel-point.i:65 (by main): - cond1 FROM cond1 (and SELF) - \result FROM cond1 + cond1 FROM cond1; "%d"[bits 0 to 23] (and SELF) + \result FROM cond1; "%d"[bits 0 to 23] [from] call to scanf at tests/slicing/unravel-point.i:66 (by main): - cond2 FROM cond2 (and SELF) - \result FROM cond2 + cond2 FROM cond2; "%d"[bits 0 to 23] (and SELF) + \result FROM cond2; "%d"[bits 0 to 23] [from] call to send1_slice_1 at tests/slicing/unravel-point.i:75 (by main): \result FROM x [from] call to send4_slice_1 at tests/slicing/unravel-point.i:78 (by main): @@ -229,8 +229,9 @@ [sparecode] removed unused global declarations in new project 'Slicing export' /* Generated by Frama-C */ /*@ assigns \result, *p; - assigns \result \from *p; - assigns *p \from *p; */ + assigns \result \from *(__x0 + (0 ..)), *p; + assigns *p \from *(__x0 + (0 ..)), *p; + */ int scanf(char const *, int *p); int send1_slice_1(int x) diff --git a/tests/spec/oracle/unused.res.oracle b/tests/spec/oracle/unused.res.oracle index c28824052ed4446fdf10c762e1d7ff2a44fe9876..1853a1ef2a9e02473873c63fbc13014c2c364c61 100644 --- a/tests/spec/oracle/unused.res.oracle +++ b/tests/spec/oracle/unused.res.oracle @@ -15,6 +15,6 @@ static int i; extern int c; /*@ requires c ≡ 0; */ - __attribute__((__FC_BUILTIN__)) void foo(int *); + __attribute__((__FC_BUILTIN__)) void foo(int *__x0); diff --git a/tests/syntax/oracle/check_builtin_bts1440.res.oracle b/tests/syntax/oracle/check_builtin_bts1440.res.oracle index 510a8f2b3ab41a3c39cd5c26cc41c8703528b9e1..e3f67044af38fd7e0b6bc3940c501fb55455fc03 100644 --- a/tests/syntax/oracle/check_builtin_bts1440.res.oracle +++ b/tests/syntax/oracle/check_builtin_bts1440.res.oracle @@ -2,232 +2,239 @@ [kernel:file:print-one] result of parsing tests/syntax/check_builtin_bts1440.i: /* Generated by Frama-C */ - void __builtin__Exit(int); + void __builtin__Exit(int __x0); - int __builtin___fprintf_chk(void *, int, char const * , ...); + int __builtin___fprintf_chk(void *__x0, int __x1, char const *__x2 , ...); - void *__builtin___memcpy_chk(void *, void const *, unsigned int, unsigned int); + void *__builtin___memcpy_chk(void *__x0, void const *__x1, unsigned int __x2, + unsigned int __x3); - void *__builtin___memmove_chk(void *, void const *, unsigned int, - unsigned int); + void *__builtin___memmove_chk(void *__x0, void const *__x1, + unsigned int __x2, unsigned int __x3); - void *__builtin___mempcpy_chk(void *, void const *, unsigned int, - unsigned int); + void *__builtin___mempcpy_chk(void *__x0, void const *__x1, + unsigned int __x2, unsigned int __x3); - void *__builtin___memset_chk(void *, int, unsigned int, unsigned int); + void *__builtin___memset_chk(void *__x0, int __x1, unsigned int __x2, + unsigned int __x3); - int __builtin___printf_chk(int, char const * , ...); + int __builtin___printf_chk(int __x0, char const *__x1 , ...); - int __builtin___snprintf_chk(char *, unsigned int, int, unsigned int, - char const * , ...); + int __builtin___snprintf_chk(char *__x0, unsigned int __x1, int __x2, + unsigned int __x3, char const *__x4 , ...); - int __builtin___sprintf_chk(char *, int, unsigned int, char const * , ...); + int __builtin___sprintf_chk(char *__x0, int __x1, unsigned int __x2, + char const *__x3 , ...); - char *__builtin___stpcpy_chk(char *, char const *, unsigned int); + char *__builtin___stpcpy_chk(char *__x0, char const *__x1, unsigned int __x2); - char *__builtin___strcat_chk(char *, char const *, unsigned int); + char *__builtin___strcat_chk(char *__x0, char const *__x1, unsigned int __x2); - char *__builtin___strcpy_chk(char *, char const *, unsigned int); + char *__builtin___strcpy_chk(char *__x0, char const *__x1, unsigned int __x2); - char *__builtin___strncat_chk(char *, char const *, unsigned int, - unsigned int); + char *__builtin___strncat_chk(char *__x0, char const *__x1, + unsigned int __x2, unsigned int __x3); - char *__builtin___strncpy_chk(char *, char const *, unsigned int, - unsigned int); + char *__builtin___strncpy_chk(char *__x0, char const *__x1, + unsigned int __x2, unsigned int __x3); - int __builtin___vfprintf_chk(void *, int, char const *, __builtin_va_list); + int __builtin___vfprintf_chk(void *__x0, int __x1, char const *__x2, + __builtin_va_list __x3); - int __builtin___vprintf_chk(int, char const *, __builtin_va_list); + int __builtin___vprintf_chk(int __x0, char const *__x1, + __builtin_va_list __x2); - int __builtin___vsnprintf_chk(char *, unsigned int, int, unsigned int, - char const *, __builtin_va_list); + 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 *, int, unsigned int, char const *, - __builtin_va_list); + int __builtin___vsprintf_chk(char *__x0, int __x1, unsigned int __x2, + char const *__x3, __builtin_va_list __x4); - int __builtin_abs(int); + int __builtin_abs(int __x0); - double __builtin_acos(double); + double __builtin_acos(double __x0); - float __builtin_acosf(float); + float __builtin_acosf(float __x0); - double __builtin_acosh(double); + double __builtin_acosh(double __x0); - float __builtin_acoshf(float); + float __builtin_acoshf(float __x0); - long double __builtin_acoshl(long double); + long double __builtin_acoshl(long double __x0); - long double __builtin_acosl(long double); + long double __builtin_acosl(long double __x0); - void *__builtin_alloca(unsigned int); + void *__builtin_alloca(unsigned int __x0); - double __builtin_asin(double); + double __builtin_asin(double __x0); - float __builtin_asinf(float); + float __builtin_asinf(float __x0); - double __builtin_asinh(double); + double __builtin_asinh(double __x0); - float __builtin_asinhf(float); + float __builtin_asinhf(float __x0); - long double __builtin_asinhl(long double); + long double __builtin_asinhl(long double __x0); - long double __builtin_asinl(long double); + long double __builtin_asinl(long double __x0); - double __builtin_atan(double); + double __builtin_atan(double __x0); - double __builtin_atan2(double, double); + double __builtin_atan2(double __x0, double __x1); - float __builtin_atan2f(float, float); + float __builtin_atan2f(float __x0, float __x1); - long double __builtin_atan2l(long double, long double); + long double __builtin_atan2l(long double __x0, long double __x1); - float __builtin_atanf(float); + float __builtin_atanf(float __x0); - double __builtin_atanh(double); + double __builtin_atanh(double __x0); - float __builtin_atanhf(float); + float __builtin_atanhf(float __x0); - long double __builtin_atanhl(long double); + long double __builtin_atanhl(long double __x0); - long double __builtin_atanl(long double); + long double __builtin_atanl(long double __x0); - unsigned short __builtin_bswap16(unsigned short); + unsigned short __builtin_bswap16(unsigned short __x0); - unsigned int __builtin_bswap32(unsigned int); + unsigned int __builtin_bswap32(unsigned int __x0); - unsigned long long __builtin_bswap64(unsigned long long); + unsigned long long __builtin_bswap64(unsigned long long __x0); - void *__builtin_calloc(unsigned int, unsigned int); + void *__builtin_calloc(unsigned int __x0, unsigned int __x1); - double __builtin_cbrt(double); + double __builtin_cbrt(double __x0); - float __builtin_cbrtf(float); + float __builtin_cbrtf(float __x0); - long double __builtin_cbrtl(long double); + long double __builtin_cbrtl(long double __x0); - double __builtin_ceil(double); + double __builtin_ceil(double __x0); - float __builtin_ceilf(float); + float __builtin_ceilf(float __x0); - long double __builtin_ceill(long double); + long double __builtin_ceill(long double __x0); - int __builtin_constant_p(int); + int __builtin_constant_p(int __x0); - double __builtin_copysign(double, double); + double __builtin_copysign(double __x0, double __x1); - float __builtin_copysignf(float, float); + float __builtin_copysignf(float __x0, float __x1); - long double __builtin_copysignl(long double, long double); + long double __builtin_copysignl(long double __x0, long double __x1); - double __builtin_cos(double); + double __builtin_cos(double __x0); - float __builtin_cosf(float); + float __builtin_cosf(float __x0); - double __builtin_cosh(double); + double __builtin_cosh(double __x0); - float __builtin_coshf(float); + float __builtin_coshf(float __x0); - long double __builtin_coshl(long double); + long double __builtin_coshl(long double __x0); - long double __builtin_cosl(long double); + long double __builtin_cosl(long double __x0); - double __builtin_erf(double); + double __builtin_erf(double __x0); - double __builtin_erfc(double); + double __builtin_erfc(double __x0); - float __builtin_erfcf(float); + float __builtin_erfcf(float __x0); - long double __builtin_erfcl(long double); + long double __builtin_erfcl(long double __x0); - float __builtin_erff(float); + float __builtin_erff(float __x0); - long double __builtin_erfl(long double); + long double __builtin_erfl(long double __x0); - void __builtin_exit(int); + void __builtin_exit(int __x0); - double __builtin_exp(double); + double __builtin_exp(double __x0); - double __builtin_exp2(double); + double __builtin_exp2(double __x0); - float __builtin_exp2f(float); + float __builtin_exp2f(float __x0); - long double __builtin_exp2l(long double); + long double __builtin_exp2l(long double __x0); - long __builtin_expect(long, long); + long __builtin_expect(long __x0, long __x1); - float __builtin_expf(float); + float __builtin_expf(float __x0); - long double __builtin_expl(long double); + long double __builtin_expl(long double __x0); - double __builtin_expm1(double); + double __builtin_expm1(double __x0); - float __builtin_expm1f(float); + float __builtin_expm1f(float __x0); - long double __builtin_expm1l(long double); + long double __builtin_expm1l(long double __x0); - double __builtin_fabs(double); + double __builtin_fabs(double __x0); - float __builtin_fabsf(float); + float __builtin_fabsf(float __x0); - long double __builtin_fabsl(long double); + long double __builtin_fabsl(long double __x0); - double __builtin_fdim(double, double); + double __builtin_fdim(double __x0, double __x1); - float __builtin_fdimf(float, float); + float __builtin_fdimf(float __x0, float __x1); - long double __builtin_fdiml(long double, long double); + long double __builtin_fdiml(long double __x0, long double __x1); - int __builtin_ffs(unsigned int); + int __builtin_ffs(unsigned int __x0); - int __builtin_ffsl(unsigned long); + int __builtin_ffsl(unsigned long __x0); - int __builtin_ffsll(unsigned long long); + int __builtin_ffsll(unsigned long long __x0); - double __builtin_floor(double); + double __builtin_floor(double __x0); - float __builtin_floorf(float); + float __builtin_floorf(float __x0); - long double __builtin_floorl(long double); + long double __builtin_floorl(long double __x0); - double __builtin_fma(double, double, double); + double __builtin_fma(double __x0, double __x1, double __x2); - float __builtin_fmaf(float, float, float); + float __builtin_fmaf(float __x0, float __x1, float __x2); - long double __builtin_fmal(long double, long double, long double); + long double __builtin_fmal(long double __x0, long double __x1, + long double __x2); - double __builtin_fmax(double, double); + double __builtin_fmax(double __x0, double __x1); - float __builtin_fmaxf(float, float); + float __builtin_fmaxf(float __x0, float __x1); - long double __builtin_fmaxl(long double, long double); + long double __builtin_fmaxl(long double __x0, long double __x1); - double __builtin_fmin(double, double); + double __builtin_fmin(double __x0, double __x1); - float __builtin_fminf(float, float); + float __builtin_fminf(float __x0, float __x1); - long double __builtin_fminl(long double, long double); + long double __builtin_fminl(long double __x0, long double __x1); - double __builtin_fmod(double); + double __builtin_fmod(double __x0); - float __builtin_fmodf(float); + float __builtin_fmodf(float __x0); - long double __builtin_fmodl(long double); + long double __builtin_fmodl(long double __x0); - int __builtin_fprintf(void *, char const * , ...); + int __builtin_fprintf(void *__x0, char const *__x1 , ...); - int __builtin_fputs(char const *, void *); + int __builtin_fputs(char const *__x0, void *__x1); - void *__builtin_frame_address(unsigned int); + void *__builtin_frame_address(unsigned int __x0); - void __builtin_free(void *); + void __builtin_free(void *__x0); - double __builtin_frexp(double, int *); + double __builtin_frexp(double __x0, int *__x1); - float __builtin_frexpf(float, int *); + float __builtin_frexpf(float __x0, int *__x1); - long double __builtin_frexpl(long double, int *); + long double __builtin_frexpl(long double __x0, int *__x1); - int __builtin_fscanf(void *, char const * , ...); + int __builtin_fscanf(void *__x0, char const *__x1 , ...); double __builtin_huge_val(void); @@ -235,11 +242,11 @@ long double __builtin_huge_vall(void); - double __builtin_hypot(double, double); + double __builtin_hypot(double __x0, double __x1); - float __builtin_hypotf(float, float); + float __builtin_hypotf(float __x0, float __x1); - long double __builtin_hypotl(long double, long double); + long double __builtin_hypotl(long double __x0, long double __x1); void __builtin_ia32_lfence(void); @@ -247,11 +254,11 @@ void __builtin_ia32_sfence(void); - double __builtin_ilogb(double); + double __builtin_ilogb(double __x0); - float __builtin_ilogbf(float); + float __builtin_ilogbf(float __x0); - long double __builtin_ilogbl(long double); + long double __builtin_ilogbl(long double __x0); double __builtin_inf(void); @@ -259,677 +266,710 @@ long double __builtin_infl(void); - int __builtin_isalnum(int); + int __builtin_isalnum(int __x0); - int __builtin_isalpha(int); + int __builtin_isalpha(int __x0); - int __builtin_isblank(int); + int __builtin_isblank(int __x0); - int __builtin_iscntrl(int); + int __builtin_iscntrl(int __x0); - int __builtin_isdigit(int); + int __builtin_isdigit(int __x0); - int __builtin_isgraph(int); + int __builtin_isgraph(int __x0); - int __builtin_islower(int); + int __builtin_islower(int __x0); - int __builtin_isprint(int); + int __builtin_isprint(int __x0); - int __builtin_ispunct(int); + int __builtin_ispunct(int __x0); - int __builtin_isspace(int); + int __builtin_isspace(int __x0); - int __builtin_isupper(int); + int __builtin_isupper(int __x0); - int __builtin_isxdigit(int); + int __builtin_isxdigit(int __x0); - long __builtin_labs(long); + long __builtin_labs(long __x0); - double __builtin_ldexp(double, int); + double __builtin_ldexp(double __x0, int __x1); - float __builtin_ldexpf(float, int); + float __builtin_ldexpf(float __x0, int __x1); - long double __builtin_ldexpl(long double, int); + long double __builtin_ldexpl(long double __x0, int __x1); - double __builtin_lgamma(double); + double __builtin_lgamma(double __x0); - float __builtin_lgammaf(float); + float __builtin_lgammaf(float __x0); - long double __builtin_lgammal(long double); + long double __builtin_lgammal(long double __x0); - long long __builtin_llabs(long long); + long long __builtin_llabs(long long __x0); - long long __builtin_llrint(double); + long long __builtin_llrint(double __x0); - long long __builtin_llrintf(float); + long long __builtin_llrintf(float __x0); - long long __builtin_llrintl(long double); + long long __builtin_llrintl(long double __x0); - long long __builtin_llround(double); + long long __builtin_llround(double __x0); - long long __builtin_llroundf(float); + long long __builtin_llroundf(float __x0); - long long __builtin_llroundl(long double); + long long __builtin_llroundl(long double __x0); - double __builtin_log(double); + double __builtin_log(double __x0); - double __builtin_log10(double); + double __builtin_log10(double __x0); - float __builtin_log10f(float); + float __builtin_log10f(float __x0); - long double __builtin_log10l(long double); + long double __builtin_log10l(long double __x0); - double __builtin_log1p(double); + double __builtin_log1p(double __x0); - float __builtin_log1pf(float); + float __builtin_log1pf(float __x0); - long double __builtin_log1pl(long double); + long double __builtin_log1pl(long double __x0); - double __builtin_log2(double); + double __builtin_log2(double __x0); - float __builtin_log2f(float); + float __builtin_log2f(float __x0); - long double __builtin_log2l(long double); + long double __builtin_log2l(long double __x0); - double __builtin_logb(double); + double __builtin_logb(double __x0); - float __builtin_logbf(float); + float __builtin_logbf(float __x0); - long double __builtin_logbl(long double); + long double __builtin_logbl(long double __x0); - float __builtin_logf(float); + float __builtin_logf(float __x0); - long double __builtin_logl(long double); + long double __builtin_logl(long double __x0); - long __builtin_lrint(double); + long __builtin_lrint(double __x0); - long __builtin_lrintf(float); + long __builtin_lrintf(float __x0); - long __builtin_lrintl(long double); + long __builtin_lrintl(long double __x0); - long __builtin_lround(double); + long __builtin_lround(double __x0); - long __builtin_lroundf(float); + long __builtin_lroundf(float __x0); - long __builtin_lroundl(long double); + long __builtin_lroundl(long double __x0); - void *__builtin_malloc(unsigned int); + void *__builtin_malloc(unsigned int __x0); - void *__builtin_memchr(void const *, int, unsigned int); + void *__builtin_memchr(void const *__x0, int __x1, unsigned int __x2); - int __builtin_memcmp(void const *, void const *, unsigned int); + int __builtin_memcmp(void const *__x0, void const *__x1, unsigned int __x2); - void *__builtin_memcpy(void *, void const *, unsigned int); + void *__builtin_memcpy(void *__x0, void const *__x1, unsigned int __x2); - void *__builtin_mempcpy(void *, void const *, unsigned int); + void *__builtin_mempcpy(void *__x0, void const *__x1, unsigned int __x2); - void *__builtin_memset(void *, int, unsigned int); + void *__builtin_memset(void *__x0, int __x1, unsigned int __x2); - double __builtin_modf(double, double *); + double __builtin_modf(double __x0, double *__x1); - float __builtin_modff(float, float *); + float __builtin_modff(float __x0, float *__x1); - long double __builtin_modfl(long double, long double *); + long double __builtin_modfl(long double __x0, long double *__x1); - double __builtin_nan(char const *); + double __builtin_nan(char const *__x0); - float __builtin_nanf(char const *); + float __builtin_nanf(char const *__x0); - long double __builtin_nanl(char const *); + long double __builtin_nanl(char const *__x0); - double __builtin_nans(char const *); + double __builtin_nans(char const *__x0); - float __builtin_nansf(char const *); + float __builtin_nansf(char const *__x0); - long double __builtin_nansl(char const *); + long double __builtin_nansl(char const *__x0); - double __builtin_nearbyint(double); + double __builtin_nearbyint(double __x0); - float __builtin_nearbyintf(float); + float __builtin_nearbyintf(float __x0); - long double __builtin_nearbyintl(long double); + long double __builtin_nearbyintl(long double __x0); __builtin_va_list __builtin_next_arg(void); - double __builtin_nextafter(double, double); + double __builtin_nextafter(double __x0, double __x1); - float __builtin_nextafterf(float, float); + float __builtin_nextafterf(float __x0, float __x1); - long double __builtin_nextafterl(long double, long double); + long double __builtin_nextafterl(long double __x0, long double __x1); - double __builtin_nexttoward(double, long double); + double __builtin_nexttoward(double __x0, long double __x1); - float __builtin_nexttowardf(float, long double); + float __builtin_nexttowardf(float __x0, long double __x1); - long double __builtin_nexttowardl(long double, long double); + long double __builtin_nexttowardl(long double __x0, long double __x1); - unsigned int __builtin_object_size(void *, int); + unsigned int __builtin_object_size(void *__x0, int __x1); - unsigned int __builtin_offsetof(unsigned int); + unsigned int __builtin_offsetof(unsigned int __x0); - int __builtin_parity(unsigned int); + int __builtin_parity(unsigned int __x0); - int __builtin_parityl(unsigned long); + int __builtin_parityl(unsigned long __x0); - int __builtin_parityll(unsigned long long); + int __builtin_parityll(unsigned long long __x0); - double __builtin_pow(double, double); + double __builtin_pow(double __x0, double __x1); - float __builtin_powf(float, float); + float __builtin_powf(float __x0, float __x1); - double __builtin_powi(double, int); + double __builtin_powi(double __x0, int __x1); - float __builtin_powif(float, int); + float __builtin_powif(float __x0, int __x1); - long double __builtin_powil(long double, int); + long double __builtin_powil(long double __x0, int __x1); - long double __builtin_powl(long double, long double); + long double __builtin_powl(long double __x0, long double __x1); - void __builtin_prefetch(void const * , ...); + void __builtin_prefetch(void const *__x0 , ...); - int __builtin_printf(char const * , ...); + int __builtin_printf(char const *__x0 , ...); - int __builtin_putchar(int); + int __builtin_putchar(int __x0); - int __builtin_puts(char const *); + int __builtin_puts(char const *__x0); - void *__builtin_realloc(void *, unsigned int); + void *__builtin_realloc(void *__x0, unsigned int __x1); - double __builtin_remainder(double, double); + double __builtin_remainder(double __x0, double __x1); - float __builtin_remainderf(float, float); + float __builtin_remainderf(float __x0, float __x1); - long double __builtin_remainderl(long double, long double); + long double __builtin_remainderl(long double __x0, long double __x1); - double __builtin_remquo(double, double, int *); + double __builtin_remquo(double __x0, double __x1, int *__x2); - float __builtin_remquof(float, float, int *); + float __builtin_remquof(float __x0, float __x1, int *__x2); - long double __builtin_remquol(long double, long double, int *); + long double __builtin_remquol(long double __x0, long double __x1, int *__x2); - void __builtin_return(void const *); + void __builtin_return(void const *__x0); - void *__builtin_return_address(unsigned int); + void *__builtin_return_address(unsigned int __x0); - double __builtin_rint(double); + double __builtin_rint(double __x0); - float __builtin_rintf(float); + float __builtin_rintf(float __x0); - long double __builtin_rintl(long double); + long double __builtin_rintl(long double __x0); - double __builtin_round(double); + double __builtin_round(double __x0); - float __builtin_roundf(float); + float __builtin_roundf(float __x0); - long double __builtin_roundl(long double); + long double __builtin_roundl(long double __x0); - double __builtin_scalbln(double, long); + double __builtin_scalbln(double __x0, long __x1); - float __builtin_scalblnf(float, long); + float __builtin_scalblnf(float __x0, long __x1); - long double __builtin_scalblnl(long double, long); + long double __builtin_scalblnl(long double __x0, long __x1); - double __builtin_scalbn(double, int); + double __builtin_scalbn(double __x0, int __x1); - float __builtin_scalbnf(float, int); + float __builtin_scalbnf(float __x0, int __x1); - long double __builtin_scalbnl(long double, int); + long double __builtin_scalbnl(long double __x0, int __x1); - int __builtin_scanf(char const * , ...); + int __builtin_scanf(char const *__x0 , ...); - double __builtin_sin(double); + double __builtin_sin(double __x0); - float __builtin_sinf(float); + float __builtin_sinf(float __x0); - double __builtin_sinh(double); + double __builtin_sinh(double __x0); - float __builtin_sinhf(float); + float __builtin_sinhf(float __x0); - long double __builtin_sinhl(long double); + long double __builtin_sinhl(long double __x0); - long double __builtin_sinl(long double); + long double __builtin_sinl(long double __x0); - int __builtin_snprintf(char *, unsigned int, char const * , ...); + int __builtin_snprintf(char *__x0, unsigned int __x1, char const *__x2 , ...); - int __builtin_sprintf(char *, char const * , ...); + int __builtin_sprintf(char *__x0, char const *__x1 , ...); - double __builtin_sqrt(double); + double __builtin_sqrt(double __x0); - float __builtin_sqrtf(float); + float __builtin_sqrtf(float __x0); - long double __builtin_sqrtl(long double); + long double __builtin_sqrtl(long double __x0); - int __builtin_sscanf(char const *, char const * , ...); + int __builtin_sscanf(char const *__x0, char const *__x1 , ...); - void __builtin_stdarg_start(__builtin_va_list); + void __builtin_stdarg_start(__builtin_va_list __x0); - char *__builtin_stpcpy(char *, char const *); + char *__builtin_stpcpy(char *__x0, char const *__x1); - char *__builtin_strcat(char *, char const *); + char *__builtin_strcat(char *__x0, char const *__x1); - char *__builtin_strchr(char *, int); + char *__builtin_strchr(char *__x0, int __x1); - int __builtin_strcmp(char const *, char const *); + int __builtin_strcmp(char const *__x0, char const *__x1); - char *__builtin_strcpy(char *, char const *); + char *__builtin_strcpy(char *__x0, char const *__x1); - unsigned int __builtin_strcspn(char const *, char const *); + unsigned int __builtin_strcspn(char const *__x0, char const *__x1); - unsigned int __builtin_strlen(char const *); + unsigned int __builtin_strlen(char const *__x0); - char *__builtin_strncat(char *, char const *, unsigned int); + char *__builtin_strncat(char *__x0, char const *__x1, unsigned int __x2); - int __builtin_strncmp(char const *, char const *, unsigned int); + int __builtin_strncmp(char const *__x0, char const *__x1, unsigned int __x2); - char *__builtin_strncpy(char *, char const *, unsigned int); + char *__builtin_strncpy(char *__x0, char const *__x1, unsigned int __x2); - char *__builtin_strpbrk(char const *, char const *); + char *__builtin_strpbrk(char const *__x0, char const *__x1); - char *__builtin_strrchr(char const *, int); + char *__builtin_strrchr(char const *__x0, int __x1); - unsigned int __builtin_strspn(char const *, char const *); + unsigned int __builtin_strspn(char const *__x0, char const *__x1); - char *__builtin_strstr(char const *, char const *); + char *__builtin_strstr(char const *__x0, char const *__x1); - double __builtin_tan(double); + double __builtin_tan(double __x0); - float __builtin_tanf(float); + float __builtin_tanf(float __x0); - double __builtin_tanh(double); + double __builtin_tanh(double __x0); - float __builtin_tanhf(float); + float __builtin_tanhf(float __x0); - long double __builtin_tanhl(long double); + long double __builtin_tanhl(long double __x0); - long double __builtin_tanl(long double); + long double __builtin_tanl(long double __x0); - double __builtin_tgamma(double); + double __builtin_tgamma(double __x0); - float __builtin_tgammaf(float); + float __builtin_tgammaf(float __x0); - long double __builtin_tgammal(long double); + long double __builtin_tgammal(long double __x0); - int __builtin_tolower(int); + int __builtin_tolower(int __x0); - int __builtin_toupper(int); + int __builtin_toupper(int __x0); - double __builtin_trunc(double); + double __builtin_trunc(double __x0); - float __builtin_truncf(float); + float __builtin_truncf(float __x0); - long double __builtin_truncl(long double); + long double __builtin_truncl(long double __x0); - int __builtin_types_compatible_p(unsigned int, unsigned int); + int __builtin_types_compatible_p(unsigned int __x0, unsigned int __x1); void __builtin_unreachable(void); - void __builtin_va_arg(__builtin_va_list, unsigned int, void *); + void __builtin_va_arg(__builtin_va_list __x0, unsigned int __x1, void *__x2); - void __builtin_va_copy(__builtin_va_list, __builtin_va_list); + void __builtin_va_copy(__builtin_va_list __x0, __builtin_va_list __x1); - void __builtin_va_end(__builtin_va_list); + void __builtin_va_end(__builtin_va_list __x0); - void __builtin_va_start(__builtin_va_list); + void __builtin_va_start(__builtin_va_list __x0); - void __builtin_varargs_start(__builtin_va_list); + void __builtin_varargs_start(__builtin_va_list __x0); - int __builtin_vfprintf(void *, char const *, __builtin_va_list); + int __builtin_vfprintf(void *__x0, char const *__x1, __builtin_va_list __x2); - int __builtin_vfscanf(void *, char const *, __builtin_va_list); + int __builtin_vfscanf(void *__x0, char const *__x1, __builtin_va_list __x2); - int __builtin_vprintf(char const *, __builtin_va_list); + int __builtin_vprintf(char const *__x0, __builtin_va_list __x1); - int __builtin_vscanf(char const *, __builtin_va_list); + int __builtin_vscanf(char const *__x0, __builtin_va_list __x1); - int __builtin_vsnprintf(char *, unsigned int, char const *, __builtin_va_list); + int __builtin_vsnprintf(char *__x0, unsigned int __x1, char const *__x2, + __builtin_va_list __x3); - int __builtin_vsprintf(char *, char const *, __builtin_va_list); + int __builtin_vsprintf(char *__x0, char const *__x1, __builtin_va_list __x2); - int __builtin_vsscanf(char const *, char const *, __builtin_va_list); + int __builtin_vsscanf(char const *__x0, char const *__x1, + __builtin_va_list __x2); - short __sync_add_and_fetch_int16_t(short volatile *, short , ...); + short __sync_add_and_fetch_int16_t(short volatile *__x0, short __x1 , ...); - int __sync_add_and_fetch_int32_t(int volatile *, int , ...); + int __sync_add_and_fetch_int32_t(int volatile *__x0, int __x1 , ...); - long long __sync_add_and_fetch_int64_t(long long volatile *, long long , ...); + 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 *, signed char - , ...); + 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 *, - unsigned short , ...); + 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 *, - unsigned int , ...); + 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 *, - unsigned long long , ...); + 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 *, - unsigned char , ...); + unsigned char __sync_add_and_fetch_uint8_t(unsigned char volatile *__x0, + unsigned char __x1 , ...); - short __sync_and_and_fetch_int16_t(short volatile *, short , ...); + short __sync_and_and_fetch_int16_t(short volatile *__x0, short __x1 , ...); - int __sync_and_and_fetch_int32_t(int volatile *, int , ...); + int __sync_and_and_fetch_int32_t(int volatile *__x0, int __x1 , ...); - long long __sync_and_and_fetch_int64_t(long long volatile *, long long , ...); + 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 *, signed char - , ...); + 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 *, - unsigned short , ...); + 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 *, - unsigned int , ...); + 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 *, - unsigned long long , ...); + 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 *, - unsigned char , ...); + 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 *, short, short , ...); + 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 *, int, int , ...); + 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 *, long long, - long long , ...); + 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 *, signed char, - signed char , ...); + 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 *, - unsigned short, unsigned short - , ...); + 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 *, - unsigned int, unsigned int , ...); + 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 *, - unsigned long long, - unsigned long long , ...); + 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 *, - unsigned char, unsigned char , ...); + 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 *, short , ...); + short __sync_fetch_and_add_int16_t(short volatile *__x0, short __x1 , ...); - int __sync_fetch_and_add_int32_t(int volatile *, int , ...); + int __sync_fetch_and_add_int32_t(int volatile *__x0, int __x1 , ...); - long long __sync_fetch_and_add_int64_t(long long volatile *, long long , ...); + 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 *, signed char - , ...); + 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 *, - unsigned short , ...); + 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 *, - unsigned int , ...); + 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 *, - unsigned long long , ...); + 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 *, - unsigned char , ...); + unsigned char __sync_fetch_and_add_uint8_t(unsigned char volatile *__x0, + unsigned char __x1 , ...); - short __sync_fetch_and_and_int16_t(short volatile *, short , ...); + short __sync_fetch_and_and_int16_t(short volatile *__x0, short __x1 , ...); - int __sync_fetch_and_and_int32_t(int volatile *, int , ...); + int __sync_fetch_and_and_int32_t(int volatile *__x0, int __x1 , ...); - long long __sync_fetch_and_and_int64_t(long long volatile *, long long , ...); + 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 *, signed char - , ...); + 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 *, - unsigned short , ...); + 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 *, - unsigned int , ...); + 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 *, - unsigned long long , ...); + 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 *, - unsigned char , ...); + unsigned char __sync_fetch_and_and_uint8_t(unsigned char volatile *__x0, + unsigned char __x1 , ...); - short __sync_fetch_and_nand_int16_t(short volatile *, short , ...); + short __sync_fetch_and_nand_int16_t(short volatile *__x0, short __x1 , ...); - int __sync_fetch_and_nand_int32_t(int volatile *, int , ...); + int __sync_fetch_and_nand_int32_t(int volatile *__x0, int __x1 , ...); - long long __sync_fetch_and_nand_int64_t(long long volatile *, long long , ...); + 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 *, signed char - , ...); + 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 *, - unsigned short , ...); + 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 *, - unsigned int , ...); + 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 *, - unsigned long long , ...); + 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 *, - unsigned char , ...); + unsigned char __sync_fetch_and_nand_uint8_t(unsigned char volatile *__x0, + unsigned char __x1 , ...); - short __sync_fetch_and_or_int16_t(short volatile *, short , ...); + short __sync_fetch_and_or_int16_t(short volatile *__x0, short __x1 , ...); - int __sync_fetch_and_or_int32_t(int volatile *, int , ...); + int __sync_fetch_and_or_int32_t(int volatile *__x0, int __x1 , ...); - long long __sync_fetch_and_or_int64_t(long long volatile *, long long , ...); + 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 *, signed char - , ...); + 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 *, - unsigned short , ...); + 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 *, - unsigned int , ...); + 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 *, - unsigned long long , ...); + 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 *, - unsigned char , ...); + unsigned char __sync_fetch_and_or_uint8_t(unsigned char volatile *__x0, + unsigned char __x1 , ...); - short __sync_fetch_and_sub_int16_t(short volatile *, short , ...); + short __sync_fetch_and_sub_int16_t(short volatile *__x0, short __x1 , ...); - int __sync_fetch_and_sub_int32_t(int volatile *, int , ...); + int __sync_fetch_and_sub_int32_t(int volatile *__x0, int __x1 , ...); - long long __sync_fetch_and_sub_int64_t(long long volatile *, long long , ...); + 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 *, signed char - , ...); + 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 *, - unsigned short , ...); + 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 *, - unsigned int , ...); + 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 *, - unsigned long long , ...); + 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 *, - unsigned char , ...); + unsigned char __sync_fetch_and_sub_uint8_t(unsigned char volatile *__x0, + unsigned char __x1 , ...); - short __sync_fetch_and_xor_int16_t(short volatile *, short , ...); + short __sync_fetch_and_xor_int16_t(short volatile *__x0, short __x1 , ...); - int __sync_fetch_and_xor_int32_t(int volatile *, int , ...); + int __sync_fetch_and_xor_int32_t(int volatile *__x0, int __x1 , ...); - long long __sync_fetch_and_xor_int64_t(long long volatile *, long long , ...); + 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 *, signed char - , ...); + 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 *, - unsigned short , ...); + 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 *, - unsigned int , ...); + 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 *, - unsigned long long , ...); + 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 *, - unsigned char , ...); + unsigned char __sync_fetch_and_xor_uint8_t(unsigned char volatile *__x0, + unsigned char __x1 , ...); - void __sync_lock_release_int16_t(short volatile * , ...); + void __sync_lock_release_int16_t(short volatile *__x0 , ...); - void __sync_lock_release_int32_t(int volatile * , ...); + void __sync_lock_release_int32_t(int volatile *__x0 , ...); - void __sync_lock_release_int64_t(long long volatile * , ...); + void __sync_lock_release_int64_t(long long volatile *__x0 , ...); - void __sync_lock_release_int8_t(signed char volatile * , ...); + void __sync_lock_release_int8_t(signed char volatile *__x0 , ...); - void __sync_lock_release_uint16_t(unsigned short volatile * , ...); + void __sync_lock_release_uint16_t(unsigned short volatile *__x0 , ...); - void __sync_lock_release_uint32_t(unsigned int volatile * , ...); + void __sync_lock_release_uint32_t(unsigned int volatile *__x0 , ...); - void __sync_lock_release_uint64_t(unsigned long long volatile * , ...); + void __sync_lock_release_uint64_t(unsigned long long volatile *__x0 , ...); - void __sync_lock_release_uint8_t(unsigned char volatile * , ...); + void __sync_lock_release_uint8_t(unsigned char volatile *__x0 , ...); - short __sync_lock_test_and_set_int16_t(short volatile *, short , ...); + short __sync_lock_test_and_set_int16_t(short volatile *__x0, short __x1 , ...); - int __sync_lock_test_and_set_int32_t(int volatile *, int , ...); + 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 *, long long - , ...); + 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 *, - signed char , ...); + 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 *, - unsigned short , ...); + 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 *, - unsigned int , ...); + 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 *, - unsigned long long , ...); + 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 *, - unsigned char , ...); + 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 *, short , ...); + short __sync_nand_and_fetch_int16_t(short volatile *__x0, short __x1 , ...); - int __sync_nand_and_fetch_int32_t(int volatile *, int , ...); + int __sync_nand_and_fetch_int32_t(int volatile *__x0, int __x1 , ...); - long long __sync_nand_and_fetch_int64_t(long long volatile *, long long , ...); + 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 *, signed char - , ...); + 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 *, - unsigned short , ...); + 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 *, - unsigned int , ...); + 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 *, - unsigned long long , ...); + 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 *, - unsigned char , ...); + unsigned char __sync_nand_and_fetch_uint8_t(unsigned char volatile *__x0, + unsigned char __x1 , ...); - short __sync_or_and_fetch_int16_t(short volatile *, short , ...); + short __sync_or_and_fetch_int16_t(short volatile *__x0, short __x1 , ...); - int __sync_or_and_fetch_int32_t(int volatile *, int , ...); + int __sync_or_and_fetch_int32_t(int volatile *__x0, int __x1 , ...); - long long __sync_or_and_fetch_int64_t(long long volatile *, long long , ...); + 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 *, signed char - , ...); + 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 *, - unsigned short , ...); + 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 *, - unsigned int , ...); + 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 *, - unsigned long long , ...); + 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 *, - unsigned char , ...); + unsigned char __sync_or_and_fetch_uint8_t(unsigned char volatile *__x0, + unsigned char __x1 , ...); - short __sync_sub_and_fetch_int16_t(short volatile *, short , ...); + short __sync_sub_and_fetch_int16_t(short volatile *__x0, short __x1 , ...); - int __sync_sub_and_fetch_int32_t(int volatile *, int , ...); + int __sync_sub_and_fetch_int32_t(int volatile *__x0, int __x1 , ...); - long long __sync_sub_and_fetch_int64_t(long long volatile *, long long , ...); + 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 *, signed char - , ...); + 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 *, - unsigned short , ...); + 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 *, - unsigned int , ...); + 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 *, - unsigned long long , ...); + 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 *, - unsigned char , ...); + unsigned char __sync_sub_and_fetch_uint8_t(unsigned char volatile *__x0, + unsigned char __x1 , ...); void __sync_synchronize(...); - short __sync_val_compare_and_swap_int16_t(short volatile *, short, short - , ...); + 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 *, int, int , ...); + 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 *, - long long, long long , ...); + 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 *, - signed char, signed char , ...); + 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 *, - unsigned short, - unsigned short , ...); + 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 *, - unsigned int, unsigned int - , ...); + 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 *, - unsigned long long, - unsigned long long + 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 *, - unsigned char, - unsigned char , ...); + 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 *, short , ...); + short __sync_xor_and_fetch_int16_t(short volatile *__x0, short __x1 , ...); - int __sync_xor_and_fetch_int32_t(int volatile *, int , ...); + int __sync_xor_and_fetch_int32_t(int volatile *__x0, int __x1 , ...); - long long __sync_xor_and_fetch_int64_t(long long volatile *, long long , ...); + 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 *, signed char - , ...); + 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 *, - unsigned short , ...); + 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 *, - unsigned int , ...); + 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 *, - unsigned long long , ...); + 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 *, - unsigned char , ...); + unsigned char __sync_xor_and_fetch_uint8_t(unsigned char volatile *__x0, + unsigned char __x1 , ...); int max(int i, int j) { diff --git a/tests/syntax/oracle/vdescr_bts1387.res.oracle b/tests/syntax/oracle/vdescr_bts1387.res.oracle index a5c81d268f53e53ef3daac9619cf2d5378f26381..fa87e2625fbac770015eb9e9cadc1e097a6e4442 100644 --- a/tests/syntax/oracle/vdescr_bts1387.res.oracle +++ b/tests/syntax/oracle/vdescr_bts1387.res.oracle @@ -1,8 +1,8 @@ [kernel] Parsing tests/syntax/vdescr_bts1387.i (no preprocessing) [kernel] Variable f has vdescr '' -[kernel] Variable has vdescr '' +[kernel] Variable __x0 has vdescr '' [kernel] Variable g has vdescr '' -[kernel] Variable has vdescr '' +[kernel] Variable __x0 has vdescr '' [kernel] Variable fptr has vdescr '' [kernel] Variable main has vdescr '' [kernel] Variable j has vdescr '' diff --git a/tests/value/oracle/bug0223.0.res.oracle b/tests/value/oracle/bug0223.0.res.oracle index 95216a488d0cd5ba9ab0bb184bf366158fec215e..60ea63f4943e1283c987763f5aa1609c5505571e 100644 --- a/tests/value/oracle/bug0223.0.res.oracle +++ b/tests/value/oracle/bug0223.0.res.oracle @@ -48,7 +48,7 @@ [from] ====== DEPENDENCIES COMPUTED ====== These dependencies hold at termination for the executions that terminate: [from] Function F: - \result FROM \nothing + \result FROM __x0; __x1 [from] Function my_strcnmp: \result FROM n [from] Function h2: diff --git a/tests/value/oracle/bug0223.1.res.oracle b/tests/value/oracle/bug0223.1.res.oracle index 95216a488d0cd5ba9ab0bb184bf366158fec215e..60ea63f4943e1283c987763f5aa1609c5505571e 100644 --- a/tests/value/oracle/bug0223.1.res.oracle +++ b/tests/value/oracle/bug0223.1.res.oracle @@ -48,7 +48,7 @@ [from] ====== DEPENDENCIES COMPUTED ====== These dependencies hold at termination for the executions that terminate: [from] Function F: - \result FROM \nothing + \result FROM __x0; __x1 [from] Function my_strcnmp: \result FROM n [from] Function h2: diff --git a/tests/value/oracle/from_call.0.res.oracle b/tests/value/oracle/from_call.0.res.oracle index 90af155562b9b8797ae7bcbd68e0ee6bd42434e9..3c1554933630cb972f005d119af7e5131ad64662 100644 --- a/tests/value/oracle/from_call.0.res.oracle +++ b/tests/value/oracle/from_call.0.res.oracle @@ -233,7 +233,7 @@ [from] call to g at tests/value/from_call.i:20 (by f): \result FROM t; w [from] call to h at tests/value/from_call.i:20 (by f): - \result FROM \nothing + \result FROM __x0 [from] call to return_A1 at tests/value/from_call.i:44 (by dispatcher2): \result FROM A1 [from] call to return_A2 at tests/value/from_call.i:44 (by dispatcher2): @@ -247,15 +247,15 @@ [from] call to f at tests/value/from_call.i:81 (by main): b FROM a; p; f_previous f_previous FROM p - \result FROM a; t; p; f_previous + \result FROM a; x; t; p; f_previous [from] call to f at tests/value/from_call.i:82 (by main): c FROM b; p; f_previous f_previous FROM p - \result FROM b; t; p; f_previous + \result FROM b; x; t; p; f_previous [from] call to f at tests/value/from_call.i:82 (by main): d FROM c; p; f_previous f_previous FROM p - \result FROM c; t; p; f_previous + \result FROM c; x; t; p; f_previous [from] call to dispatcher at tests/value/from_call.i:83 (by main): \result FROM c_0; y_0 [from] call to dispatcher at tests/value/from_call.i:84 (by main): @@ -281,8 +281,8 @@ b FROM a; f_previous c FROM a; f_previous d FROM a; f_previous - y FROM a; t; f_previous - z FROM a; t; f_previous + y FROM a; x; t; f_previous + z FROM a; x; t; f_previous R1 FROM A1 R2 FROM A4 R3 FROM A4; A5; r diff --git a/tests/value/oracle/from_call.1.res.oracle b/tests/value/oracle/from_call.1.res.oracle index eb4493ddfd3a65d3dfce413d96809353d388e0e9..8c4d385823045d66ea53f176df188e4c31960b04 100644 --- a/tests/value/oracle/from_call.1.res.oracle +++ b/tests/value/oracle/from_call.1.res.oracle @@ -179,13 +179,13 @@ [from] Function g: \result FROM direct: t; w [from] Function h: - \result FROM \nothing + \result FROM direct: __x0 [from] Function f: b FROM indirect: p; f_previous; direct: a; b; c (and SELF) c FROM indirect: p; f_previous; direct: a; b; c (and SELF) d FROM indirect: p; f_previous; direct: a; b; c (and SELF) f_previous FROM direct: p - \result FROM indirect: p; f_previous; direct: a; b; c; d; t + \result FROM indirect: p; f_previous; direct: a; b; c; d; x; t [from] Function return_A1: \result FROM direct: A1 [from] Function return_A2: @@ -205,8 +205,8 @@ b FROM indirect: f_previous; direct: a; b; c (and SELF) c FROM indirect: f_previous; direct: a; b; c (and SELF) d FROM indirect: f_previous; direct: a; b; c (and SELF) - y FROM indirect: f_previous; direct: a; b; c; d; t - z FROM indirect: f_previous; direct: a; b; c; d; t + y FROM indirect: f_previous; direct: a; b; c; d; x; t + z FROM indirect: f_previous; direct: a; b; c; d; x; t R1 FROM direct: A1; A2 R2 FROM direct: A3; A4 R3 FROM indirect: r; direct: A4; A5 diff --git a/tests/value/oracle/resolve.res.oracle b/tests/value/oracle/resolve.res.oracle index 49a9d91450d37554a884986c1280d4208214afca..05b5f86f0764be2e8b6ce56670ca501162673cf4 100644 --- a/tests/value/oracle/resolve.res.oracle +++ b/tests/value/oracle/resolve.res.oracle @@ -22,7 +22,7 @@ [from] ====== DEPENDENCIES COMPUTED ====== These dependencies hold at termination for the executions that terminate: [from] Function f: - \result FROM \nothing + \result FROM __x0; __x1 [from] Function main: \result FROM \nothing [from] ====== END OF DEPENDENCIES ====== diff --git a/tests/value/oracle/va_list2.1.res.oracle b/tests/value/oracle/va_list2.1.res.oracle index a3b3d14e82c077e0377b92df53337ce4b7b54ece..4cae1c2cf4ddd9c1b9018b1cb195b15e5065ffd2 100644 --- a/tests/value/oracle/va_list2.1.res.oracle +++ b/tests/value/oracle/va_list2.1.res.oracle @@ -22,6 +22,7 @@ accessing uninitialized left-value. assert \initialized(&tmp); (tmp from vararg) +[eva] tests/value/va_list2.c:16: Frama_C_show_each_i: [-2147483648..2147483647] [eva] computing for function __builtin_va_arg <- main. Called from tests/value/va_list2.c:20. [eva] Done for function __builtin_va_arg @@ -29,15 +30,23 @@ accessing uninitialized left-value. assert \initialized(&tmp_0); (tmp_0 from vararg) +[eva:alarm] tests/value/va_list2.c:20: Warning: + non-finite float value. assert \is_finite(tmp_0); + (tmp_0 from vararg) +[eva] tests/value/va_list2.c:21: + Frama_C_show_each_f: [-3.40282346639e+38 .. 3.40282346639e+38] [eva] tests/value/va_list2.c:12: starting to merge loop iterations [eva:alarm] tests/value/va_list2.c:13: Warning: out of bounds read. assert \valid_read(fmt); [eva] computing for function __builtin_va_arg <- main. Called from tests/value/va_list2.c:15. [eva] Done for function __builtin_va_arg +[eva] tests/value/va_list2.c:16: Frama_C_show_each_i: [-2147483648..2147483647] [eva] computing for function __builtin_va_arg <- main. Called from tests/value/va_list2.c:20. [eva] Done for function __builtin_va_arg +[eva] tests/value/va_list2.c:21: + Frama_C_show_each_f: [-3.40282346639e+38 .. 3.40282346639e+38] [eva] computing for function __builtin_va_end <- main. Called from tests/value/va_list2.c:28. [kernel:annot:missing-spec] tests/value/va_list2.c:28: Warning: @@ -46,10 +55,6 @@ [eva] Done for function __builtin_va_end [eva] Recording results for main [eva] done for function main -[eva] tests/value/va_list2.c:15: - assertion 'Eva,initialization' got final status invalid. -[eva] tests/value/va_list2.c:20: - assertion 'Eva,initialization' got final status invalid. [scope:rm_asserts] removing 1 assertion(s) [eva] ====== VALUES COMPUTED ====== [eva:final-states] Values at end of function main: @@ -65,7 +70,8 @@ [from] ====== DEPENDENCIES COMPUTED ====== These dependencies hold at termination for the executions that terminate: [from] Function __builtin_va_arg: - NO EFFECTS + tmp FROM __x0; __x1; tmp; tmp_0 (and SELF) + tmp_0 FROM __x0; __x1; tmp; tmp_0 (and SELF) [from] Function __builtin_va_end: NO EFFECTS [from] Function __builtin_va_start: @@ -74,6 +80,6 @@ NO EFFECTS [from] ====== END OF DEPENDENCIES ====== [inout] Out (internal) for function main: - fmt; i; f + fmt; i; tmp; f; tmp_0 [inout] Inputs for function main: S_fmt[0..1]