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 14dfa2185f1a48040310597e5911f1f410eeec1a..12e87b8de7de2e1d02d1f3d9082ba1f2378e5798 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 f6c8152c43b1807d21442e47c2ae3aa269ed7dd1..8d84c2c3338b650cba314a8fc9a998e0dda1322c 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 bcbaa40882b4e9025aacdcf38a27d29376d3e3d1..8f2dae04629c15ccc3f26ad5f4a285bd5f9da370 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"