Skip to content

Commit

Permalink
Allow using DBL_MIN
Browse files Browse the repository at this point in the history
Some compilers specifiy DBL_MIN as long double.
As we do not support long double in neither cil nor goblint itself,
 but want to use DBL_MIN we have no other option than to explicitly check for this one case
  • Loading branch information
Dudeldu committed Jun 11, 2022
1 parent a27a501 commit 715d6ae
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions src/analyses/base.ml
Original file line number Diff line number Diff line change
Expand Up @@ -731,6 +731,8 @@ struct
| Const (CReal (_, (FDouble as fkind), Some str)) -> `Float (FD.of_string fkind str) (* prefer parsing from string due to higher precision *)
| Const (CReal (num, (FFloat as fkind), None))
| Const (CReal (num, (FDouble as fkind), None)) -> `Float (FD.of_const fkind num)
(* this is so far only for DBL_MIN 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)
(* 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* *)
Expand Down

0 comments on commit 715d6ae

Please sign in to comment.