From 24ddf93889fdb8b1e307dac9cf65cb7cdeae27c2 Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.oliveiramaroneze@cea.fr> Date: Mon, 18 Jun 2018 09:56:09 +0200 Subject: [PATCH] [tests] remove some warnings about missing spec --- .../tests/format/oracle/fprintf.res.oracle | 24 ------------------- .../tests/format/oracle/printf.res.oracle | 8 ------- src/plugins/e-acsl/tests/format/test_config | 2 +- 3 files changed, 1 insertion(+), 33 deletions(-) diff --git a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle index 14dfa2185f1..12e87b8de7d 100644 --- a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle +++ b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle @@ -12,20 +12,6 @@ [e-acsl] Warning: annotating undefined function `fclose': the generated program may miss memory instrumentation if there are memory-related annotations. -[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:154: Warning: - Neither code nor specification for function fprintf, generating default assigns from the prototype -[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:158: Warning: - Neither code nor specification for function printf, generating default assigns from the prototype -[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:160: Warning: - Neither code nor specification for function snprintf, generating default assigns from the prototype -[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:162: Warning: - Neither code nor specification for function sprintf, generating default assigns from the prototype -[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:358: Warning: - Neither code nor specification for function dprintf, generating default assigns from the prototype -[kernel:annot:missing-spec] FRAMAC_SHARE/libc/sys/wait.h:60: Warning: - Neither code nor specification for function waitpid, generating default assigns from the prototype -[kernel:annot:missing-spec] tests/format/fprintf.c:15: Warning: - Neither code nor specification for function fork, generating default assigns from the prototype [e-acsl] FRAMAC_SHARE/libc/stdio.h:94: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. @@ -85,15 +71,11 @@ [value] using specification for function __e_acsl_full_init [value] using specification for function __e_acsl_mark_readonly [value] using specification for function fork -[kernel:annot:missing-spec] tests/format/fprintf.c:15: Warning: - Neither code nor specification for function __e_acsl_builtin_fprintf, generating default assigns from the prototype [value] using specification for function __e_acsl_builtin_fprintf [value] using specification for function exit [value] using specification for function waitpid [value:alarm] tests/format/fprintf.c:15: Warning: accessing uninitialized left-value. assert \initialized(&process_status); -[kernel:annot:missing-spec] tests/format/signalled.h:12: Warning: - Neither code nor specification for function __e_acsl_builtin_printf, generating default assigns from the prototype [value] using specification for function __e_acsl_builtin_printf [value] using specification for function __e_acsl_delete_block [value] tests/format/fprintf.c:16: Warning: @@ -114,15 +96,11 @@ Completely invalid destination for assigns clause *stream. Ignoring. [value:alarm] tests/format/fprintf.c:22: Warning: accessing uninitialized left-value. assert \initialized(&process_status_3); -[kernel:annot:missing-spec] tests/format/fprintf.c:27: Warning: - Neither code nor specification for function __e_acsl_builtin_dprintf, generating default assigns from the prototype [value] using specification for function __e_acsl_builtin_dprintf [value:alarm] tests/format/fprintf.c:27: Warning: accessing uninitialized left-value. assert \initialized(&process_status_4); [value:alarm] tests/format/fprintf.c:28: Warning: accessing uninitialized left-value. assert \initialized(&process_status_5); -[kernel:annot:missing-spec] tests/format/fprintf.c:34: Warning: - Neither code nor specification for function __e_acsl_builtin_sprintf, generating default assigns from the prototype [value] using specification for function __e_acsl_builtin_sprintf [value:alarm] tests/format/fprintf.c:34: Warning: accessing uninitialized left-value. assert \initialized(&process_status_6); @@ -138,8 +116,6 @@ Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring. [value:alarm] tests/format/fprintf.c:38: Warning: accessing uninitialized left-value. assert \initialized(&process_status_10); -[kernel:annot:missing-spec] tests/format/fprintf.c:41: Warning: - Neither code nor specification for function __e_acsl_builtin_snprintf, generating default assigns from the prototype [value] using specification for function __e_acsl_builtin_snprintf [value:alarm] tests/format/fprintf.c:41: Warning: accessing uninitialized left-value. assert \initialized(&process_status_11); diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle index f6c8152c43b..8d84c2c3338 100644 --- a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle +++ b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle @@ -17,12 +17,6 @@ [e-acsl] Warning: annotating undefined function `strcpy': the generated program may miss memory instrumentation if there are memory-related annotations. -[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:158: Warning: - Neither code nor specification for function printf, generating default assigns from the prototype -[kernel:annot:missing-spec] FRAMAC_SHARE/libc/unistd.h:791: Warning: - Neither code nor specification for function fork, generating default assigns from the prototype -[kernel:annot:missing-spec] FRAMAC_SHARE/libc/sys/wait.h:60: Warning: - Neither code nor specification for function waitpid, generating default assigns from the prototype [e-acsl] FRAMAC_SHARE/libc/string.h:327: Warning: E-ACSL construct `logic function application' is not yet supported. Ignoring annotation. @@ -421,8 +415,6 @@ [value] using specification for function __e_acsl_full_init [value] using specification for function __e_acsl_mark_readonly [value] using specification for function fork -[kernel:annot:missing-spec] tests/format/printf.c:179: Warning: - Neither code nor specification for function __e_acsl_builtin_printf, generating default assigns from the prototype [value] using specification for function __e_acsl_builtin_printf [value] using specification for function exit [value] using specification for function waitpid diff --git a/src/plugins/e-acsl/tests/format/test_config b/src/plugins/e-acsl/tests/format/test_config index bcbaa40882b..8f2dae04629 100644 --- a/src/plugins/e-acsl/tests/format/test_config +++ b/src/plugins/e-acsl/tests/format/test_config @@ -1,3 +1,3 @@ LOG: gen_@PTEST_NAME@.c -OPT: -variadic-no-translation -machdep gcc_x86_64 -check -e-acsl -e-acsl-full-mmodel -e-acsl-validate-format-strings -then-last -load-script tests/print.cmxs -print -ocode tests/format/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results +OPT: -variadic-no-translation -machdep gcc_x86_64 -check -e-acsl -e-acsl-full-mmodel -e-acsl-validate-format-strings -kernel-warn-key=-annot:missing-spec -then-last -load-script tests/print.cmxs -print -ocode tests/format/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results EXEC: ./scripts/testrun.sh @PTEST_NAME@ format "1" "--frama-c=@frama-c@ --full-mmodel --validate-format-strings" -- GitLab