[variadic][eacsl] Update tests

src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcmp.c

@@ -116,21 +116,7 @@ char *__gen_e_acsl_strdup(char const *s);
 __inline static void fail_ncomp(int cond, char *fmt, int l, int r)
 {
   if (cond) {
-    {
-      int __va_arg0 = l;
-      __e_acsl_store_block((void *)(& __va_arg0),(size_t)4);
-      __e_acsl_full_init((void *)(& __va_arg0));
-      int __va_arg1 = r;
-      __e_acsl_store_block((void *)(& __va_arg1),(size_t)4);
-      __e_acsl_full_init((void *)(& __va_arg1));
-      void *__va_args[2] = {& __va_arg0, & __va_arg1};
-      __e_acsl_store_block((void *)(__va_args),(size_t)16);
-      __e_acsl_full_init((void *)(& __va_args));
-      fprintf(stderr,(char const *)fmt,(void * const *)(__va_args));
-      __e_acsl_delete_block((void *)(__va_args));
-      __e_acsl_delete_block((void *)(& __va_arg1));
-      __e_acsl_delete_block((void *)(& __va_arg0));
-    }
+    fprintf(stderr,(char const *)fmt,l,r); /* fprintf_fallback_1 */
     __gen_e_acsl_abort();
   }
   return;

src/plugins/variadic/tests/erroneous/oracle/exec.res.oracle

@@ -11,11 +11,11 @@
 [variadic] tests/erroneous/exec.c:7: Warning: 
   Failed to find a sentinel (NULL pointer) in the argument list.
 [variadic] tests/erroneous/exec.c:7: 
-  Generic translation of call to variadic function.
+  Fallback translation of call execlp to a call to the specialized version execlp_fallback_1.
 [variadic] tests/erroneous/exec.c:9: Warning: 
   Not enough arguments: expected 5, given 4.
 [variadic] tests/erroneous/exec.c:9: 
-  Generic translation of call to variadic function.
+  Fallback translation of call execle to a call to the specialized version execle_fallback_1.
 [variadic] tests/erroneous/exec.c:11: Warning: 
   Incorrect type for argument 5. The argument will be cast from int to char * const *.
 [variadic] tests/erroneous/exec.c:11: 

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

@@ -18,4 +18,4 @@
 [variadic] tests/erroneous/printf.c:8: Warning: 
   Flag ' ' and conversion specififer e are not compatibles.
 [variadic] tests/erroneous/printf.c:8: 
-  Generic translation of call to variadic function.
+  Fallback translation of call printf to a call to the specialized version printf_fallback_1.

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

@@ -19,14 +19,19 @@
 [variadic] tests/known/exec.c:15: Warning: 
   Failed to find a sentinel (NULL pointer) in the argument list.
 [variadic] tests/known/exec.c:15: 
-  Generic translation of call to variadic function.
+  Fallback translation of call execlp to a call to the specialized version execlp_fallback_1.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
 [eva] using specification for function execve
 [eva] using specification for function execv
 [eva] using specification for function execvp
-[eva] using specification for function execlp
+[kernel:annot:missing-spec] tests/known/exec.c:15: Warning: 
+  Neither code nor specification for function execlp_fallback_1, generating default assigns from the prototype
+[eva] using specification for function execlp_fallback_1
+[eva:invalid-assigns] tests/known/exec.c:15: 
+  Completely invalid destination for assigns clause *(param1 + (0 ..)).
+  Ignoring.
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
@@ -36,6 +41,17 @@
   __retres ∈ {0}
 /* Generated by Frama-C */
 #include "unistd.h"
+/*@ assigns \result, *(param1 + (0 ..));
+    assigns \result
+      \from *(path + (0 ..)), *(arg + (0 ..)), *(param0 + (0 ..)),
+            *(param1 + (0 ..));
+    assigns *(param1 + (0 ..))
+      \from *(path + (0 ..)), *(arg + (0 ..)), *(param0 + (0 ..)),
+            *(param1 + (0 ..));
+ */
+int execlp_fallback_1(char const *path, char const *arg, char const *param0,
+                      char *param1);
+
 int main(void)
 {
   int __retres;
@@ -63,12 +79,7 @@ int main(void)
     void *tmp_16 = (void *)0;
     execve("ls",argv_12,(char * const *)(env));
   }
-  {
-    char const *__va_arg0 = "--reverse";
-    char *__va_arg1 = sentinel;
-    void *__va_args[2] = {& __va_arg0, & __va_arg1};
-    execlp("ls","ls",(void * const *)(__va_args));
-  }
+  execlp("ls","ls","--reverse",sentinel); /* execlp_fallback_1 */
   __retres = 0;
   return __retres;
 }

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

