diff --git a/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle b/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle index 7369a68d0b2dff785f411483c5f39da4584de845..8b7c3751760dd97356c018c963be9e2e7b33ef1b 100644 --- a/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle +++ b/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle @@ -53,7 +53,7 @@ int *pack(int first, void * const *__va_params) if (! tmp) break; size ++; } - ret = (int *)malloc(sizeof(int) * (unsigned int)(size + 1)); + ret = (int *)malloc(sizeof(int) * (unsigned long)(size + 1)); *(ret + 0) = first; list = __va_params; i = 0; diff --git a/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle b/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle index 83a0ba4f9cf11e5afd51b149f043b7ed155f2658..f67c309b1b9ea8688ab4937b23366b6d7178504f 100644 --- a/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle +++ b/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle @@ -54,7 +54,7 @@ int *pack(int first, void * const *__va_params) if (! tmp) break; size ++; } - ret = (int *)malloc(sizeof(int) * (unsigned int)(size + 1)); + ret = (int *)malloc(sizeof(int) * (unsigned long)(size + 1)); *(ret + 0) = first; i = 0; while (i < size) { diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle index 5dfc5110fbc51a13382b0667c59193994327797f..cac34c3b81106e48fc46ce258937ba54cea5230e 100644 --- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle +++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle @@ -468,7 +468,7 @@ int printf_va_18(char const * __restrict format, size_t param0, __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))), param0; */ -int printf_va_19(char const * __restrict format, unsigned long long param0); +int printf_va_19(char const * __restrict format, unsigned long param0); /*@ requires valid_read_string(format); assigns \result, __fc_stdout->__fc_FILE_data; @@ -494,7 +494,7 @@ int printf_va_20(char const * __restrict format, int param0); __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))), param0; */ -int printf_va_21(char const * __restrict format, unsigned long long param0); +int printf_va_21(char const * __restrict format, unsigned long param0); /*@ requires valid_read_string(format); assigns \result, __fc_stdout->__fc_FILE_data; @@ -617,9 +617,9 @@ int main(void) uintmax_t uj = (unsigned long long)42; double f = (double)42.0f; long double L = 42.0l; - uint64_t u64 = (unsigned long long)42ul; + uint64_t u64 = 42ul; int8_t i8 = (signed char)42; - uint_least64_t uleast64 = (unsigned long long)42u; + uint_least64_t uleast64 = (unsigned long)42u; int_fast32_t ifast32 = 42; printf("Hello world !\n"); /* printf_va_1 */ printf("%s%n",string,& i); /* printf_va_2 */ @@ -639,9 +639,9 @@ int main(void) printf("%llu ",ull); /* printf_va_16 */ printf("%jo ",uj); /* printf_va_17 */ printf("%zx %tX\n",z,t); /* printf_va_18 */ - printf("%llu",u64); /* printf_va_19 */ + printf("%lu",u64); /* printf_va_19 */ printf("%hhi",(int)i8); /* printf_va_20 */ - printf("%llx",uleast64); /* printf_va_21 */ + printf("%lx",uleast64); /* printf_va_21 */ printf("%d",ifast32); /* printf_va_22 */ printf("%f %Le\n",f,L); /* printf_va_23 */ printf("%c\n",(int)c); /* printf_va_24 */ diff --git a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle index 18e298855651f28719771d12be1b821e2af2e8ee..3cecd8f9b1e42365b8af2c9e3217c941bd59aea4 100644 --- a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle +++ b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle @@ -26,7 +26,7 @@ The imprecision originates from Arithmetic {tests/known/printf_garbled_mix.c:6} [eva:alarm] tests/known/printf_garbled_mix.c:7: Warning: - pointer downcast. assert (unsigned int)b ≤ 2147483647; + pointer downcast. assert (unsigned long)b ≤ 2147483647; [eva] using specification for function printf_va_1 [eva] tests/known/printf_garbled_mix.c:8: Frama_C_show_each_nb_printed: [-2147483648..2147483647] @@ -68,8 +68,8 @@ int printf_va_1(char const * __restrict format, int param0); void main(void) { int a[2] = {1, 2}; - int *b = (int *)((unsigned int)(a) * (unsigned int)2); - /*@ assert Eva: pointer_downcast: (unsigned int)b ≤ 2147483647; */ + int *b = (int *)((unsigned long)(a) * (unsigned long)2); + /*@ assert Eva: pointer_downcast: (unsigned long)b ≤ 2147483647; */ int nb_printed = printf_va_1("%d",(int)b); Frama_C_show_each_nb_printed(nb_printed); b = (int *)0; diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle index e7804a787db53d028ac81c30cf7c26577f43b559..a9e71214ada7413c87b1325f0974ba0acf0d8d72 100644 --- a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle +++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle @@ -438,12 +438,20 @@ int main(void) Incorrect type for argument 2. The argument will be cast from int to unsigned int. [variadic] tests/known/printf_wrong_types.c:21: Translating call to printf to a call to the specialized version printf_va_4. +[variadic] tests/known/printf_wrong_types.c:21: Warning: + Incorrect type for argument 2. The argument will be cast from int to long. [variadic] tests/known/printf_wrong_types.c:22: Translating call to printf to a call to the specialized version printf_va_5. +[variadic] tests/known/printf_wrong_types.c:22: Warning: + Incorrect type for argument 2. The argument will be cast from long to int. [variadic] tests/known/printf_wrong_types.c:23: Translating call to printf to a call to the specialized version printf_va_6. +[variadic] tests/known/printf_wrong_types.c:23: Warning: + Incorrect type for argument 2. The argument will be cast from unsigned int to unsigned long. [variadic] tests/known/printf_wrong_types.c:24: Translating call to printf to a call to the specialized version printf_va_7. +[variadic] tests/known/printf_wrong_types.c:24: Warning: + Incorrect type for argument 2. The argument will be cast from unsigned long to unsigned int. [variadic] tests/known/printf_wrong_types.c:25: Translating call to printf to a call to the specialized version printf_va_8. [variadic] tests/known/printf_wrong_types.c:25: Warning: diff --git a/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle index e8e49846730a17c80917b05866bcf50eea92871e..a55e9b9b9051ebaf7bd0333d33c1eaa6b3cad380 100644 --- a/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle +++ b/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle @@ -84,7 +84,7 @@ int main(void) int __retres; char data[100]; size_t tmp_0; - memset((void *)(data),'A',(unsigned int)99); + memset((void *)(data),'A',(unsigned long)99); data[99] = (char)0; char dest[50] = {(char)'\000'}; if (nondet) { diff --git a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle index 338a605bafc35c6667d7b4da2917eda828ad264c..505fe9d8346afc035f367aaf1005fad87644e19c 100644 --- a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle +++ b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle @@ -97,7 +97,7 @@ int main(void) int __retres; wchar_t data[100]; size_t tmp_0; - wmemset(data,65,(unsigned int)99); + wmemset(data,65,(unsigned long)99); data[99] = 0; wchar_t dest[50] = {0}; if (nondet) { diff --git a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle index 631396fece92093dd91c3a852c1af15dec335c3c..b0188cdf1525b78c8f76532497dad499c2bfd2ff 100644 --- a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle +++ b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle @@ -263,7 +263,7 @@ int main(void) "%" "E" "\\n" ,42.0,42.0,42.0); /* wprintf_va_4 */ wprintf((wchar_t const *)L"%" "*" "d" " " "\\n" ,4,2); /* wprintf_va_5 */ wprintf((wchar_t const *)L"%" "l" "s" " " "\\n" ,(wchar_t *)L"4" "2" ); /* wprintf_va_6 */ - swprintf(wstring,(unsigned int)0x100,(wchar_t const *)L"%" "s" " " "=" " " + swprintf(wstring,(unsigned long)0x100,(wchar_t const *)L"%" "s" " " "=" " " "%" "d" ,(char *)L"4" "2" " " "+" " " "4" "2" ,42 + 42); /* swprintf_va_1 */ wscanf((wchar_t const *)L"%" "l" "s" ,wstring); /* wscanf_va_1 */ wscanf((wchar_t const *)L"%" "d" " " "%" "d" ,& i,& j); /* wscanf_va_2 */