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 603bb0736371a1433b57909d540fc680df08b111..e0fb28f138a99d5b723a372f59bf6e58f4b0bed1 100644 --- a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle +++ b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle @@ -96,7 +96,7 @@ [eva:alarm] tests/format/fprintf.c:15: Warning: accessing uninitialized left-value. assert \initialized(&process_status); [eva] using specification for function __e_acsl_builtin_printf -[eva] tests/format/fprintf.c:16: Warning: +[eva:invalid-assigns] tests/format/fprintf.c:16: Completely invalid destination for assigns clause *stream. Ignoring. [eva:alarm] tests/format/fprintf.c:16: Warning: accessing uninitialized left-value. assert \initialized(&process_status_0); @@ -108,7 +108,7 @@ [eva] using specification for function fclose [eva:alarm] tests/format/fprintf.c:21: Warning: accessing uninitialized left-value. assert \initialized(&process_status_2); -[eva] tests/format/fprintf.c:22: Warning: +[eva:invalid-assigns] tests/format/fprintf.c:22: Completely invalid destination for assigns clause *stream. Ignoring. [eva:alarm] tests/format/fprintf.c:22: Warning: accessing uninitialized left-value. assert \initialized(&process_status_3); @@ -124,11 +124,11 @@ accessing uninitialized left-value. assert \initialized(&process_status_7); [eva:alarm] tests/format/fprintf.c:36: Warning: accessing uninitialized left-value. assert \initialized(&process_status_8); -[eva] tests/format/fprintf.c:37: Warning: +[eva:invalid-assigns] tests/format/fprintf.c:37: Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring. [eva:alarm] tests/format/fprintf.c:37: Warning: accessing uninitialized left-value. assert \initialized(&process_status_9); -[eva] tests/format/fprintf.c:38: Warning: +[eva:invalid-assigns] tests/format/fprintf.c:38: Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring. [eva:alarm] tests/format/fprintf.c:38: Warning: accessing uninitialized left-value. assert \initialized(&process_status_10); @@ -137,17 +137,17 @@ accessing uninitialized left-value. assert \initialized(&process_status_11); [eva:alarm] tests/format/fprintf.c:42: Warning: accessing uninitialized left-value. assert \initialized(&process_status_12); -[eva] tests/format/fprintf.c:43: Warning: +[eva:invalid-assigns] tests/format/fprintf.c:43: Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring. [eva:alarm] tests/format/fprintf.c:43: Warning: accessing uninitialized left-value. assert \initialized(&process_status_13); [eva:alarm] tests/format/fprintf.c:44: Warning: accessing uninitialized left-value. assert \initialized(&process_status_14); -[eva] tests/format/fprintf.c:45: Warning: +[eva:invalid-assigns] tests/format/fprintf.c:45: Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring. [eva:alarm] tests/format/fprintf.c:45: Warning: accessing uninitialized left-value. assert \initialized(&process_status_15); -[eva] tests/format/fprintf.c:46: Warning: +[eva:invalid-assigns] tests/format/fprintf.c:46: Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring. [eva:alarm] tests/format/fprintf.c:46: Warning: accessing uninitialized left-value. assert \initialized(&process_status_16); diff --git a/src/plugins/e-acsl/tests/runtime/oracle/hidden_malloc.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/hidden_malloc.res.oracle index 31e79374518c234d9973af32e7eb1ff12995f7b2..f4cfabb6990983d8cd7c939d73910391343c4a89 100644 --- a/src/plugins/e-acsl/tests/runtime/oracle/hidden_malloc.res.oracle +++ b/src/plugins/e-acsl/tests/runtime/oracle/hidden_malloc.res.oracle @@ -4,6 +4,6 @@ [kernel:annot:missing-spec] tests/runtime/hidden_malloc.c:11: Warning: Neither code nor specification for function realpath, generating default assigns from the prototype [e-acsl] translation done in project "e-acsl". -[eva] tests/runtime/hidden_malloc.c:11: Warning: +[eva:invalid-assigns] tests/runtime/hidden_malloc.c:11: Completely invalid destination for assigns clause *((char *)x_1 + (0 ..)). Ignoring. diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle index 6b0a9be3f209c0a34df396439444b1e326f0a4bd..fc81d45a65d8e98708f876b874a513d12ef1e060 100644 --- a/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle +++ b/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle @@ -4,7 +4,7 @@ [kernel:annot:missing-spec] tests/temporal/t_fun_lib.c:20: Warning: Neither code nor specification for function realpath, generating default assigns from the prototype [e-acsl] translation done in project "e-acsl". -[eva] tests/temporal/t_fun_lib.c:20: Warning: +[eva:invalid-assigns] tests/temporal/t_fun_lib.c:20: Completely invalid destination for assigns clause *(x_0 + (0 ..)). Ignoring. -[eva] tests/temporal/t_fun_lib.c:21: Warning: +[eva:invalid-assigns] tests/temporal/t_fun_lib.c:21: Completely invalid destination for assigns clause *(x_0 + (0 ..)). Ignoring.