@@ -18,7 +18,7 @@
   Given arguments:
          fcntl(int, int, int, int)
 [variadic] tests/known/fcntl.c:16: 
-  Generic translation of call to variadic function.
+  Fallback translation of call fcntl to a call to the specialized version fcntl_fallback_1.
 [variadic] tests/known/fcntl.c:20: 
   Translating call to the specialized version fcntl(int, int).
 [variadic] tests/known/fcntl.c:24: 
@@ -32,18 +32,23 @@
   Given arguments:
          fcntl(int, int, double)
 [variadic] tests/known/fcntl.c:28: 
-  Generic translation of call to variadic function.
+  Fallback translation of call fcntl to a call to the specialized version fcntl_fallback_2.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
 [eva] using specification for function __va_fcntl_void
 [eva] using specification for function __va_fcntl_int
 [eva] using specification for function __va_fcntl_flock
-[eva] using specification for function fcntl
+[kernel:annot:missing-spec] tests/known/fcntl.c:16: Warning: 
+  Neither code nor specification for function fcntl_fallback_1, generating default assigns from the prototype
+[eva] using specification for function fcntl_fallback_1
 [eva:alarm] tests/known/fcntl.c:20: Warning: 
   function __va_fcntl_void: precondition 'cmd_has_void_arg' got status invalid.
 [eva:alarm] tests/known/fcntl.c:24: Warning: 
   function __va_fcntl_flock: precondition 'cmd_as_flock_arg' got status invalid.
+[kernel:annot:missing-spec] tests/known/fcntl.c:28: Warning: 
+  Neither code nor specification for function fcntl_fallback_2, generating default assigns from the prototype
+[eva] using specification for function fcntl_fallback_2
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
@@ -53,6 +58,14 @@
   __retres ∈ {0}
 /* Generated by Frama-C */
 #include "fcntl.h"
+/*@ assigns \result;
+    assigns \result \from fd, cmd, param0, param1; */
+int fcntl_fallback_1(int fd, int cmd, int param0, int param1);
+
+/*@ assigns \result;
+    assigns \result \from fd, cmd, param0; */
+int fcntl_fallback_2(int fd, int cmd, double param0);
+
 int main(void)
 {
   int __retres;
@@ -62,21 +75,10 @@ int main(void)
   fcntl(0,2,flags); /* __va_fcntl_int */
   fcntl(0,5,& fl); /* __va_fcntl_flock */
   switch (choice) {
-    case 1:
-    {
-      int __va_arg0 = flags;
-      int __va_arg1 = 5;
-      void *__va_args[2] = {& __va_arg0, & __va_arg1};
-      fcntl(0,2,(void * const *)(__va_args));
-    }
+    case 1: fcntl(0,2,flags,5); /* fcntl_fallback_1 */
     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;
-      void *__va_args_11[1] = {& __va_arg0_9};
-      fcntl(0,2,(void * const *)(__va_args_11));
-    }
+    case 4: fcntl(0,2,0.5); /* fcntl_fallback_2 */
   }
   __retres = 0;
   return __retres;

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

