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 d3b3faf1c1da088a90cedd23e22683c024352412..79dc90c91ee9e50716f733c5b5f2e6af04df9e1a 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 bccfea12b316ac60738fc72227ac103a77797342..2992d4c5a824fda7e940fb808af3425ea461d848 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