Skip to content
Snippets Groups Projects
Commit bc128017 authored by Julien Signoles's avatar Julien Signoles
Browse files

[tests] update wrt Eva's changes

parent 8803ee15
No related branches found
No related tags found
No related merge requests found
......@@ -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);
......
......@@ -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.
......@@ -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.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment