[variadic] Update tests

src/plugins/variadic/tests/known/oracle/fcntl.res.oracle

@@ -59,8 +59,8 @@ int main(void)
   struct flock fl;
   int volatile choice = 0;
   int flags = __va_fcntl_void(0,1);
-  __va_fcntl_int(0,2,flags);
-  __va_fcntl_flock(0,5,& fl);
+  fcntl(0,2,flags); /* __va_fcntl_int */
+  fcntl(0,5,& fl); /* __va_fcntl_flock */
   switch (choice) {
     case 1:
     {
@@ -69,8 +69,8 @@ int main(void)
       void *__va_args[2] = {& __va_arg0, & __va_arg1};
       fcntl(0,2,(void * const *)(__va_args));
     }
-    case 2: __va_fcntl_void(0,2);
-    case 3: __va_fcntl_flock(0,2,& fl);
+    case 2: fcntl(0,2); /* __va_fcntl_void */
+    case 3: fcntl(0,2,& fl); /* __va_fcntl_flock */
     case 4:
     {
       double __va_arg0_9 = 0.5;

src/plugins/variadic/tests/known/oracle/ioctl.res.oracle

@@ -41,8 +41,8 @@ int main(void)
   char arg = (char)42;
   int r2 = __va_ioctl_ptr(fd1,request1,(void *)(& arg));
   struct st *p = (struct st *)0;
-  __va_ioctl_ptr(fd1,request1,(void *)p);
-  __va_ioctl_int(fd1,request1,42);
+  ioctl(fd1,request1,(void *)p); /* __va_ioctl_ptr */
+  ioctl(fd1,request1,42); /* __va_ioctl_int */
   __retres = 0;
   return __retres;
 }

src/plugins/variadic/tests/known/oracle/openat.res.oracle

@@ -40,8 +40,8 @@ int main(void)
   mode_t mode1 = (unsigned int)0;
   int mode2 = 0;
   char *file = (char *)"file";
-  __va_openat_mode_t(0,(char const *)file,flag,mode1);
-  __va_openat_mode_t(0,(char const *)file,flag,(mode_t)mode2);
+  openat(0,(char const *)file,flag,mode1); /* __va_openat_mode_t */
+  openat(0,(char const *)file,flag,(mode_t)mode2); /* __va_openat_mode_t */
   {
     double __va_arg0 = 3.0;
     void *__va_args[1] = {& __va_arg0};

src/plugins/variadic/tests/known/oracle/print_libc.pretty.c

@@ -18,7 +18,7 @@ int printf_va_1(char const * __restrict format);
 int main(void)
 {
   int __retres;
-  printf_va_1("");
+  printf(""); /* printf_va_1 */
   __retres = 0;
   return __retres;
 }
@@ -41,10 +41,22 @@ int main(void)
  */
 int printf_va_1(char const * __restrict format);
 
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
+ */
+int printf_va_1(char const * __restrict format);
+
 int main(void)
 {
   int __retres;
-  printf_va_1("");
+  printf(""); /* printf_va_1 */
   __retres = 0;
   return __retres;
 }

src/plugins/variadic/tests/known/oracle/printf.res.oracle

@@ -621,32 +621,32 @@ int main(void)
   int8_t i8 = (signed char)42;
   uint_least64_t uleast64 = (unsigned long long)42u;
   int_fast32_t ifast32 = 42;
-  printf_va_1("Hello world !\n");
-  printf_va_2("%s%n",string,& i);
-  printf_va_3("%ls",wstring);
-  printf_va_4("%d %hhn",i,& hh);
-  printf_va_5("%hhi %hn",(int)hh,& h);
-  printf_va_6("%hd %ln",(int)h,& l);
-  printf_va_7("%li %lln",l,& ll);
-  printf_va_8("%lld %jn",ll,& j);
-  printf_va_9("%jd %zn",j,& z);
-  printf_va_10("%zd %tn",z,& t);
-  printf_va_11("%td\n",t);
-  printf_va_12("%u ",ui);
-  printf_va_13("%hho ",(int)uhh);
-  printf_va_14("%hx ",(int)uh);
-  printf_va_15("%lX ",ul);
-  printf_va_16("%llu ",ull);
-  printf_va_17("%jo ",uj);
-  printf_va_18("%zx %tX\n",z,t);
-  printf_va_19("%llu",u64);
-  printf_va_20("%hhi",(int)i8);
-  printf_va_21("%llx",uleast64);
-  printf_va_22("%d",ifast32);
-  printf_va_23("%f %Le\n",f,L);
-  printf_va_24("%c\n",(int)c);
-  printf_va_25("%p ",(void *)string);
-  printf_va_26("%d %*.*u\n",1,- (-1),2,ui);
+  printf("Hello world !\n"); /* printf_va_1 */
+  printf("%s%n",string,& i); /* printf_va_2 */
+  printf("%ls",wstring); /* printf_va_3 */
+  printf("%d %hhn",i,& hh); /* printf_va_4 */
+  printf("%hhi %hn",(int)hh,& h); /* printf_va_5 */
+  printf("%hd %ln",(int)h,& l); /* printf_va_6 */
+  printf("%li %lln",l,& ll); /* printf_va_7 */
+  printf("%lld %jn",ll,& j); /* printf_va_8 */
+  printf("%jd %zn",j,& z); /* printf_va_9 */
+  printf("%zd %tn",z,& t); /* printf_va_10 */
+  printf("%td\n",t); /* printf_va_11 */
+  printf("%u ",ui); /* printf_va_12 */
+  printf("%hho ",(int)uhh); /* printf_va_13 */
+  printf("%hx ",(int)uh); /* printf_va_14 */
+  printf("%lX ",ul); /* printf_va_15 */
+  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("%hhi",(int)i8); /* printf_va_20 */
+  printf("%llx",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 */
+  printf("%p ",(void *)string); /* printf_va_25 */
+  printf("%d %*.*u\n",1,- (-1),2,ui); /* printf_va_26 */
   {
     unsigned int __va_arg0 = ui;
     char *__va_arg1 = string;
@@ -656,8 +656,8 @@ int main(void)
            (void * const *)(__va_args));
   }
   char hashes[4] = {(char)'#', (char)'#', (char)'#', (char)'#'};
-  printf_va_27("%.*s",4,hashes);
-  printf_va_28("%.4s",hashes);
+  printf("%.*s",4,hashes); /* printf_va_27 */
+  printf("%.4s",hashes); /* printf_va_28 */
   __retres = 0;
   return __retres;
 }

src/plugins/variadic/tests/known/oracle/printf_redefined.res.oracle

@@ -25,7 +25,7 @@ int printf_va_1(char const * __restrict __format, size_t param0);
 void main(void)
 {
   long x = (long)0;
-  printf_va_1("%zd\n",(size_t)x);
+  printf("%zd\n",(size_t)x); /* printf_va_1 */
   return;
 }
 

src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle

@@ -77,7 +77,7 @@ int main(void)
   int __retres;
   {
     int tmp = 2;
-    printf_va_1("%d",1);
+    printf("%d",1); /* printf_va_1 */
   }
   {
     int __va_arg0 = 1;

src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle

@@ -140,11 +140,11 @@ int main(void)
   wchar_t *wstring = (wchar_t *)L"b" "a" "r" ;
   int volatile nondet = 0;
   switch (nondet) {
-    case 0: printf_va_1("%n",(int *)(& tt));
-    case 1: printf_va_2("%n",(int *)(& ui));
-    case 2: printf_va_3("%hhn",(signed char *)string);
-    case 3: printf_va_4("%s",(char *)wstring);
-    case 4: printf_va_5("%ls",(wchar_t *)string);
+    case 0: printf("%n",(int *)(& tt)); /* printf_va_1 */
+    case 1: printf("%n",(int *)(& ui)); /* printf_va_2 */
+    case 2: printf("%hhn",(signed char *)string); /* printf_va_3 */
+    case 3: printf("%s",(char *)wstring); /* printf_va_4 */
+    case 4: printf("%ls",(wchar_t *)string); /* printf_va_5 */
   }
   __retres = 0;
   return __retres;

src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle

@@ -326,23 +326,23 @@ int main(void)
   float f = 42.0f;
   long double ld = 42.0l;
   char *string = (char *)"42";
-  printf_va_1("%hhd",(int)c);
-  printf_va_2("%d",(int)ui);
-  printf_va_3("%x",(unsigned int)i);
-  printf_va_4("%ld",(long)i);
-  printf_va_5("%d",(int)li);
-  printf_va_6("%lu",(unsigned long)ui);
-  printf_va_7("%u",(unsigned int)uli);
-  printf_va_8("%p",(void *)ui);
-  printf_va_9("%f",(double)f);
-  printf_va_10("%f",(double)ld);
-  printf_va_11("%lf",(double)ld);
-  printf_va_12("%Lf",(long double)((double)f));
-  printf_va_13("%s",(char *)i);
-  printf_va_14("%d",(int)string);
+  printf("%hhd",(int)c); /* printf_va_1 */
+  printf("%d",(int)ui); /* printf_va_2 */
+  printf("%x",(unsigned int)i); /* printf_va_3 */
+  printf("%ld",(long)i); /* printf_va_4 */
+  printf("%d",(int)li); /* printf_va_5 */
+  printf("%lu",(unsigned long)ui); /* printf_va_6 */
+  printf("%u",(unsigned int)uli); /* printf_va_7 */
+  printf("%p",(void *)ui); /* printf_va_8 */
+  printf("%f",(double)f); /* printf_va_9 */
+  printf("%f",(double)ld); /* printf_va_10 */
+  printf("%lf",(double)ld); /* printf_va_11 */
+  printf("%Lf",(long double)((double)f)); /* printf_va_12 */
+  printf("%s",(char *)i); /* printf_va_13 */
+  printf("%d",(int)string); /* printf_va_14 */
   RC rc = OK;
-  printf_va_15("%u",rc);
-  printf_va_16("%d",(int)rc);
+  printf("%u",rc); /* printf_va_15 */
+  printf("%d",(int)rc); /* printf_va_16 */
   __retres = 0;
   return __retres;
 }
@@ -728,23 +728,23 @@ int main(void)
   float f = 42.0f;
   long double ld = 42.0l;
   char *string = (char *)"42";
-  printf_va_1("%hhd",(int)c);
-  printf_va_2("%d",(int)ui);
-  printf_va_3("%x",(unsigned int)i);
-  printf_va_4("%ld",(long)i);
-  printf_va_5("%d",(int)li);
-  printf_va_6("%lu",(unsigned long)ui);
-  printf_va_7("%u",(unsigned int)uli);
-  printf_va_8("%p",(void *)ui);
-  printf_va_9("%f",(double)f);
-  printf_va_10("%f",(double)ld);
-  printf_va_11("%lf",(double)ld);
-  printf_va_12("%Lf",(long double)((double)f));
-  printf_va_13("%s",(char *)i);
-  printf_va_14("%d",(int)string);
+  printf("%hhd",(int)c); /* printf_va_1 */
+  printf("%d",(int)ui); /* printf_va_2 */
+  printf("%x",(unsigned int)i); /* printf_va_3 */
+  printf("%ld",(long)i); /* printf_va_4 */
+  printf("%d",(int)li); /* printf_va_5 */
+  printf("%lu",(unsigned long)ui); /* printf_va_6 */
+  printf("%u",(unsigned int)uli); /* printf_va_7 */
+  printf("%p",(void *)ui); /* printf_va_8 */
+  printf("%f",(double)f); /* printf_va_9 */
+  printf("%f",(double)ld); /* printf_va_10 */
+  printf("%lf",(double)ld); /* printf_va_11 */
+  printf("%Lf",(long double)((double)f)); /* printf_va_12 */
+  printf("%s",(char *)i); /* printf_va_13 */
+  printf("%d",(int)string); /* printf_va_14 */
   RC rc = OK;
-  printf_va_15("%u",rc);
-  printf_va_16("%d",(int)rc);
+  printf("%u",rc); /* printf_va_15 */
+  printf("%d",(int)rc); /* printf_va_16 */
   __retres = 0;
   return __retres;
 }