@@ -17,13 +17,15 @@
   Given arguments:
          open(char const *, int, int, int, char const *, int)
 [variadic] tests/known/open.c:9: 
-  Generic translation of call to variadic function.
+  Fallback translation of call open to a call to the specialized version open_fallback_1.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
 [eva] using specification for function __va_open_mode_t
 [eva] using specification for function __va_open_void
-[eva] using specification for function open
+[kernel:annot:missing-spec] tests/known/open.c:9: Warning: 
+  Neither code nor specification for function open_fallback_1, generating default assigns from the prototype
+[eva] using specification for function open_fallback_1
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
@@ -32,18 +34,18 @@
   file ∈ {{ "file" }}
   fd1 ∈ [-1..1023]
   fd2 ∈ [-1..1023]
-  fd3 ∈ [-1..1023]
-  __va_arg0 ∈ {0}
-  __va_arg1 ∈ {3}
-  __va_arg2 ∈ {{ "arg4" }}
-  __va_arg3 ∈ {5}
-  __va_args[0] ∈ {{ (void *)&__va_arg0 }}
-           [1] ∈ {{ (void *)&__va_arg1 }}
-           [2] ∈ {{ (void *)&__va_arg2 }}
-           [3] ∈ {{ (void *)&__va_arg3 }}
+  fd3 ∈ [--..--]
   __retres ∈ {0}
 /* Generated by Frama-C */
 #include "fcntl.h"
+/*@ assigns \result;
+    assigns \result
+      \from *(filename + (0 ..)), *(param2 + (0 ..)), flags, param0, param1,
+            param3;
+ */
+int open_fallback_1(char const *filename, int flags, int param0, int param1,
+                    char const *param2, int param3);
+
 int main(void)
 {
   int __retres;
@@ -52,12 +54,7 @@ int main(void)
   char *file = (char *)"file";
   int fd1 = __va_open_mode_t((char const *)file,flag,(mode_t)mode);
   int fd2 = __va_open_void((char const *)file,flag);
-  int __va_arg0 = mode;
-  int __va_arg1 = 3;
-  char const *__va_arg2 = "arg4";
-  int __va_arg3 = 5;
-  void *__va_args[4] = {& __va_arg0, & __va_arg1, & __va_arg2, & __va_arg3};
-  int fd3 = open((char const *)file,flag,(void * const *)(__va_args));
+  int fd3 = open_fallback_1((char const *)file,flag,mode,3,"arg4",5);
   __retres = 0;
   return __retres;
 }

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

@@ -11,11 +11,13 @@
   Given arguments:
          open(char const *, int, char const *)
 [variadic] tests/known/open_wrong.c:13: 
-  Generic translation of call to variadic function.
+  Fallback translation of call open to a call to the specialized version open_fallback_1.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
-[eva] using specification for function open
+[kernel:annot:missing-spec] tests/known/open_wrong.c:13: Warning: 
+  Neither code nor specification for function open_fallback_1, generating default assigns from the prototype
+[eva] using specification for function open_fallback_1
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
@@ -24,16 +26,17 @@
   __retres ∈ {0}
 /* Generated by Frama-C */
 #include "fcntl.h"
+/*@ assigns \result;
+    assigns \result \from *(filename + (0 ..)), *(param0 + (0 ..)), flags;
+ */
+int open_fallback_1(char const *filename, int flags, char const *param0);
+
 int main(void)
 {
   int __retres;
   char *file = (char *)"file";
   int flag = 0;
-  {
-    char const *__va_arg0 = "";
-    void *__va_args[1] = {& __va_arg0};
-    open((char const *)file,flag,(void * const *)(__va_args));
-  }
+  open((char const *)file,flag,""); /* open_fallback_1 */
   __retres = 0;
   return __retres;
 }

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

@@ -17,12 +17,14 @@
   Given arguments:
          openat(int, char const *, int, double)
 [variadic] tests/known/openat.c:10: 
