From d24fdf11c2669b821f72a2a63accea6ebe783e54 Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.oliveiramaroneze@cea.fr> Date: Thu, 10 Aug 2017 10:10:07 +0200 Subject: [PATCH] sync with frama-c/frama-c!1439 --- src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle | 3 ++- src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle | 3 ++- src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle | 3 ++- 3 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle index b829e722be5..a904b504644 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle @@ -5,4 +5,5 @@ tests/bts/bts1307.i:23:[e-acsl] warning: approximating a real number by a float tests/bts/bts1307.i:11:[e-acsl] warning: approximating a real number by a float [e-acsl] translation done in project "e-acsl". FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown. -[value] user error: type long double not implemented. Using double instead +[value] user error: type long double wider than 64 bits not supported. + Using double instead for the remainder of the analysis. diff --git a/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle index 5cd81b76e9f..a54a14a8d90 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle +++ b/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle @@ -20,5 +20,6 @@ tests/gmp/cast.i:23:[e-acsl] warning: approximating a real number by a float __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308] [value] using specification for function __e_acsl_memory_init [value] using specification for function __e_acsl_assert -[value] user error: type long double not implemented. Using double instead +[value] user error: type long double wider than 64 bits not supported. + Using double instead for the remainder of the analysis. [value] done for function main diff --git a/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle index 9f712c261f8..2787673575f 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle +++ b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle @@ -27,7 +27,8 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: preco [value] using specification for function __gmpz_clear [value] using specification for function __gmpz_get_ui [value] using specification for function __gmpz_init_set_ui -[value] user error: type long double not implemented. Using double instead +[value] user error: type long double wider than 64 bits not supported. + Using double instead for the remainder of the analysis. tests/gmp/cast.i:23:[value] warning: accessing out of bounds index. assert 0 ≤ __gen_e_acsl_cast_9; tests/gmp/cast.i:23:[value] warning: accessing out of bounds index. assert __gen_e_acsl_cast_9 < 2; [value] done for function main -- GitLab