src/plugins/variadic/tests/known/oracle/scanf.res.oracle

@@ -65,7 +65,7 @@ int main(void)
   int __retres;
   char c[10];
   int i;
-  scanf_va_1("Hello %*10le %% %10s %[^]world] %d !",c,c,& i);
+  scanf("Hello %*10le %% %10s %[^]world] %d !",c,c,& i); /* scanf_va_1 */
   __retres = 0;
   return __retres;
 }

src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle

@@ -53,7 +53,7 @@ int main(void)
   int n;
   while (1) {
     int tmp;
-    tmp = scanf_va_1("%d",& n);
+    tmp = scanf("%d",& n); /* scanf_va_1 */
     if (! (tmp > 0)) break;
     if (nondet) break;
   }

src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle

@@ -68,7 +68,7 @@ int main(void)
   char c[10];
   int i;
   /*@ assert Eva: initialization: \initialized(&d); */
-  scanf_va_1("Hello %*10le %% %10s %[^]world] %d !",(char *)d,c,& i);
+  scanf("Hello %*10le %% %10s %[^]world] %d !",(char *)d,c,& i); /* scanf_va_1 */
   __retres = 0;
   return __retres;
 }

src/plugins/variadic/tests/known/oracle/snprintf.res.oracle

@@ -90,11 +90,11 @@ int main(void)
   if (nondet) {
     size_t tmp;
     tmp = strlen((char const *)(data));
-    snprintf_va_1(dest,tmp,"%s",data);
+    snprintf(dest,tmp,"%s",data); /* snprintf_va_1 */
     /*@ assert \false; */ ;
   }
   tmp_0 = strlen((char const *)(data));