-  Generic translation of call to variadic function.
+  Fallback translation of call openat to a call to the specialized version openat_fallback_1.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
 [eva] using specification for function __va_openat_mode_t
-[eva] using specification for function openat
+[kernel:annot:missing-spec] tests/known/openat.c:10: Warning: 
+  Neither code nor specification for function openat_fallback_1, generating default assigns from the prototype
+[eva] using specification for function openat_fallback_1
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
@@ -33,6 +35,12 @@
   __retres ∈ {0}
 /* Generated by Frama-C */
 #include "fcntl.h"
+/*@ assigns \result;
+    assigns \result \from *(filename + (0 ..)), dirfd, flags, param0;
+ */
+int openat_fallback_1(int dirfd, char const *filename, int flags,
+                      double param0);
+
 int main(void)
 {
   int __retres;
@@ -42,11 +50,7 @@ int main(void)
   char *file = (char *)"file";
   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};
-    openat(0,(char const *)file,flag,(void * const *)(__va_args));
-  }
+  openat(0,(char const *)file,flag,3.0); /* openat_fallback_1 */
   __retres = 0;
   return __retres;
 }

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

@@ -81,7 +81,7 @@
 [variadic] tests/known/printf.c:71: Warning: 
   Flag ' ' and conversion specififer x are not compatibles.
 [variadic] tests/known/printf.c:71: 
-  Generic translation of call to variadic function.
+  Fallback translation of call printf to a call to the specialized version printf_fallback_1.
 [variadic] tests/known/printf.c:74: 
   Translating call to printf to a call to the specialized version printf_va_27.
 [variadic] tests/known/printf.c:75: 
@@ -116,8 +116,11 @@
 [eva] using specification for function printf_va_25
 [eva] using specification for function printf_va_26
 [kernel:annot:missing-spec] tests/known/printf.c:71: Warning: 
-  Neither code nor specification for function printf, generating default assigns from the prototype
-[eva] using specification for function printf
+  Neither code nor specification for function printf_fallback_1, generating default assigns from the prototype
+[eva] using specification for function printf_fallback_1
+[eva:invalid-assigns] tests/known/printf.c:71: 
+  Completely invalid destination for assigns clause *(param1 + (0 ..)).
+  Ignoring.
 [eva] using specification for function printf_va_27
 [eva] using specification for function printf_va_28
 [eva] done for function main
@@ -562,6 +565,15 @@ int printf_va_25(char const * restrict format, void *param0);
 int printf_va_26(char const * restrict format, int param0, int param1,
                  int param2, unsigned int param3);
 
+/*@ assigns \result, *(param1 + (0 ..));
+    assigns \result
+      \from *(format + (0 ..)), *(param1 + (0 ..)), param0, param2;
+    assigns *(param1 + (0 ..))
+      \from *(format + (0 ..)), *(param1 + (0 ..)), param0, param2;
+ */
+int printf_fallback_1(char const * restrict format, unsigned int param0,
+                      char *param1, int param2);
+
 /*@ requires valid_read_nstring(param1, param0);
     requires valid_read_string(format);
     assigns \result, __fc_stdout->__fc_FILE_data;
@@ -644,14 +656,7 @@ int main(void)
   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;
-    int __va_arg2 = 42;
-    void *__va_args[3] = {& __va_arg0, & __va_arg1, & __va_arg2};
-    printf("Hello %- 0+#20.10lx %% %s world %d !",
-           (void * const *)(__va_args));
-  }
+  printf("Hello %- 0+#20.10lx %% %s world %d !",ui,string,42); /* printf_fallback_1 */
   char hashes[4] = {(char)'#', (char)'#', (char)'#', (char)'#'};
   printf("%.*s",4,hashes); /* printf_va_27 */
   printf("%.4s",hashes); /* printf_va_28 */

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

@@ -23,14 +23,14 @@
 [variadic] tests/known/printf_wrong_arity.c:9: Warning: 
   Not enough arguments: expected 3, given 2.
 [variadic] tests/known/printf_wrong_arity.c:9: 
