diff --git a/src/plugins/variadic/format_typer.ml b/src/plugins/variadic/format_typer.ml
index 3a9fc3992f390b99b136003d8e2a044830ef2e9c..d5f60a7ee7853b0f8da0754a4bc6158f9fb59d49 100644
--- a/src/plugins/variadic/format_typer.ml
+++ b/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
diff --git a/src/plugins/variadic/standard.ml b/src/plugins/variadic/standard.ml
index 98eefe0444d8a2b8313c137f22f55668bff17537..ae07bb0df4ee365492332fda2d4447e169dc0137 100644
--- a/src/plugins/variadic/standard.ml
+++ b/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
diff --git a/src/plugins/variadic/tests/known/oracle/scanf.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf.0.res.oracle
similarity index 63%
rename from src/plugins/variadic/tests/known/oracle/scanf.res.oracle
rename to src/plugins/variadic/tests/known/oracle/scanf.0.res.oracle
index f01080214554f1e753c64b2728a44b1a7cff5cd3..3b3929047d11a5d489a49ad7de293a5586bc3721 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf.res.oracle
+++ b/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;
+}
+
diff --git a/src/plugins/variadic/tests/known/oracle/scanf.1.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..44221e5bb220b87e06bf9640fb09e6404e660fd3
--- /dev/null
+++ b/src/plugins/variadic/tests/known/oracle/scanf.1.res.oracle
@@ -0,0 +1,122 @@
+[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;
+}
+
+
diff --git a/src/plugins/variadic/tests/known/scanf.c b/src/plugins/variadic/tests/known/scanf.c
index f407ca56e68af2fa6548c739c586970a16302321..8943f82294f5e5a0788c4afae166afa62b3e5f13 100644
--- a/src/plugins/variadic/tests/known/scanf.c
+++ b/src/plugins/variadic/tests/known/scanf.c
@@ -1,3 +1,8 @@
+/* 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
}