-  snprintf_va_2(dest,tmp_0 / (size_t)2,"%s",data);
+  snprintf(dest,tmp_0 / (size_t)2,"%s",data); /* snprintf_va_2 */
   __retres = 0;
   return __retres;
 }

src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle

@@ -185,11 +185,11 @@ int main(void)
     void *__va_args_40[3] = {& __va_arg0_34, & __va_arg1_36, & __va_arg2_38};
     dprintf(1,(char const *)format,(void * const *)(__va_args_40));
   }
-  fprintf_va_1(stream,"%d %s %d",1,(char *)"2",3);
-  printf_va_1("%d %s %d",1,(char *)"2",3);
-  snprintf_va_1(str,size,"%d %s %d",1,(char *)"2",3);
-  sprintf_va_1(str,"%d %s %d",1,(char *)"2",3);
-  dprintf_va_1(1,"%d %s %s",1,(char *)"3",(char *)"4");
+  fprintf(stream,"%d %s %d",1,(char *)"2",3); /* fprintf_va_1 */
+  printf("%d %s %d",1,(char *)"2",3); /* printf_va_1 */
+  snprintf(str,size,"%d %s %d",1,(char *)"2",3); /* snprintf_va_1 */
+  sprintf(str,"%d %s %d",1,(char *)"2",3); /* sprintf_va_1 */
+  dprintf(1,"%d %s %s",1,(char *)"3",(char *)"4"); /* dprintf_va_1 */
   __retres = 0;
   return __retres;
 }

