From bc12801777521a32993616c3108793df5a194cad Mon Sep 17 00:00:00 2001 From: Julien Signoles <julien.signoles@cea.fr> Date: Tue, 27 Aug 2019 17:26:08 +0200 Subject: [PATCH] [tests] update wrt Eva's changes --- .../e-acsl/tests/format/oracle/fprintf.res.oracle | 14 +++++++------- .../tests/runtime/oracle/hidden_malloc.res.oracle | 2 +- .../tests/temporal/oracle/t_fun_lib.res.oracle | 4 ++-- 3 files changed, 10 insertions(+), 10 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 603bb073637..e0fb28f138a 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 31e79374518..f4cfabb6990 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 6b0a9be3f20..fc81d45a65d 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. -- GitLab