-  Generic translation of call to variadic function.
+  Fallback translation of call printf to a call to the specialized version printf_va_2_fallback_1.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
 [eva] using specification for function printf_va_1
 [kernel:annot:missing-spec] tests/known/printf_wrong_arity.c:9: Warning: 
-  Neither code nor specification for function printf, generating default assigns from the prototype
-[eva] using specification for function printf
+  Neither code nor specification for function printf_va_2_fallback_1, generating default assigns from the prototype
+[eva] using specification for function printf_va_2_fallback_1
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
@@ -72,6 +72,10 @@ int printf_va_1(char const * restrict format, int param0);
  */
 int printf_va_2(char const * restrict format, int param0, int param1);
 
+/*@ assigns \result;
+    assigns \result \from *(format + (0 ..)), param0; */
+int printf_va_2_fallback_1(char const * restrict format, int param0);
+
 int main(void)
 {
   int __retres;
@@ -79,11 +83,7 @@ int main(void)
     int tmp = 2;
     printf("%d",1); /* printf_va_1 */
   }
-  {
-    int __va_arg0 = 1;
-    void *__va_args[1] = {& __va_arg0};
-    printf("%d %d",(void * const *)(__va_args));
-  }
+  printf("%d %d",1); /* printf_va_2_fallback_1 */
   __retres = 0;
   return __retres;
 }

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

@@ -18,27 +18,27 @@
   Call to function fprintf with non-static format argument:
   no specification will be generated.
 [variadic] tests/known/stdio_print.c:9: 
-  Generic translation of call to variadic function.
+  Fallback translation of call fprintf to a call to the specialized version fprintf_fallback_1.
 [variadic] tests/known/stdio_print.c:10: Warning: 
   Call to function printf with non-static format argument:
   no specification will be generated.
 [variadic] tests/known/stdio_print.c:10: 
-  Generic translation of call to variadic function.
+  Fallback translation of call printf to a call to the specialized version printf_fallback_1.
 [variadic] tests/known/stdio_print.c:11: Warning: 
   Call to function snprintf with non-static format argument:
   no specification will be generated.
 [variadic] tests/known/stdio_print.c:11: 
-  Generic translation of call to variadic function.
+  Fallback translation of call snprintf to a call to the specialized version snprintf_fallback_1.
 [variadic] tests/known/stdio_print.c:12: Warning: 
   Call to function sprintf with non-static format argument:
   no specification will be generated.
 [variadic] tests/known/stdio_print.c:12: 
-  Generic translation of call to variadic function.
+  Fallback translation of call sprintf to a call to the specialized version sprintf_fallback_1.
 [variadic] tests/known/stdio_print.c:13: Warning: 
   Call to function dprintf with non-static format argument:
   no specification will be generated.
 [variadic] tests/known/stdio_print.c:13: 
-  Generic translation of call to variadic function.
+  Fallback translation of call dprintf to a call to the specialized version dprintf_fallback_1.
 [variadic] tests/known/stdio_print.c:15: 
   Translating call to fprintf to a call to the specialized version fprintf_va_1.
 [variadic] tests/known/stdio_print.c:16: 
@@ -58,7 +58,7 @@
 [eva] tests/known/stdio_print.c:9: 
   assertion 'Eva,initialization' got final status invalid.
 [kernel:annot:missing-spec] tests/known/stdio_print.c:9: Warning: 
-  Neither code nor specification for function fprintf, generating default assigns from the prototype
+  Neither code nor specification for function fprintf_fallback_1, generating default assigns from the prototype
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   NON TERMINATING FUNCTION
@@ -67,6 +67,28 @@
 #include "stdarg.h"
 #include "stddef.h"
 #include "stdio.h"
