Merge branch '1106-warning-include-stdint-h' into 'master'

[Variadic] Improve warning message about intmax_t and fix issue with %lc

Closes #1106

See merge request frama-c/frama-c!4459

src/plugins/variadic/format_typer.ml

@@ -65,7 +65,7 @@ let type_f_specifier ?find_typedef spec =
   | #float_specifier, Some `l -> Cil.doubleType
   | #float_specifier, Some `L -> Cil.longDoubleType
   | `c, None    -> Cil.intType
-  | `c, Some `l -> get_typedef ?find_typedef "intmax_t"
+  | `c, Some `l -> get_typedef ?find_typedef "wint_t"
   | `s, None    -> Cil.charPtrType
   | `s, Some `l -> ptr (get_typedef ?find_typedef "wchar_t")
   | `p, None    -> Cil.voidPtrType

src/plugins/variadic/standard.ml

@@ -731,13 +731,13 @@ let format_fun_call ~builder env format_fun vf args =
   let tvparams =
     try
       Format_typer.type_format ~find_typedef format
-    with Format_typer.Type_not_found type_name ->
+    with Format_typer.Type_not_found (type_name) ->
       Self.warning ~current:true
         "Unable to find type %s in the source code which should be used in \
          this call:@ no specification will be generated.@ \
          Note that due to cleanup, the type may have been defined in the \
-         original code but not used anywhere."
-        type_name;
+         original code but not used anywhere.@.\
+         Did you include <stdint.h> ?" type_name;
       raise (Translate_call_exn vf.vf_decl)
   in
 

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

@@ -16,15 +16,26 @@
   Declaration of variadic function dprintf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:610: 
   Declaration of variadic function asprintf.
-[variadic] scanf.c:7: 
+[variadic] scanf.c:12: 
   Translating call to scanf to a call to the specialized version scanf_va_1.
+[variadic] scanf.c:15: 
+  Translating call to scanf to a call to the specialized version scanf_va_2.
+[variadic] scanf.c:23: Warning: 
+  Unable to find type intmax_t in the source code which should be used in this call:
+  no specification will be generated.
+  Note that due to cleanup, the type may have been defined in the original code but not used anywhere.
+  Did you include <stdint.h> ?
+[variadic] scanf.c:23: 
+  Fallback translation of call scanf to a call to the specialized version scanf_fallback_1.
 [eva] Analyzing a complete application starting at main
 [eva] using specification for function scanf_va_1
+[eva] using specification for function scanf_va_2
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   c[0] ∈ [--..--]
    [1..9] ∈ [--..--] or UNINITIALIZED
   i ∈ [--..--]
+  wc ∈ [--..--]
   __retres ∈ {0}
   S___fc_stdin[0..1] ∈ [--..--]
 /* Generated by Frama-C */
@@ -59,14 +70,42 @@
 int scanf_va_1(char const * restrict format, char *param0, char *param1,
                int *param2);
 
+/*@ requires \valid(param0);
+    requires valid_read_string(format);
+    ensures \initialized(param0);
+    assigns \result, __fc_stdin->__fc_FILE_data, *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 *param0
+      \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
+            (indirect: *(format + (0 ..)));
+ */
+int scanf_va_2(char const * restrict format, wchar_t *param0);
+
 int main(void)
 {
   int __retres;
   char c[10];
   int i;
+  wchar_t wc;
   scanf("Hello %*10le %% %10s %[^]world] %d !",c,c,& i); /* scanf_va_1 */
+  scanf("%lc",& wc); /* scanf_va_2 */
   __retres = 0;
   return __retres;
 }
 
+int scanf_fallback_1(char const * restrict format, int *param0);
+
+void warn_about_intmax_t(void)
+{
+  int i;
+  scanf("%jd",& i); /* scanf_fallback_1 */
+  return;
+}
+
 

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

+[variadic] FRAMAC_SHARE/libc/stdio.h:207: 
+  Declaration of variadic function fprintf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:209: 
+  Declaration of variadic function fscanf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:211: 
+  Declaration of variadic function printf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:212: 
+  Declaration of variadic function scanf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:213: 
+  Declaration of variadic function snprintf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:215: 
+  Declaration of variadic function sprintf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:217: 
+  Declaration of variadic function sscanf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:550: 
+  Declaration of variadic function dprintf.
+[variadic] FRAMAC_SHARE/libc/stdio.h:610: 
+  Declaration of variadic function asprintf.
+[variadic] scanf.c:12: 
+  Translating call to scanf to a call to the specialized version scanf_va_1.
+[variadic] scanf.c:15: 
+  Translating call to scanf to a call to the specialized version scanf_va_2.
+[variadic] scanf.c:23: 
+  Translating call to scanf to a call to the specialized version scanf_va_3.
+[eva] Analyzing a complete application starting at main
+[eva] using specification for function scanf_va_1
+[eva] using specification for function scanf_va_2
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  c[0] ∈ [--..--]
+   [1..9] ∈ [--..--] or UNINITIALIZED
+  i ∈ [--..--]
+  wc ∈ [--..--]
+  __retres ∈ {0}
+  S___fc_stdin[0..1] ∈ [--..--]
+/* Generated by Frama-C */
+#include "errno.h"
+#include "stdarg.h"
+#include "stddef.h"
+#include "stdint.h"
+#include "stdio.h"
+/*@ requires \valid(param1);
+    requires \valid(param2);
+    requires valid_read_string(format);
+    ensures \initialized(param1);
+    ensures \initialized(param2);
+    assigns \result, __fc_stdin->__fc_FILE_data, *param2, *param1,
+            *(param0 + (0 ..));
+    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 + (0 ..))
+      \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
+            (indirect: *(format + (0 ..)));
+ */
+int scanf_va_1(char const * restrict format, char *param0, char *param1,
+               int *param2);
+
+/*@ requires \valid(param0);
+    requires valid_read_string(format);
+    ensures \initialized(param0);
+    assigns \result, __fc_stdin->__fc_FILE_data, *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 *param0
+      \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
+            (indirect: *(format + (0 ..)));
+ */
+int scanf_va_2(char const * restrict format, wchar_t *param0);
+
+int main(void)
+{
+  int __retres;
+  char c[10];
+  int i;
+  wchar_t wc;
+  scanf("Hello %*10le %% %10s %[^]world] %d !",c,c,& i); /* scanf_va_1 */
+  scanf("%lc",& wc); /* scanf_va_2 */
+  __retres = 0;
+  return __retres;
+}
+
+/*@ requires \valid(param0);
+    requires valid_read_string(format);
+    ensures \initialized(param0);
+    assigns \result, __fc_stdin->__fc_FILE_data, *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 *param0
+      \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
+            (indirect: *(format + (0 ..)));
+ */
+int scanf_va_3(char const * restrict format, intmax_t *param0);
+
+void warn_about_intmax_t(void)
+{
+  int i;
+  scanf("%jd",(intmax_t *)(& i)); /* scanf_va_3 */
+  return;
+}
+
+

src/plugins/variadic/tests/known/scanf.c

+/* run.config
+   STDOPT:
+   STDOPT: #"-cpp-extra-args=-DINCLUDE_STDINT"
+*/
+
 #include <stdio.h>
 
 int main(){
@@ -5,4 +10,15 @@ int main(){
   int i;
 
   scanf("Hello %*10le %% %10s %[^]world] %d !", c, c, &i);
+
+  wchar_t wc;
+  scanf("%lc", &wc);
+}
+
+#ifdef INCLUDE_STDINT
+#include <stdint.h> // avoids warning due to missing intmax_t below
+#endif
+void warn_about_intmax_t(void) {
+  int i;
+  scanf("%jd", &i); // '%j' is for intmax_t
 }