src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle

@@ -156,9 +156,9 @@ int main(void)
     sscanf((char const *)str,(char const *)format,
            (void * const *)(__va_args_26));
   }
-  fscanf_va_1(stream,"%d %s %d",& i,s,& j);
-  scanf_va_1("%d %s %d",& i,s,& j);
-  sscanf_va_1((char const *)str,"%d %s %d",& i,s,& j);
+  fscanf(stream,"%d %s %d",& i,s,& j); /* fscanf_va_1 */
+  scanf("%d %s %d",& i,s,& j); /* scanf_va_1 */
+  sscanf((char const *)str,"%d %s %d",& i,s,& j); /* sscanf_va_1 */
   __retres = 0;
   return __retres;
 }

src/plugins/variadic/tests/known/oracle/swprintf.res.oracle

@@ -103,11 +103,11 @@ int main(void)
   if (nondet) {
     size_t tmp;
     tmp = wcslen((wchar_t const *)(data));
-    swprintf_va_1(dest,tmp,(wchar_t const *)L"%" "l" "s" ,data);
+    swprintf(dest,tmp,(wchar_t const *)L"%" "l" "s" ,data); /* swprintf_va_1 */
     /*@ assert \false; */ ;
   }
   tmp_0 = wcslen((wchar_t const *)(data));
