[variadic] fix warning msg and update oracles

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

@@ -116,7 +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) {
-    fprintf(stderr,(char const *)fmt,l,r); /* fprintf_fallback_1 */
+    fprintf(stderr,(char const *)fmt,l,r); /* fprintf_va_6 */
     __gen_e_acsl_abort();
   }
   return;

src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle

 [variadic] tests/builtin/strcmp.c:11: Warning: 
   Call to function fprintf with non-static format argument:
-  no specification will be generated.
+  assuming that parameters are coherent with the format
 [e-acsl] beginning translation.
 [e-acsl] Warning: annotating undefined function `abort':
   the generated program may miss memory instrumentation

src/plugins/variadic/standard.ml

@@ -723,7 +723,7 @@ let format_fun_call ~fundec env format_fun scope loc mk_call vf args =
       | None ->
         Self.warning ~current:true
           "Call to function %s with non-static format argument:@ \
-           Assuming that parameters are coherent with the format"
+           assuming that parameters are coherent with the format"
           vf.vf_decl.vorig_name;
         infer_format_from_args vf format_fun args
       | Some s -> Format_parser.parse_format format_fun.f_kind s

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

@@ -18,39 +18,39 @@
   Declaration of variadic function asprintf.
 [variadic] tests/known/stdio_print.c:9: Warning: 
   Call to function fprintf with non-static format argument:
-  no specification will be generated.
+  assuming that parameters are coherent with the format
 [variadic] tests/known/stdio_print.c:9: 
-  Fallback translation of call fprintf to a call to the specialized version fprintf_fallback_1.
+  Translating call to fprintf to a call to the specialized version fprintf_va_1.
 [variadic] tests/known/stdio_print.c:10: Warning: 
   Call to function printf with non-static format argument:
-  no specification will be generated.
+  assuming that parameters are coherent with the format
 [variadic] tests/known/stdio_print.c:10: 
-  Fallback translation of call printf to a call to the specialized version printf_fallback_1.
+  Translating call to printf to a call to the specialized version printf_va_1.
 [variadic] tests/known/stdio_print.c:11: Warning: 
   Call to function snprintf with non-static format argument:
-  no specification will be generated.
+  assuming that parameters are coherent with the format
 [variadic] tests/known/stdio_print.c:11: 
-  Fallback translation of call snprintf to a call to the specialized version snprintf_fallback_1.
+  Translating call to snprintf to a call to the specialized version snprintf_va_1.
 [variadic] tests/known/stdio_print.c:12: Warning: 
   Call to function sprintf with non-static format argument:
-  no specification will be generated.
+  assuming that parameters are coherent with the format
 [variadic] tests/known/stdio_print.c:12: 
-  Fallback translation of call sprintf to a call to the specialized version sprintf_fallback_1.
+  Translating call to sprintf to a call to the specialized version sprintf_va_1.
 [variadic] tests/known/stdio_print.c:13: Warning: 
   Call to function dprintf with non-static format argument:
-  no specification will be generated.
+  assuming that parameters are coherent with the format
 [variadic] tests/known/stdio_print.c:13: 
-  Fallback translation of call dprintf to a call to the specialized version dprintf_fallback_1.
+  Translating call to dprintf to a call to the specialized version dprintf_va_1.
 [variadic] tests/known/stdio_print.c:15: 
-  Translating call to fprintf to a call to the specialized version fprintf_va_1.
+  Translating call to fprintf to a call to the specialized version fprintf_va_2.
 [variadic] tests/known/stdio_print.c:16: 
-  Translating call to printf to a call to the specialized version printf_va_1.
+  Translating call to printf to a call to the specialized version printf_va_2.
 [variadic] tests/known/stdio_print.c:17: 
-  Translating call to snprintf to a call to the specialized version snprintf_va_1.
+  Translating call to snprintf to a call to the specialized version snprintf_va_2.
 [variadic] tests/known/stdio_print.c:18: 
-  Translating call to sprintf to a call to the specialized version sprintf_va_1.
+  Translating call to sprintf to a call to the specialized version sprintf_va_2.
 [variadic] tests/known/stdio_print.c:19: 
-  Translating call to dprintf to a call to the specialized version dprintf_va_1.
+  Translating call to dprintf to a call to the specialized version dprintf_va_2.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
@@ -59,8 +59,6 @@
 [eva] done for function main
 [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_fallback_1, generating default assigns from the prototype
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   NON TERMINATING FUNCTION
@@ -69,27 +67,79 @@
 #include "stdarg.h"
 #include "stddef.h"
 #include "stdio.h"
-/*@ assigns \result, *stream;
+/*@ requires valid_read_string(param1);
+    requires valid_read_string(format);
+    assigns \result, stream->__fc_FILE_data;
     assigns \result
-      \from *stream, *(format + (0 ..)), *(param1 + (0 ..)), param0, param2;
-    assigns *stream
-      \from *stream, *(format + (0 ..)), *(param1 + (0 ..)), param0, param2;
+      \from (indirect: stream->__fc_FILE_id),
+            (indirect: stream->__fc_FILE_data),
+            (indirect: *(format + (0 ..))), (indirect: param2),
+            (indirect: *(param1 + (0 ..))), (indirect: param0);
+    assigns stream->__fc_FILE_data
+      \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+            (indirect: *(format + (0 ..))), param2, *(param1 + (0 ..)),
+            param0;
  */
-int fprintf_fallback_1(FILE * restrict stream, char const * restrict format,
-                       int param0, char const *param1, int param2);
+int fprintf_va_1(FILE * restrict stream, char const * restrict format,
+                 int param0, char *param1, int param2);
 
-int printf_fallback_1(char const * restrict format, int param0,
-                      char const *param1, int param2);
+/*@ requires valid_read_string(param1);
+    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 ..))), (indirect: param2),
+            (indirect: *(param1 + (0 ..))), (indirect: param0);
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
+            param2, *(param1 + (0 ..)), param0;
+ */
+int printf_va_1(char const * restrict format, int param0, char *param1,
+                int param2);
 
-int snprintf_fallback_1(char * restrict s, size_t n,
-                        char const * restrict format, int param0,
-                        char const *param1, int param2);
+/*@ requires valid_read_string(param1);
+    requires valid_read_string(format);
+    requires
+      \valid(s + (0 .. n - 1)) ∨
+      \valid(s + (0 .. format_length(format) - 1));
+    assigns \result, *(s + (0 ..));
+    assigns \result
+      \from (indirect: n), (indirect: *(format + (0 ..))),
+            (indirect: param2), (indirect: *(param1 + (0 ..))),
+            (indirect: param0);
+    assigns *(s + (0 ..))
+      \from (indirect: n), (indirect: *(format + (0 ..))), param2,
+            *(param1 + (0 ..)), param0;
+ */
+int snprintf_va_1(char * restrict s, size_t n, char const * restrict format,
+                  int param0, char *param1, int param2);
 
-int sprintf_fallback_1(char * restrict s, char const * restrict format,
-                       int param0, char const *param1, int param2);
+/*@ requires valid_read_string(param1);
+    requires valid_read_string(format);
+    assigns \result, *(s + (0 ..));
+    assigns \result
+      \from (indirect: *(format + (0 ..))), (indirect: param2),
+            (indirect: *(param1 + (0 ..))), (indirect: param0);
+    assigns *(s + (0 ..))
+      \from (indirect: *(format + (0 ..))), param2, *(param1 + (0 ..)),
+            param0;
+ */
+int sprintf_va_1(char * restrict s, char const * restrict format, int param0,
+                 char *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(param2);
+    requires valid_read_string(format);
+    assigns \result;
+    assigns \result
+      \from (indirect: fd), (indirect: *(format + (0 ..))),
+            (indirect: *(param2 + (0 ..))), (indirect: *(param1 + (0 ..))),
+            (indirect: param0);
+ */
+int dprintf_va_1(int fd, char const * restrict format, int param0,
+                 char *param1, char *param2);
 
 /*@ requires valid_read_string(param1);
     requires valid_read_string(format);
@@ -104,7 +154,7 @@ int dprintf_fallback_1(int fd, char const * restrict format, int param0,
             (indirect: *(format + (0 ..))), param2, *(param1 + (0 ..)),
             param0;
  */
-int fprintf_va_1(FILE * restrict stream, char const * restrict format,
+int fprintf_va_2(FILE * restrict stream, char const * restrict format,
                  int param0, char *param1, int param2);
 
 /*@ requires valid_read_string(param1);
@@ -120,7 +170,7 @@ int fprintf_va_1(FILE * restrict stream, char const * restrict format,
             __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
             param2, *(param1 + (0 ..)), param0;
  */
-int printf_va_1(char const * restrict format, int param0, char *param1,
+int printf_va_2(char const * restrict format, int param0, char *param1,
                 int param2);
 
 /*@ requires valid_read_string(param1);
@@ -137,7 +187,7 @@ int printf_va_1(char const * restrict format, int param0, char *param1,
       \from (indirect: n), (indirect: *(format + (0 ..))), param2,
             *(param1 + (0 ..)), param0;
  */
-int snprintf_va_1(char * restrict s, size_t n, char const * restrict format,
+int snprintf_va_2(char * restrict s, size_t n, char const * restrict format,
                   int param0, char *param1, int param2);
 
 /*@ requires valid_read_string(param1);
@@ -150,7 +200,7 @@ int snprintf_va_1(char * restrict s, size_t n, char const * restrict format,
       \from (indirect: *(format + (0 ..))), param2, *(param1 + (0 ..)),
             param0;
  */
-int sprintf_va_1(char * restrict s, char const * restrict format, int param0,
+int sprintf_va_2(char * restrict s, char const * restrict format, int param0,
                  char *param1, int param2);
 
 /*@ requires valid_read_string(param1);
@@ -162,7 +212,7 @@ int sprintf_va_1(char * restrict s, char const * restrict format, int param0,
             (indirect: *(param2 + (0 ..))), (indirect: *(param1 + (0 ..))),
             (indirect: param0);
  */
-int dprintf_va_1(int fd, char const * restrict format, int param0,
+int dprintf_va_2(int fd, char const * restrict format, int param0,
                  char *param1, char *param2);
 
 int main(void)
@@ -173,16 +223,16 @@ int main(void)
   char *str;
   size_t size;
   /*@ 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 */
-  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 */
+  fprintf(stream,(char const *)format,1,(char *)"2",3); /* fprintf_va_1 */
+  printf((char const *)format,1,(char *)"2",3); /* printf_va_1 */
+  snprintf(str,size,(char const *)format,1,(char *)"2",3); /* snprintf_va_1 */
+  sprintf(str,(char const *)format,1,(char *)"2",3); /* sprintf_va_1 */
+  dprintf(1,(char const *)format,1,(char *)"3",(char *)"4"); /* dprintf_va_1 */
+  fprintf(stream,"%d %s %d",1,(char *)"2",3); /* fprintf_va_2 */
+  printf("%d %s %d",1,(char *)"2",3); /* printf_va_2 */
+  snprintf(str,size,"%d %s %d",1,(char *)"2",3); /* snprintf_va_2 */
+  sprintf(str,"%d %s %d",1,(char *)"2",3); /* sprintf_va_2 */
+  dprintf(1,"%d %s %s",1,(char *)"3",(char *)"4"); /* dprintf_va_2 */
   __retres = 0;
   return __retres;
 }

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

@@ -18,25 +18,25 @@
   Declaration of variadic function asprintf.
 [variadic] tests/known/stdio_scan.c:10: Warning: 
   Call to function fscanf with non-static format argument:
-  no specification will be generated.
+  assuming that parameters are coherent with the format
 [variadic] tests/known/stdio_scan.c:10: 
-  Fallback translation of call fscanf to a call to the specialized version fscanf_fallback_1.
+  Translating call to fscanf to a call to the specialized version fscanf_va_1.
 [variadic] tests/known/stdio_scan.c:11: Warning: 
   Call to function scanf with non-static format argument:
-  no specification will be generated.
+  assuming that parameters are coherent with the format
 [variadic] tests/known/stdio_scan.c:11: 
-  Fallback translation of call scanf to a call to the specialized version scanf_fallback_1.
+  Translating call to scanf to a call to the specialized version scanf_va_1.
 [variadic] tests/known/stdio_scan.c:12: Warning: 
   Call to function sscanf with non-static format argument:
-  no specification will be generated.
+  assuming that parameters are coherent with the format
 [variadic] tests/known/stdio_scan.c:12: 
-  Fallback translation of call sscanf to a call to the specialized version sscanf_fallback_1.
+  Translating call to sscanf to a call to the specialized version sscanf_va_1.
 [variadic] tests/known/stdio_scan.c:14: 
-  Translating call to fscanf to a call to the specialized version fscanf_va_1.
+  Translating call to fscanf to a call to the specialized version fscanf_va_2.
 [variadic] tests/known/stdio_scan.c:15: 
-  Translating call to scanf to a call to the specialized version scanf_va_1.
+  Translating call to scanf to a call to the specialized version scanf_va_2.
 [variadic] tests/known/stdio_scan.c:16: 
-  Translating call to sscanf to a call to the specialized version sscanf_va_1.
+  Translating call to sscanf to a call to the specialized version sscanf_va_2.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
@@ -45,8 +45,6 @@
 [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
@@ -55,26 +53,82 @@
 #include "stdarg.h"
 #include "stddef.h"
 #include "stdio.h"
-/*@ assigns \result, *stream, *param0, *(param1 + (0 ..)), *param2;
+/*@ requires \valid(param0);
+    requires \valid(param1);
+    requires \valid(param2);
+    requires valid_read_string(format);
+    ensures \initialized(param0);
+    ensures \initialized(param1);
+    ensures \initialized(param2);
+    assigns \result, stream->__fc_FILE_data, *param2, *param1, *param0;
     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;
+      \from (indirect: stream->__fc_FILE_id),
+            (indirect: stream->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns stream->__fc_FILE_data
+      \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+            (indirect: *(format + (0 ..)));
     assigns *param2
-      \from *stream, *(format + (0 ..)), *param0, *(param1 + (0 ..)), *param2;
+      \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+            (indirect: *(format + (0 ..)));
+    assigns *param1
+      \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+            (indirect: *(format + (0 ..)));
+    assigns *param0
+      \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+            (indirect: *(format + (0 ..)));
  */
-int fscanf_fallback_1(FILE * restrict stream, char const * restrict format,
-                      int *param0, char *param1, int *param2);
+int fscanf_va_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);
+/*@ requires \valid(param0);
+    requires \valid(param1);
+    requires \valid(param2);
+    requires valid_read_string(format);
+    ensures \initialized(param0);
+    ensures \initialized(param1);
+    ensures \initialized(param2);
+    assigns \result, __fc_stdin->__fc_FILE_data, *param2, *param1, *param0;
+    assigns \result
+      \from (indirect: __fc_stdin->__fc_FILE_id),
+            (indirect: __fc_stdin->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns __fc_stdin->__fc_FILE_data
+      \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
+            (indirect: *(format + (0 ..)));
+    assigns *param2
+      \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
+            (indirect: *(format + (0 ..)));
+    assigns *param1
+      \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
+            (indirect: *(format + (0 ..)));
+    assigns *param0
+      \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
+            (indirect: *(format + (0 ..)));
+ */
+int scanf_va_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(param1);
+    requires \valid(param2);
+    requires valid_read_string(format);
+    requires valid_read_string(s);
+    ensures \initialized(param0);
+    ensures \initialized(param1);
+    ensures \initialized(param2);
+    assigns \result, *param2, *param1, *param0;
+    assigns \result
+      \from (indirect: *(s + (0 ..))), (indirect: *(format + (0 ..)));
+    assigns *param2
+      \from (indirect: *(s + (0 ..))), (indirect: *(format + (0 ..)));
+    assigns *param1
+      \from (indirect: *(s + (0 ..))), (indirect: *(format + (0 ..)));
+    assigns *param0
+      \from (indirect: *(s + (0 ..))), (indirect: *(format + (0 ..)));
+ */
+int sscanf_va_1(char const * restrict s, char const * restrict format,
+                int *param0, char *param1, int *param2);
 
 /*@ requires \valid(param0);
     requires \valid(param2);
@@ -100,7 +154,7 @@ int sscanf_fallback_1(char const * restrict s, char const * restrict format,
       \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
             (indirect: *(format + (0 ..)));
  */
-int fscanf_va_1(FILE * restrict stream, char const * restrict format,
+int fscanf_va_2(FILE * restrict stream, char const * restrict format,
                 int *param0, char *param1, int *param2);
 
 /*@ requires \valid(param0);
@@ -127,7 +181,7 @@ int fscanf_va_1(FILE * restrict stream, char const * restrict format,
       \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
             (indirect: *(format + (0 ..)));
  */
-int scanf_va_1(char const * restrict format, int *param0, char *param1,
+int scanf_va_2(char const * restrict format, int *param0, char *param1,
                int *param2);
 
 /*@ requires \valid(param0);
@@ -146,7 +200,7 @@ int scanf_va_1(char const * restrict format, int *param0, char *param1,
     assigns *param0
       \from (indirect: *(s + (0 ..))), (indirect: *(format + (0 ..)));
  */
-int sscanf_va_1(char const * restrict s, char const * restrict format,
+int sscanf_va_2(char const * restrict s, char const * restrict format,
                 int *param0, char *param1, int *param2);
 
 int main(void)
@@ -159,12 +213,12 @@ int main(void)
   int j;
   char *s;
   /*@ 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 */
+  fscanf(stream,(char const *)format,& i,s,& j); /* fscanf_va_1 */
+  scanf((char const *)format,& i,s,& j); /* scanf_va_1 */
+  sscanf((char const *)str,(char const *)format,& i,s,& j); /* sscanf_va_1 */
+  fscanf(stream,"%d %s %d",& i,s,& j); /* fscanf_va_2 */
+  scanf("%d %s %d",& i,s,& j); /* scanf_va_2 */
+  sscanf((char const *)str,"%d %s %d",& i,s,& j); /* sscanf_va_2 */
   __retres = 0;
   return __retres;
 }