add Dudeldu's fix for DBL_MIN/DBL_MAX

src/analyses/base.ml

@@ -730,8 +730,8 @@ struct
       | Const (CReal (_, (FFloat | FDouble as fkind), Some str)) -> `Float (FD.of_string fkind str) (* prefer parsing from string due to higher precision *)
       | Const (CReal (num, (FFloat | FDouble as fkind), None)) -> `Float (FD.of_const fkind num)
       (* this is so far only for DBL_MIN/DBL_MAX as it is represented as LongDouble although it would fit into a double as well *)
-      | Const (CReal (_, (FLongDouble), Some str)) when str = "2.2250738585072014e-308L" -> `Float (FD.of_string FDouble str)
-      | Const (CReal (_, (FLongDouble), Some str)) when str = "1.7976931348623157e+308L" -> `Float (FD.of_string FDouble str)
+      | Const (CReal (num, (FLongDouble), _)) when Stdlib.Float.abs num = Stdlib.Float.min_float -> `Float (FD.of_const FDouble num)
+      | Const (CReal (num, (FLongDouble), _)) when Stdlib.Float.abs num = Stdlib.Float.max_float -> `Float (FD.of_const FDouble num)
       (* String literals *)
       | Const (CStr (x,_)) -> `Address (AD.from_string x) (* normal 8-bit strings, type: char* *)
       | Const (CWStr (xs,_) as c) -> (* wide character strings, type: wchar_t* *)

tests/regression/56-floats/06-library_functions.c

@@ -4,7 +4,6 @@
 #include <float.h>
 
 int main() {
-    double dbl_min = 2.2250738585072014e-308;
     double inf = 1. / 0.;
     double nan = 0. / 0.;
 
@@ -30,9 +29,9 @@ int main() {
     assert(__builtin_isnan(nan)); //UNKNOWN
 
     //__buitin_isnormal(x):
-    assert(__builtin_isnormal(dbl_min)); //SUCCESS!
+    assert(__builtin_isnormal(DBL_MIN)); //SUCCESS!
     assert(__builtin_isnormal(0.0)); //FAIL!
-    assert(__builtin_isnormal(dbl_min / 2)); //FAIL!
+    assert(__builtin_isnormal(DBL_MIN / 2)); //FAIL!
     assert(__builtin_isnormal(inf)); //UNKNOWN
     assert(__builtin_isnormal(nan)); //UNKNOWN