[variadic] Update tests for new default machdep

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;

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) {

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 */

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;

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: 

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) {

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) {

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 */