From 7be21989ef55128aba1d342ad2be35fbf8bcc444 Mon Sep 17 00:00:00 2001 From: Boris Yakobowski <boris.yakobowski@cea.fr> Date: Mon, 27 Jul 2015 01:06:02 +0200 Subject: [PATCH] Update tests to trunk (at most one origin in garbled mix) --- .../e-acsl/tests/e-acsl-runtime/oracle/longlong.0.res.oracle | 4 +--- .../e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle | 5 +---- 2 files changed, 2 insertions(+), 7 deletions(-) diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.0.res.oracle index d3b3faf1c1d..79dc90c91ee 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.0.res.oracle @@ -46,9 +46,7 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:173:[value] Function __gmpz_tdiv_r: preconditio [value] using specification for function __gmpz_get_ui FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid. tests/e-acsl-runtime/longlong.i:19:[value] Reading left-value __e_acsl_4. - It contains a garbled mix of {x} because of Arithmetic - {tests/e-acsl-runtime/longlong.i:19; tests/e-acsl-runtime/longlong.i:19; - tests/e-acsl-runtime/longlong.i:19; tests/e-acsl-runtime/longlong.i:19}. + It contains a garbled mix of {x} because of Arithmetic. tests/e-acsl-runtime/longlong.i:19:[kernel] warning: pointer comparison: assert \pointer_comparable((void *)__e_acsl_4, (void *)1); [value] using specification for function __gmpz_clear diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle index bccfea12b31..2992d4c5a82 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle @@ -44,10 +44,7 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:171:[value] Function __gmpz_tdiv_r: preconditio FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:172:[value] Function __gmpz_tdiv_r: precondition got status valid. FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:173:[value] Function __gmpz_tdiv_r: precondition got status valid. tests/e-acsl-runtime/longlong.i:19:[value] Reading left-value __e_acsl_eq. - It contains a garbled mix of {x} because of Arithmetic - {tests/e-acsl-runtime/longlong.i:19; tests/e-acsl-runtime/longlong.i:19; - tests/e-acsl-runtime/longlong.i:19; tests/e-acsl-runtime/longlong.i:19; - tests/e-acsl-runtime/longlong.i:19}. + It contains a garbled mix of {x} because of Arithmetic. tests/e-acsl-runtime/longlong.i:19:[kernel] warning: pointer comparison: assert \pointer_comparable((void *)__e_acsl_eq, (void *)0); [value] using specification for function __gmpz_clear -- GitLab