+/*@ assigns \result, *stream;
+    assigns \result
+      \from *stream, *(format + (0 ..)), *(param1 + (0 ..)), param0, param2;
+    assigns *stream
+      \from *stream, *(format + (0 ..)), *(param1 + (0 ..)), param0, param2;
+ */
+int fprintf_fallback_1(FILE * restrict stream, char const * restrict format,
+                       int param0, char const *param1, int param2);
+
+int printf_fallback_1(char const * restrict format, int param0,
+                      char const *param1, int param2);
+
+int snprintf_fallback_1(char * restrict s, size_t n,
+                        char const * restrict format, int param0,
+                        char const *param1, int param2);
+
+int sprintf_fallback_1(char * restrict s, char const * restrict format,
+                       int param0, char const *param1, int param2);
+
+int dprintf_fallback_1(int fd, char const * restrict format, int param0,
+                       char const *param1, char const *param2);
+
 /*@ requires valid_read_string(param1);
     requires valid_read_string(format);
     assigns \result, stream->__fc_FILE_data;
@@ -148,42 +170,12 @@ int main(void)
   char *format;
   char *str;
   size_t size;
-  {
-    int __va_arg0 = 1;
-    char const *__va_arg1 = "2";
-    int __va_arg2 = 3;
-    void *__va_args[3] = {& __va_arg0, & __va_arg1, & __va_arg2};
-    /*@ assert Eva: initialization: \initialized(&format); */
-    fprintf(stream,(char const *)format,(void * const *)(__va_args));
-  }
-  {
-    int __va_arg0_10 = 1;
-    char const *__va_arg1_12 = "2";
-    int __va_arg2_14 = 3;
-    void *__va_args_16[3] = {& __va_arg0_10, & __va_arg1_12, & __va_arg2_14};
-    printf((char const *)format,(void * const *)(__va_args_16));
-  }
-  {
-    int __va_arg0_18 = 1;
-    char const *__va_arg1_20 = "2";
-    int __va_arg2_22 = 3;
-    void *__va_args_24[3] = {& __va_arg0_18, & __va_arg1_20, & __va_arg2_22};
-    snprintf(str,size,(char const *)format,(void * const *)(__va_args_24));
-  }
-  {
-    int __va_arg0_26 = 1;
-    char const *__va_arg1_28 = "2";
-    int __va_arg2_30 = 3;
-    void *__va_args_32[3] = {& __va_arg0_26, & __va_arg1_28, & __va_arg2_30};
-    sprintf(str,(char const *)format,(void * const *)(__va_args_32));
-  }
-  {
-    int __va_arg0_34 = 1;
-    char const *__va_arg1_36 = "3";
-    char const *__va_arg2_38 = "4";
-    void *__va_args_40[3] = {& __va_arg0_34, & __va_arg1_36, & __va_arg2_38};
-    dprintf(1,(char const *)format,(void * const *)(__va_args_40));
-  }
+  /*@ assert Eva: initialization: \initialized(&format); */
+  fprintf(stream,(char const *)format,1,"2",3); /* fprintf_fallback_1 */
+  printf((char const *)format,1,"2",3); /* printf_fallback_1 */
+  snprintf(str,size,(char const *)format,1,"2",3); /* snprintf_fallback_1 */
+  sprintf(str,(char const *)format,1,"2",3); /* sprintf_fallback_1 */
+  dprintf(1,(char const *)format,1,"3","4"); /* dprintf_fallback_1 */
   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 */

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

@@ -18,17 +18,17 @@
   Call to function fscanf with non-static format argument:
   no specification will be generated.
 [variadic] tests/known/stdio_scan.c:10: 
-  Generic translation of call to variadic function.
+  Fallback translation of call fscanf to a call to the specialized version fscanf_fallback_1.
 [variadic] tests/known/stdio_scan.c:11: Warning: 
   Call to function scanf with non-static format argument:
   no specification will be generated.
 [variadic] tests/known/stdio_scan.c:11: 
