From 3bb7cf019f53341ce7b688695b0b598681546b52 Mon Sep 17 00:00:00 2001 From: Virgile Prevosto <virgile.prevosto@m4x.org> Date: Thu, 26 Aug 2021 12:15:16 +0200 Subject: [PATCH] [variadic] fix warning msg and update oracles --- .../e-acsl/tests/builtin/oracle/gen_strcmp.c | 2 +- .../tests/builtin/oracle/strcmp.res.oracle | 2 +- src/plugins/variadic/standard.ml | 2 +- .../tests/known/oracle/stdio_print.res.oracle | 144 ++++++++++++------ .../tests/known/oracle/stdio_scan.res.oracle | 124 ++++++++++----- 5 files changed, 189 insertions(+), 85 deletions(-) diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c index 0f0aa26e6d1..fcc76624c98 100644 --- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c +++ b/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; diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle index c63c31e97c5..588c0bf722b 100644 --- a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle +++ b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle @@ -1,6 +1,6 @@ [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 diff --git a/src/plugins/variadic/standard.ml b/src/plugins/variadic/standard.ml index c5f1dbe24bc..40129fbf0b8 100644 --- a/src/plugins/variadic/standard.ml +++ b/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 diff --git a/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle b/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle index 5cded5c9814..e461895f776 100644 --- a/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle +++ b/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; } diff --git a/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle b/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle index 933132b0680..66601b31517 100644 --- a/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle +++ b/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; } -- GitLab