-  swprintf_va_2(dest,tmp_0 / (size_t)2,(wchar_t const *)L"%" "l" "s" ,data);
+  swprintf(dest,tmp_0 / (size_t)2,(wchar_t const *)L"%" "l" "s" ,data); /* swprintf_va_2 */
   __retres = 0;
   return __retres;
 }

src/plugins/variadic/tests/known/oracle/wchar.res.oracle

@@ -254,21 +254,21 @@ int main(void)
   int j;
   wchar_t input[0x100] =
     {102, 111, 114, 116, 121, 45, 116, 119, 111, 32, 105, 115, 0};
-  wprintf_va_1((wchar_t const *)L"%" "d" " " "%" "l" "d" "\\n" ,42,42L);
-  wprintf_va_2((wchar_t const *)L"%" "1" "0" "d" " " "%" "0" "1" "0" "d"
-               "\\n" ,42,42);
-  wprintf_va_3((wchar_t const *)L"%" "d" " " "%" "x" " " "%" "o" " " "%" "#"
-               "x" " " "%" "#" "o" "\\n" ,42,42u,42u,42u,42u);
-  wprintf_va_4((wchar_t const *)L"%" "2" "." "1" "f" " " "%" "+" "." "0" "e"
-               " " "%" "E" "\\n" ,42.0,42.0,42.0);
-  wprintf_va_5((wchar_t const *)L"%" "*" "d" " " "\\n" ,4,2);
-  wprintf_va_6((wchar_t const *)L"%" "l" "s" " " "\\n" ,(wchar_t *)L"4" "2" );
-  swprintf_va_1(wstring,(unsigned int)0x100,(wchar_t const *)L"%" "s" " " "="
-                " " "%" "d" ,(char *)L"4" "2" " " "+" " " "4" "2" ,42 + 42);
-  wscanf_va_1((wchar_t const *)L"%" "l" "s" ,wstring);
-  wscanf_va_2((wchar_t const *)L"%" "d" " " "%" "d" ,& i,& j);
-  swscanf_va_1((wchar_t const *)(input),(wchar_t const *)L"%" "l" "s" " " "%"
-               "*" "s" " " "%" "d" ,wstring,& i);
+  wprintf((wchar_t const *)L"%" "d" " " "%" "l" "d" "\\n" ,42,42L); /* wprintf_va_1 */
+  wprintf((wchar_t const *)L"%" "1" "0" "d" " " "%" "0" "1" "0" "d" "\\n" ,
+          42,42); /* wprintf_va_2 */
+  wprintf((wchar_t const *)L"%" "d" " " "%" "x" " " "%" "o" " " "%" "#" "x"
+          " " "%" "#" "o" "\\n" ,42,42u,42u,42u,42u); /* wprintf_va_3 */
+  wprintf((wchar_t const *)L"%" "2" "." "1" "f" " " "%" "+" "." "0" "e" " "
+          "%" "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" " " "=" " "
+           "%" "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 */
+  swscanf((wchar_t const *)(input),(wchar_t const *)L"%" "l" "s" " " "%" "*"
+          "s" " " "%" "d" ,wstring,& i); /* swscanf_va_1 */
   __retres = 0;
   return __retres;
 }

tests/libc/oracle/inttypes_h.0.res.oracle

