From fcca008369174f095535919ca83c7d61754342ee Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.oliveiramaroneze@cea.fr> Date: Wed, 24 Oct 2018 18:00:45 +0200 Subject: [PATCH] fix test oracles --- .../e-acsl/tests/format/oracle/fprintf.res.oracle | 11 +++++++---- 1 file changed, 7 insertions(+), 4 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 f11e3e9cd19..979384c70a7 100644 --- a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle +++ b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle @@ -15,7 +15,10 @@ [e-acsl] Warning: annotating undefined function `waitpid': the generated program may miss memory instrumentation if there are memory-related annotations. -[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:87: Warning: +[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:92: Warning: + E-ACSL construct `assigns clause in behavior' is not yet supported. + Ignoring annotation. +[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:86: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/stdio.h:94: Warning: @@ -83,11 +86,11 @@ [eva] using specification for function __e_acsl_assert [eva] using specification for function waitpid [eva] using specification for function __e_acsl_initialized -[eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:93: Warning: +[eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:86: Warning: function __e_acsl_assert: precondition got status unknown. [eva] using specification for function __e_acsl_delete_block -[eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:93: Warning: - function __gen_e_acsl_waitpid, behavior stat_loc_non_null: postcondition 'initialization,stat_loc_init_on_success' got status unknown. +[eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:86: Warning: + function __gen_e_acsl_waitpid: postcondition 'initialization,stat_loc_init_on_success' got status unknown. [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 -- GitLab