From e18ad67b0170095b5d0c8b8e2a7fa6371e57aa4d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Wed, 16 Feb 2022 17:23:01 +0100
Subject: [PATCH] [IVal] float to int32
topify can create top for floats
---
src/kernel_services/abstract_interp/ival.ml | 8 +++++---
1 file changed, 5 insertions(+), 3 deletions(-)
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index 5022d6fd6ad..ef21fe8eec6 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -882,9 +882,11 @@ let cast_float_to_int_non_nan ~signed ~size (min, max) =
assert false (* impossible if min-max are correct *)
let cast_float_to_int ~signed ~size iv =
- match Fval.min_and_max (project_float iv) with
- | Some (min, max), _nan -> cast_float_to_int_non_nan ~signed ~size (min, max)
- | None, _ -> bottom (* means NaN *)
+ if equal top iv then top
+ else
+ match Fval.min_and_max (project_float iv) with
+ | Some (min, max), _nan -> cast_float_to_int_non_nan ~signed ~size (min, max)
+ | None, _ -> bottom (* means NaN *)
(* These are the bounds of the range of integers that can be represented
--
GitLab