@@ -2531,255 +2531,255 @@ int main(void)
   int __retres;
   {
     int8_t x;
-    scanf_va_1("%hhd",(signed char *)(& x));
-    printf_va_1("%hhd",(int)x);
-    scanf_va_2("%hhi",(signed char *)(& x));
-    printf_va_2("%hhi",(int)x);
+    scanf("%hhd",(signed char *)(& x)); /* scanf_va_1 */
+    printf("%hhd",(int)x); /* printf_va_1 */
+    scanf("%hhi",(signed char *)(& x)); /* scanf_va_2 */
+    printf("%hhi",(int)x); /* printf_va_2 */
   }
   {
     uint8_t x_0;
-    scanf_va_3("%hho",(unsigned char *)(& x_0));
-    printf_va_3("%hho",(int)x_0);
-    scanf_va_4("%hhu",(unsigned char *)(& x_0));
-    printf_va_4("%hhu",(int)x_0);
-    scanf_va_5("%hhx",(unsigned char *)(& x_0));
-    printf_va_5("%hhx",(int)x_0);
-    scanf_va_6("%hhx",(unsigned char *)(& x_0));
-    printf_va_6("%hhX",(int)x_0);
+    scanf("%hho",(unsigned char *)(& x_0)); /* scanf_va_3 */
+    printf("%hho",(int)x_0); /* printf_va_3 */
+    scanf("%hhu",(unsigned char *)(& x_0)); /* scanf_va_4 */
+    printf("%hhu",(int)x_0); /* printf_va_4 */
+    scanf("%hhx",(unsigned char *)(& x_0)); /* scanf_va_5 */
+    printf("%hhx",(int)x_0); /* printf_va_5 */
+    scanf("%hhx",(unsigned char *)(& x_0)); /* scanf_va_6 */
+    printf("%hhX",(int)x_0); /* printf_va_6 */
   }
   {
     int16_t x_1;
-    scanf_va_7("%hd",(short *)(& x_1));
-    printf_va_7("%hd",(int)x_1);
-    scanf_va_8("%hi",(short *)(& x_1));
-    printf_va_8("%hi",(int)x_1);
+    scanf("%hd",(short *)(& x_1)); /* scanf_va_7 */
+    printf("%hd",(int)x_1); /* printf_va_7 */
+    scanf("%hi",(short *)(& x_1)); /* scanf_va_8 */
+    printf("%hi",(int)x_1); /* printf_va_8 */
   }
   {
     uint16_t x_2;
-    scanf_va_9("%ho",(unsigned short *)(& x_2));
-    printf_va_9("%ho",(unsigned int)x_2);
-    scanf_va_10("%hu",(unsigned short *)(& x_2));
-    printf_va_10("%hu",(unsigned int)x_2);
-    scanf_va_11("%hx",(unsigned short *)(& x_2));
-    printf_va_11("%hx",(unsigned int)x_2);
-    scanf_va_12("%hx",(unsigned short *)(& x_2));
-    printf_va_12("%hX",(unsigned int)x_2);
+    scanf("%ho",(unsigned short *)(& x_2)); /* scanf_va_9 */
+    printf("%ho",(unsigned int)x_2); /* printf_va_9 */
+    scanf("%hu",(unsigned short *)(& x_2)); /* scanf_va_10 */
+    printf("%hu",(unsigned int)x_2); /* printf_va_10 */
+    scanf("%hx",(unsigned short *)(& x_2)); /* scanf_va_11 */
+    printf("%hx",(unsigned int)x_2); /* printf_va_11 */
+    scanf("%hx",(unsigned short *)(& x_2)); /* scanf_va_12 */
+    printf("%hX",(unsigned int)x_2); /* printf_va_12 */
   }
   {
     int32_t x_3;
-    scanf_va_13("%ld",(long *)(& x_3));
-    printf_va_13("%ld",x_3);
-    scanf_va_14("%li",(long *)(& x_3));
-    printf_va_14("%li",x_3);
+    scanf("%ld",(long *)(& x_3)); /* scanf_va_13 */
+    printf("%ld",x_3); /* printf_va_13 */
+    scanf("%li",(long *)(& x_3)); /* scanf_va_14 */
+    printf("%li",x_3); /* printf_va_14 */
   }
   {
     uint32_t x_4;
-    scanf_va_15("%lo",(unsigned long *)(& x_4));
-    printf_va_15("%lo",x_4);
-    scanf_va_16("%lu",(unsigned long *)(& x_4));
-    printf_va_16("%lu",x_4);
-    scanf_va_17("%lx",(unsigned long *)(& x_4));
-    printf_va_17("%lx",x_4);
-    scanf_va_18("%lx",(unsigned long *)(& x_4));
-    printf_va_18("%lX",x_4);
+    scanf("%lo",(unsigned long *)(& x_4)); /* scanf_va_15 */
+    printf("%lo",x_4); /* printf_va_15 */
+    scanf("%lu",(unsigned long *)(& x_4)); /* scanf_va_16 */
+    printf("%lu",x_4); /* printf_va_16 */
+    scanf("%lx",(unsigned long *)(& x_4)); /* scanf_va_17 */
+    printf("%lx",x_4); /* printf_va_17 */
+    scanf("%lx",(unsigned long *)(& x_4)); /* scanf_va_18 */
+    printf("%lX",x_4); /* printf_va_18 */
   }
   {
     int64_t x_5;
-    scanf_va_19("%lld",(long long *)(& x_5));
-    printf_va_19("%lld",x_5);
-    scanf_va_20("%lli",(long long *)(& x_5));
-    printf_va_20("%lli",x_5);
+    scanf("%lld",(long long *)(& x_5)); /* scanf_va_19 */
+    printf("%lld",x_5); /* printf_va_19 */
+    scanf("%lli",(long long *)(& x_5)); /* scanf_va_20 */
+    printf("%lli",x_5); /* printf_va_20 */
   }
   {
     uint64_t x_6;
-    scanf_va_21("%llo",(unsigned long long *)(& x_6));
-    printf_va_21("%llo",x_6);
-    scanf_va_22("%llu",(unsigned long long *)(& x_6));
-    printf_va_22("%llu",x_6);
-    scanf_va_23("%llx",(unsigned long long *)(& x_6));
-    printf_va_23("%llx",x_6);
-    scanf_va_24("%llx",(unsigned long long *)(& x_6));
-    printf_va_24("%llX",x_6);
+    scanf("%llo",(unsigned long long *)(& x_6)); /* scanf_va_21 */
+    printf("%llo",x_6); /* printf_va_21 */
+    scanf("%llu",(unsigned long long *)(& x_6)); /* scanf_va_22 */
+    printf("%llu",x_6); /* printf_va_22 */
+    scanf("%llx",(unsigned long long *)(& x_6)); /* scanf_va_23 */
+    printf("%llx",x_6); /* printf_va_23 */
+    scanf("%llx",(unsigned long long *)(& x_6)); /* scanf_va_24 */
+    printf("%llX",x_6); /* printf_va_24 */
   }
   {
     int_least8_t x_7;
-    scanf_va_25("%hhd",(signed char *)(& x_7));
-    printf_va_25("%hhd",(int)x_7);
-    scanf_va_26("%hhi",(signed char *)(& x_7));
-    printf_va_26("%hhi",(int)x_7);
+    scanf("%hhd",(signed char *)(& x_7)); /* scanf_va_25 */
+    printf("%hhd",(int)x_7); /* printf_va_25 */
+    scanf("%hhi",(signed char *)(& x_7)); /* scanf_va_26 */
+    printf("%hhi",(int)x_7); /* printf_va_26 */
   }
   {
     uint_least8_t x_8;
-    scanf_va_27("%hho",(unsigned char *)(& x_8));
-    printf_va_27("%hho",(int)x_8);
-    scanf_va_28("%hhu",(unsigned char *)(& x_8));
-    printf_va_28("%hhu",(int)x_8);
-    scanf_va_29("%hhx",(unsigned char *)(& x_8));
-    printf_va_29("%hhx",(int)x_8);
-    scanf_va_30("%hhx",(unsigned char *)(& x_8));
-    printf_va_30("%hhX",(int)x_8);
+    scanf("%hho",(unsigned char *)(& x_8)); /* scanf_va_27 */
+    printf("%hho",(int)x_8); /* printf_va_27 */
+    scanf("%hhu",(unsigned char *)(& x_8)); /* scanf_va_28 */
+    printf("%hhu",(int)x_8); /* printf_va_28 */
+    scanf("%hhx",(unsigned char *)(& x_8)); /* scanf_va_29 */
+    printf("%hhx",(int)x_8); /* printf_va_29 */
+    scanf("%hhx",(unsigned char *)(& x_8)); /* scanf_va_30 */
+    printf("%hhX",(int)x_8); /* printf_va_30 */
   }
   {
     int_least16_t x_9;
-    scanf_va_31("%hd",(short *)(& x_9));
-    printf_va_31("%hd",(int)x_9);
-    scanf_va_32("%hi",(short *)(& x_9));
-    printf_va_32("%hi",(int)x_9);
+    scanf("%hd",(short *)(& x_9)); /* scanf_va_31 */
+    printf("%hd",(int)x_9); /* printf_va_31 */
+    scanf("%hi",(short *)(& x_9)); /* scanf_va_32 */
+    printf("%hi",(int)x_9); /* printf_va_32 */
   }
   {
     uint_least16_t x_10;
-    scanf_va_33("%ho",(unsigned short *)(& x_10));
-    printf_va_33("%ho",(unsigned int)x_10);
-    scanf_va_34("%hu",(unsigned short *)(& x_10));
-    printf_va_34("%hu",(unsigned int)x_10);
-    scanf_va_35("%hx",(unsigned short *)(& x_10));
-    printf_va_35("%hx",(unsigned int)x_10);
-    scanf_va_36("%hx",(unsigned short *)(& x_10));
-    printf_va_36("%hX",(unsigned int)x_10);
+    scanf("%ho",(unsigned short *)(& x_10)); /* scanf_va_33 */
+    printf("%ho",(unsigned int)x_10); /* printf_va_33 */
+    scanf("%hu",(unsigned short *)(& x_10)); /* scanf_va_34 */
+    printf("%hu",(unsigned int)x_10); /* printf_va_34 */
+    scanf("%hx",(unsigned short *)(& x_10)); /* scanf_va_35 */
+    printf("%hx",(unsigned int)x_10); /* printf_va_35 */
+    scanf("%hx",(unsigned short *)(& x_10)); /* scanf_va_36 */
+    printf("%hX",(unsigned int)x_10); /* printf_va_36 */
   }
   {
     int_least32_t x_11;
-    scanf_va_37("%ld",(long *)(& x_11));
-    printf_va_37("%ld",x_11);
-    scanf_va_38("%li",(long *)(& x_11));
-    printf_va_38("%li",x_11);
+    scanf("%ld",(long *)(& x_11)); /* scanf_va_37 */
+    printf("%ld",x_11); /* printf_va_37 */
+    scanf("%li",(long *)(& x_11)); /* scanf_va_38 */
+    printf("%li",x_11); /* printf_va_38 */
   }
   {
     uint_least32_t x_12;
-    scanf_va_39("%lo",(unsigned long *)(& x_12));
-    printf_va_39("%lo",x_12);
-    scanf_va_40("%lu",(unsigned long *)(& x_12));
-    printf_va_40("%lu",x_12);
-    scanf_va_41("%lx",(unsigned long *)(& x_12));
-    printf_va_41("%lx",x_12);
-    scanf_va_42("%lx",(unsigned long *)(& x_12));
-    printf_va_42("%lX",x_12);
+    scanf("%lo",(unsigned long *)(& x_12)); /* scanf_va_39 */
+    printf("%lo",x_12); /* printf_va_39 */
+    scanf("%lu",(unsigned long *)(& x_12)); /* scanf_va_40 */
+    printf("%lu",x_12); /* printf_va_40 */
+    scanf("%lx",(unsigned long *)(& x_12)); /* scanf_va_41 */