diff --git a/goblint.opam b/goblint.opam index a4b0fc7c42..c04baad8f2 100644 --- a/goblint.opam +++ b/goblint.opam @@ -101,8 +101,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git" # also remember to generate/adjust goblint.opam.locked! available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos") pin-depends: [ - # published goblint-cil 2.0.6 is currently up-to-date, but pinned for reproducibility - [ "goblint-cil.2.0.6" "git+https://github.com/goblint/cil.git#4b8b06eb39801a87d195f81d830a686578bd8b8b" ] + [ "goblint-cil.2.0.7" "git+https://github.com/goblint/cil.git#8e2212316ceda6911de2db716933bfb8c64a8585" ] # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ] ] diff --git a/goblint.opam.locked b/goblint.opam.locked index 761959553a..2fa17c8148 100644 --- a/goblint.opam.locked +++ b/goblint.opam.locked @@ -66,7 +66,7 @@ depends: [ "fileutils" {= "0.6.4"} "fmt" {= "0.9.0"} "fpath" {= "0.7.3"} - "goblint-cil" {= "2.0.6"} + "goblint-cil" {= "2.0.7"} "hex" {= "1.5.0"} "integers" {= "0.7.0"} "json-data-encoding" {= "1.0.1"} @@ -142,8 +142,8 @@ post-messages: [ ] pin-depends: [ [ - "goblint-cil.2.0.6" - "git+https://github.com/goblint/cil.git#4b8b06eb39801a87d195f81d830a686578bd8b8b" + "goblint-cil.2.0.7" + "git+https://github.com/goblint/cil.git#8e2212316ceda6911de2db716933bfb8c64a8585" ] [ "apron.v0.9.15" diff --git a/goblint.opam.template b/goblint.opam.template index 2cdc1bc245..a576e48e3e 100644 --- a/goblint.opam.template +++ b/goblint.opam.template @@ -2,7 +2,7 @@ # also remember to generate/adjust goblint.opam.locked! available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos") pin-depends: [ - [ "goblint-cil.2.0.6" "git+https://github.com/goblint/cil.git#4b8b06eb39801a87d195f81d830a686578bd8b8b" ] + [ "goblint-cil.2.0.7" "git+https://github.com/goblint/cil.git#8e2212316ceda6911de2db716933bfb8c64a8585" ] # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ] ] diff --git a/gobview b/gobview index a35d51b48e..6dc30326fb 160000 --- a/gobview +++ b/gobview @@ -1 +1 @@ -Subproject commit a35d51b48eaecfa68ecd1ead2ecfa94aa1c370f4 +Subproject commit 6dc30326fbb72c2cae0a96b9f407db6dd91fb213 diff --git a/src/cdomain/value/cdomains/floatDomain.ml b/src/cdomain/value/cdomains/floatDomain.ml index d1ef6ce3c0..d3ed4e5f71 100644 --- a/src/cdomain/value/cdomains/floatDomain.ml +++ b/src/cdomain/value/cdomains/floatDomain.ml @@ -1002,10 +1002,15 @@ module FloatIntervalImplLifted = struct | FDouble -> F64 (op64 ()) | FLongDouble -> FLong (op64 ()) | FFloat128 -> FFloat128 (op64 ()) - | _ -> + | FFloat16 -> failwith "fkind FFloat16 not supported" + | FComplexFloat + | FComplexDouble + | FComplexLongDouble + | FComplexFloat128 + | FComplexFloat16 -> (* this should never be reached, as we have to check for invalid fkind elsewhere, however we could instead of crashing also return top_of some fkind to avoid this and nonetheless have no actual information about anything*) - failwith "unsupported fkind" + failwith "complex fkind not supported" let neg = lift (F1.neg, F2.neg) let fabs = lift (F1.fabs, F2.fabs) diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml index c866bb34ab..f5e5eb1703 100644 --- a/src/cdomain/value/cdomains/valueDomain.ml +++ b/src/cdomain/value/cdomains/valueDomain.ml @@ -357,13 +357,18 @@ struct (*| TPtr _, t -> bitsSizeOf t <= bitsSizeOf !upointType | t, TPtr _ -> bitsSizeOf t >= bitsSizeOf !upointType*) | TFloat (fk1,_), TFloat (fk2,_) when fk1 = fk2 -> true + | TFloat (FFloat,_), TFloat (FFloat16,_) -> true | TFloat (FDouble,_), TFloat (FFloat,_) -> true + | TFloat (FDouble,_), TFloat (FFloat16,_) -> true | TFloat (FLongDouble,_), TFloat (FFloat,_) -> true | TFloat (FLongDouble,_), TFloat (FDouble,_) -> true + | TFloat (FLongDouble,_), TFloat (FFloat16,_) -> true | TFloat (FFloat128, _), TFloat (FFloat,_) -> true | TFloat (FFloat128, _), TFloat (FDouble,_) -> true | TFloat (FFloat128, _), TFloat (FLongDouble,_) -> true + | TFloat (FFloat128, _), TFloat (FFloat16,_) -> true | _, TFloat _ -> false (* casting float to an integral type always looses the decimals *) + | TFloat (FFloat16, _), (TInt((IBool | IChar | IUChar | ISChar), _) | TEnum ({ekind = IBool | IChar | IUChar | ISChar; _}, _)) -> true (* reasonably small integers can be stored in _Float16 *) | TFloat (fk, _), (TInt((IBool | IChar | IUChar | ISChar | IShort | IUShort), _) | TEnum ({ekind = IBool | IChar | IUChar | ISChar | IShort | IUShort; _}, _)) when not (Cilfacade.isComplexFKind fk) -> true (* reasonably small integers can be stored in all fkinds *) | TFloat ((FDouble | FLongDouble | FFloat128), _), (TInt((IInt | IUInt | ILong | IULong), _) | TEnum ({ekind = 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 completely put into a float, partially because our internal representation of long double is the same as for doubles *) diff --git a/src/common/util/cilType.ml b/src/common/util/cilType.ml index 91368052b3..d50f288a43 100644 --- a/src/common/util/cilType.ml +++ b/src/common/util/cilType.ml @@ -144,10 +144,12 @@ struct | FDouble | FLongDouble | FFloat128 + | FFloat16 | FComplexFloat | FComplexDouble | FComplexLongDouble | FComplexFloat128 + | FComplexFloat16 [@@deriving hash] (* Hashtbl.hash doesn't monomorphize, so derive instead. *) diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml index 6d0738db8a..c06b511e2a 100644 --- a/src/common/util/cilfacade.ml +++ b/src/common/util/cilfacade.ml @@ -288,10 +288,12 @@ let typeOfRealAndImagComponents t = | FDouble -> FDouble (* [double] *) | FLongDouble -> FLongDouble (* [long double] *) | FFloat128 -> FFloat128 (* [float128] *) + | FFloat16 -> FFloat16 (* [_Float16] *) | FComplexFloat -> FFloat | FComplexDouble -> FDouble | FComplexLongDouble -> FLongDouble | FComplexFloat128 -> FComplexFloat128 + | FComplexFloat16 -> FComplexFloat16 in TFloat (newfkind fkind, attrs) | _ -> raise (TypeOfError RealImag_NonNumerical) @@ -300,11 +302,13 @@ let isComplexFKind = function | FFloat | FDouble | FLongDouble - | FFloat128 -> false + | FFloat128 + | FFloat16 -> false | FComplexFloat | FComplexDouble | FComplexLongDouble - | FComplexFloat128 -> true + | FComplexFloat128 + | FComplexFloat16 -> true (** @raise TypeOfError *) let rec typeOf (e: exp) : typ =