-  Generic translation of call to variadic function.
+  Fallback translation of call scanf to a call to the specialized version scanf_fallback_1.
 [variadic] tests/known/stdio_scan.c:12: Warning: 
   Call to function sscanf with non-static format argument:
   no specification will be generated.
 [variadic] tests/known/stdio_scan.c:12: 
-  Generic translation of call to variadic function.
+  Fallback translation of call sscanf to a call to the specialized version sscanf_fallback_1.
 [variadic] tests/known/stdio_scan.c:14: 
   Translating call to fscanf to a call to the specialized version fscanf_va_1.
 [variadic] tests/known/stdio_scan.c:15: 
@@ -43,6 +43,8 @@
 [eva] done for function main
 [eva] tests/known/stdio_scan.c:10: 
   assertion 'Eva,initialization' got final status invalid.
+[kernel:annot:missing-spec] tests/known/stdio_scan.c:10: Warning: 
+  Neither code nor specification for function fscanf_fallback_1, generating default assigns from the prototype
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   NON TERMINATING FUNCTION
@@ -51,6 +53,27 @@
 #include "stdarg.h"
 #include "stddef.h"
 #include "stdio.h"
+/*@ assigns \result, *stream, *param0, *(param1 + (0 ..)), *param2;
+    assigns \result
+      \from *stream, *(format + (0 ..)), *param0, *(param1 + (0 ..)), *param2;
+    assigns *stream
+      \from *stream, *(format + (0 ..)), *param0, *(param1 + (0 ..)), *param2;
+    assigns *param0
+      \from *stream, *(format + (0 ..)), *param0, *(param1 + (0 ..)), *param2;
+    assigns *(param1 + (0 ..))
+      \from *stream, *(format + (0 ..)), *param0, *(param1 + (0 ..)), *param2;
+    assigns *param2
+      \from *stream, *(format + (0 ..)), *param0, *(param1 + (0 ..)), *param2;
+ */
+int fscanf_fallback_1(FILE * restrict stream, char const * restrict format,
+                      int *param0, char *param1, int *param2);
+
+int scanf_fallback_1(char const * restrict format, int *param0, char *param1,
+                     int *param2);
+
+int sscanf_fallback_1(char const * restrict s, char const * restrict format,
+                      int *param0, char *param1, int *param2);
+
 /*@ requires \valid(param0);
     requires \valid(param2);
     requires valid_read_string(format);
@@ -133,29 +156,10 @@ int main(void)
   int i;
   int j;
   char *s;
-  {
-    int *__va_arg0 = & i;
-    /*@ assert Eva: initialization: \initialized(&s); */
-    char *__va_arg1 = s;
-    int *__va_arg2 = & j;
-    void *__va_args[3] = {& __va_arg0, & __va_arg1, & __va_arg2};
-    fscanf(stream,(char const *)format,(void * const *)(__va_args));
-  }
-  {
-    int *__va_arg0_12 = & i;
-    char *__va_arg1_14 = s;
-    int *__va_arg2_16 = & j;
-    void *__va_args_18[3] = {& __va_arg0_12, & __va_arg1_14, & __va_arg2_16};
-    scanf((char const *)format,(void * const *)(__va_args_18));
-  }
-  {
-    int *__va_arg0_20 = & i;
-    char *__va_arg1_22 = s;
-    int *__va_arg2_24 = & j;
-    void *__va_args_26[3] = {& __va_arg0_20, & __va_arg1_22, & __va_arg2_24};
-    sscanf((char const *)str,(char const *)format,
-           (void * const *)(__va_args_26));
-  }
+  /*@ assert Eva: initialization: \initialized(&s); */
+  fscanf(stream,(char const *)format,& i,s,& j); /* fscanf_fallback_1 */
+  scanf((char const *)format,& i,s,& j); /* scanf_fallback_1 */
+  sscanf((char const *)str,(char const *)format,& i,s,& j); /* sscanf_fallback_1 */
   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 */