From 13eb8d94e5220fbd6007400e4805e2a1834daf85 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 11 Jul 2019 16:16:28 +0200
Subject: [PATCH] [Eva] Eval_terms: minor simplification by creating and using
efloat as ereal.
---
src/plugins/value/legacy/eval_terms.ml | 24 ++++++++++++------------
1 file changed, 12 insertions(+), 12 deletions(-)
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 34d987a154e..a132819cbe1 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -446,9 +446,13 @@ let einteger v =
(* Note: some reals cannot be exactly represented as floats; in which
case we do not know their under-approximation. *)
-let ereal v =
+let efloating_point etype fval =
+ let v = V.inject_float fval in
let eunder = under_from_over v in
- { etype = Cil.doubleType; eunder; eover = v; ldeps = empty_logic_deps }
+ { etype; eunder; eover = v; ldeps = empty_logic_deps }
+
+let ereal = efloating_point Cil.doubleType
+let efloat = efloating_point Cil.floatType
let is_true = function
| `True | `TrueReduced _ -> true
@@ -725,7 +729,7 @@ let rec eval_term ~alarm_mode env t =
let r_lower = Fval.F.of_float r_lower in
let r_upper = Fval.F.of_float r_upper in
let f = Fval.inject Fval.Real r_lower r_upper in
- ereal (V.inject_ival (Ival.inject_float f))
+ ereal f
end
(* | TConst ((CStr | CWstr) Missing cases *)
@@ -745,17 +749,13 @@ let rec eval_term ~alarm_mode env t =
eover = loc_bits_to_loc_bytes r.eover }
(* Special case for the constants \pi, \e, \infinity and \NaN. *)
- | TLval (TVar {lv_name = "\\pi"}, _) -> ereal (V.inject_float Fval.pi)
- | TLval (TVar {lv_name = "\\e"}, _) -> ereal (V.inject_float Fval.e)
+ | TLval (TVar {lv_name = "\\pi"}, _) -> ereal Fval.pi
+ | TLval (TVar {lv_name = "\\e"}, _) -> ereal Fval.e
| TLval (TVar {lv_name = "\\plus_infinity"}, _) ->
- let v = V.inject_float (Fval.pos_infinity Float_sig.Single) in
- { etype = Cil.floatType; eunder = v; eover = v; ldeps = empty_logic_deps }
+ efloat Fval.(pos_infinity Single)
| TLval (TVar {lv_name = "\\minus_infinity"}, _) ->
- let v = V.inject_float (Fval.neg_infinity Float_sig.Single) in
- { etype = Cil.floatType; eunder = v; eover = v; ldeps = empty_logic_deps }
- | TLval (TVar {lv_name = "\\NaN"}, _) ->
- let v = V.inject_float Fval.nan in
- { etype = Cil.floatType; eunder = v; eover = v; ldeps = empty_logic_deps }
+ efloat Fval.(neg_infinity Single)
+ | TLval (TVar {lv_name = "\\NaN"}, _) -> efloat Fval.nan
| TLval _ ->
let lval = eval_tlval ~alarm_mode env t in
--
GitLab