From 49e355e883a448447b9b9100fa8aa94ab7107fb7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 5 May 2021 11:10:26 +0200
Subject: [PATCH] [Eva] Fixes a crash on INFINITY with option
-eva-all-rounding-modes-constants.
---
src/plugins/value/values/cvalue_forward.ml | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/src/plugins/value/values/cvalue_forward.ml b/src/plugins/value/values/cvalue_forward.ml
index 532fc15103f..aabd38688fe 100644
--- a/src/plugins/value/values/cvalue_forward.ml
+++ b/src/plugins/value/values/cvalue_forward.ml
@@ -528,9 +528,10 @@ let eval_float_constant f fkind fstring =
if Fc_float.is_nan f
then V.inject_float Fval.nan
else
+ let all_rounding = Value_parameters.AllRoundingModesConstants.get in
let fl, fu = match fstring with
- | Some string when fkind = Cil_types.FLongDouble ||
- Value_parameters.AllRoundingModesConstants.get () ->
+ | Some "INFINITY" -> f, f (* Special case for the INFINITY macro. *)
+ | Some string when fkind = Cil_types.FLongDouble || all_rounding () ->
let open Floating_point in
let {f_lower; f_upper} = snd (parse string) in
(* Computations are done in double. For long double constants, if we
--
GitLab