From 05895870779a3b3a437d0cf93c1dfabc8e8cda59 Mon Sep 17 00:00:00 2001 From: Dudeldu Date: Fri, 15 Jul 2022 16:08:07 +0200 Subject: [PATCH 1/2] Find another location where get_ikind results in an error --- src/cdomains/valueDomain.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml index 5fa89cc13f..f94392b989 100644 --- a/src/cdomains/valueDomain.ml +++ b/src/cdomains/valueDomain.ml @@ -267,8 +267,9 @@ struct let is_safe_cast t2 t1 = match t2, t1 with (*| TPtr _, t -> bitsSizeOf t <= bitsSizeOf !upointType | t, TPtr _ -> bitsSizeOf t >= bitsSizeOf !upointType*) - | TInt (ik,_), TFloat (fk,_) (* does a1 fit into ik's range? *) - | TFloat (fk,_), TInt (ik,_) (* can a1 be represented as fk? *) + | TFloat (fk1,_), TFloat (fk2,_) when fk1 = fk2 -> true + | _, TFloat (fk,_) (* does a1 fit into ik's range? *) + | TFloat (fk,_), _ (* can a1 be represented as fk? *) -> false (* TODO precision *) | _ -> IntDomain.Size.is_cast_injective ~from_type:t1 ~to_type:t2 && bitsSizeOf t2 >= bitsSizeOf t1 (*| _ -> false*) From ff56a9ef0bb6880b2a4feb8ff3c7e0fe5a3e0af0 Mon Sep 17 00:00:00 2001 From: Dudeldu Date: Mon, 18 Jul 2022 14:59:39 +0200 Subject: [PATCH 2/2] Further refine determining safe casts with floats --- src/cdomains/valueDomain.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml index f94392b989..4ada05de61 100644 --- a/src/cdomains/valueDomain.ml +++ b/src/cdomains/valueDomain.ml @@ -268,9 +268,13 @@ struct (*| TPtr _, t -> bitsSizeOf t <= bitsSizeOf !upointType | t, TPtr _ -> bitsSizeOf t >= bitsSizeOf !upointType*) | TFloat (fk1,_), TFloat (fk2,_) when fk1 = fk2 -> true - | _, TFloat (fk,_) (* does a1 fit into ik's range? *) - | TFloat (fk,_), _ (* can a1 be represented as fk? *) - -> false (* TODO precision *) + | TFloat (FDouble,_), TFloat (FFloat,_) -> true + | TFloat (FLongDouble,_), TFloat (FFloat,_) -> true + | TFloat (FLongDouble,_), TFloat (FDouble,_) -> true + | _, TFloat _ -> false (* casting float to an integral type always looses the decimals *) + | TFloat ((FFloat | FDouble | FLongDouble), _), TInt((IBool | IChar | IUChar | ISChar | IShort | IUShort), _) -> true (* resonably small integers can be stored in all fkinds *) + | TFloat ((FDouble | FLongDouble), _), TInt((IInt | IUInt | ILong | IULong), _) -> true (* values stored in between 16 and 32 bits can only be stored in at least doubles *) + | TFloat _, _ -> false (* all wider integers can not be completly put into a float, partially because our internal representation of long double is the same as for doubles *) | _ -> IntDomain.Size.is_cast_injective ~from_type:t1 ~to_type:t2 && bitsSizeOf t2 >= bitsSizeOf t1 (*| _ -> false*)