From 5cda474f09f130558c256234d129bee59780bd32 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 5 Feb 2020 17:45:24 +0100
Subject: [PATCH] [Eva] Eval_terms: minor simplification in the evaluation of
TLogic_coerce.
---
src/plugins/value/legacy/eval_terms.ml | 24 +++++++++---------------
1 file changed, 9 insertions(+), 15 deletions(-)
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 45ec10860ae..843617e78ab 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -992,21 +992,15 @@ let rec eval_term ~alarm_mode env t =
|| Logic_const.is_boolean_type t.term_type -> r
| Ctype typ when Cil.isIntegralOrPointerType typ -> r
| Lreal ->
- if Logic_typing.is_integral_type t.term_type
- then (* Needs to be converted to reals *)
- let eover = V.cast_int_to_float Fval.Real r.eover in
- { etype = Cil.longDoubleType; (** hack until logic type *)
- ldeps = r.ldeps;
- eunder = under_from_over eover;
- eover;
- empty = r.empty; }
- else
- let eover = V.cast_float_to_float Fval.Real r.eover in
- { etype = Cil.longDoubleType; (** hack until logic type *)
- ldeps = r.ldeps;
- eunder = under_from_over eover;
- eover;
- empty = r.empty }
+ let eover =
+ if Logic_typing.is_integral_type t.term_type
+ then V.cast_int_to_float Fval.Real r.eover
+ else V.cast_float_to_float Fval.Real r.eover
+ in
+ { etype = Cil.longDoubleType; (** hack until logic type *)
+ ldeps = r.ldeps;
+ eover; eunder = under_from_over eover;
+ empty = r.empty }
| _ ->
if Logic_const.is_boolean_type ltyp
&& Logic_typing.is_integral_type t.term_type
--
GitLab