From 028ba29cc0de5a74c4a5a4622505ec18fdb3db45 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 10 Jun 2020 09:41:09 +0200
Subject: [PATCH] [typing] fix bug when mixing integers and floats in
annotations while -e-acsl-gmp-only is activated
---
src/plugins/e-acsl/src/analyses/typing.ml | 5 ++++-
.../gmp-only/oracle_ci/functions.res.oracle | 2 +-
.../tests/gmp-only/oracle_ci/gen_functions.c | 21 ++++++++++++++-----
3 files changed, 21 insertions(+), 7 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 075d6bfa4a7..fa5d75b572d 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -292,10 +292,13 @@ let ty_of_logic_ty ?term lty =
(* generate a context [c]. Take --e-acsl-gmp-only into account iff [use_gmp_opt]
is true. *)
let mk_ctx ~use_gmp_opt = function
+ | C_float _ as f ->
+ if use_gmp_opt && Options.Gmp_only.get () then Rational
+ else f
| C_integer _ as c ->
if use_gmp_opt && Options.Gmp_only.get () then Gmpz
else c
- | C_float _ | Gmpz | Rational | Real | Nan as c -> c
+ | Gmpz | Rational | Real | Nan as c -> c
(* the number_ty corresponding to [t] whenever use as an offset.
In that case, it cannot be a GMP, so it must be coerced to an integral type
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/functions.res.oracle b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/functions.res.oracle
index 3a0b1952d64..3c2b35833e5 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/functions.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/functions.res.oracle
@@ -28,6 +28,6 @@
[eva:alarm] tests/gmp-only/functions.c:25: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp-only/functions.c:68: Warning:
- non-finite double value. assert \is_finite(__gen_e_acsl__15);
+ non-finite double value. assert \is_finite(__gen_e_acsl_cast);
[eva:alarm] tests/gmp-only/functions.c:68: Warning:
function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
index 91010d0c7a4..f06e60821c0 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
@@ -255,9 +255,20 @@ int main(void)
double d = 2.0;
{
double __gen_e_acsl_f2_2;
+ __e_acsl_mpq_t __gen_e_acsl__15;
+ __e_acsl_mpq_t __gen_e_acsl__16;
+ int __gen_e_acsl_gt_5;
__gen_e_acsl_f2_2 = __gen_e_acsl_f2(d);
- __e_acsl_assert(__gen_e_acsl_f2_2 > 0.,"Assertion","main","f2(d) > 0",
+ __gmpq_init(__gen_e_acsl__15);
+ __gmpq_set_str(__gen_e_acsl__15,"0",10);
+ __gmpq_init(__gen_e_acsl__16);
+ __gmpq_set_d(__gen_e_acsl__16,__gen_e_acsl_f2_2);
+ __gen_e_acsl_gt_5 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__16),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__15));
+ __e_acsl_assert(__gen_e_acsl_gt_5 > 0,"Assertion","main","f2(d) > 0",
"tests/gmp-only/functions.c",68);
+ __gmpq_clear(__gen_e_acsl__15);
+ __gmpq_clear(__gen_e_acsl__16);
}
/*@ assert f2(d) > 0; */ ;
__retres = 0;
@@ -406,7 +417,7 @@ double __gen_e_acsl_f2(double x)
__e_acsl_mpq_t __gen_e_acsl__13;
__e_acsl_mpq_t __gen_e_acsl__14;
__e_acsl_mpq_t __gen_e_acsl_div;
- double __gen_e_acsl__15;
+ double __gen_e_acsl_cast;
__gmpq_init(__gen_e_acsl__13);
__gmpq_set_str(__gen_e_acsl__13,"1",10);
__gmpq_init(__gen_e_acsl__14);
@@ -415,12 +426,12 @@ double __gen_e_acsl_f2(double x)
__gmpq_div(__gen_e_acsl_div,
(__e_acsl_mpq_struct const *)(__gen_e_acsl__13),
(__e_acsl_mpq_struct const *)(__gen_e_acsl__14));
- __gen_e_acsl__15 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl_div));
+ __gen_e_acsl_cast = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl_div));
__gmpq_clear(__gen_e_acsl__13);
__gmpq_clear(__gen_e_acsl__14);
__gmpq_clear(__gen_e_acsl_div);
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__15); */
- return __gen_e_acsl__15;
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl_cast); */
+ return __gen_e_acsl_cast;
}
int __gen_e_acsl_g(int x)
--
GitLab