Merge pull request #1202 from goblint/long_double_constant_warning

Remove spurious `long double` constant warning
goblint · Oct 4, 2023 · 475f3bb · 475f3bb
2 parents a9f2bae + 058990e
commit 475f3bb
Show file tree

Hide file tree

Showing 7 changed files with 17 additions and 5 deletions.
diff --git a/goblint.opam b/goblint.opam
@@ -75,7 +75,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # also remember to generate/adjust goblint.opam.locked!
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
-  [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#398dca3d94a06a9026b3737aabf100ee3498229f" ]
+  [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#c7ffc37ad83216a84d90fdbf427cc02a68ea5331" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
 ]

diff --git a/goblint.opam.locked b/goblint.opam.locked
@@ -132,7 +132,7 @@ post-messages: [
 pin-depends: [
   [
     "goblint-cil.2.0.2"
-    "git+https://github.com/goblint/cil.git#398dca3d94a06a9026b3737aabf100ee3498229f"
+    "git+https://github.com/goblint/cil.git#c7ffc37ad83216a84d90fdbf427cc02a68ea5331"
   ]
   [
     "ppx_deriving.5.2.1"

diff --git a/goblint.opam.template b/goblint.opam.template
@@ -2,7 +2,7 @@
 # also remember to generate/adjust goblint.opam.locked!
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
-  [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#398dca3d94a06a9026b3737aabf100ee3498229f" ]
+  [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#c7ffc37ad83216a84d90fdbf427cc02a68ea5331" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
 ]

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -761,7 +761,8 @@ struct
         (match str with Some x -> M.tracel "casto" "CInt (%s, %a, %s)\n" (Z.to_string num) d_ikind ikind x | None -> ());
         Int (ID.cast_to ikind (IntDomain.of_const (num,ikind,str)))
       | Const (CReal (_,fkind, Some str)) when not (Cilfacade.isComplexFKind fkind) -> Float (FD.of_string fkind str) (* prefer parsing from string due to higher precision *)
-      | Const (CReal (num, fkind, None)) when not (Cilfacade.isComplexFKind fkind) -> Float (FD.of_const fkind num)
+      | Const (CReal (num, fkind, None)) when not (Cilfacade.isComplexFKind fkind) && num = 0.0 -> Float (FD.of_const fkind num) (* constant 0 is ok, CIL creates these for zero-initializers; it is safe across float types *)
+      | Const (CReal (_, fkind, None)) when not (Cilfacade.isComplexFKind fkind) ->  assert false (* Cil does not create other CReal without string representation *)
       (* String literals *)
       | Const (CStr (x,_)) -> Address (AD.of_string x) (* normal 8-bit strings, type: char* *)
       | Const (CWStr (xs,_) as c) -> (* wide character strings, type: wchar_t* *)

diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml
@@ -51,7 +51,8 @@ let init () =
   (* lineDirectiveStyle := None; *)
   RmUnused.keepUnused := true;
   print_CIL_Input := true;
-  Cabs2cil.allowDuplication := false
+  Cabs2cil.allowDuplication := false;
+  Cabs2cil.silenceLongDoubleWarning := true
 
 let current_file = ref dummyFile
 

diff --git a/tests/regression/00-sanity/37-long-double.c b/tests/regression/00-sanity/37-long-double.c
@@ -0,0 +1,4 @@
+int main() {
+  long double l = 0.0L;
+  return (int)l;
+}
diff --git a/tests/regression/00-sanity/37-long-double.t b/tests/regression/00-sanity/37-long-double.t
@@ -0,0 +1,6 @@
+Testing that there isn't a warning about treating long double as double constant.
+  $ goblint 37-long-double.c
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 3
+    dead: 0
+    total lines: 3