Merge pull request #1282 from goblint/batteries_bump

Bump batteries to 3.5.1 & Remove hacks
goblint · Dec 7, 2023 · 1110826 · 1110826
2 parents 9023dc8 + aa7a8bb
commit 1110826
Show file tree

Hide file tree

Showing 5 changed files with 4 additions and 14 deletions.
diff --git a/dune-project b/dune-project
@@ -25,7 +25,7 @@
   (depends
     (ocaml (>= 4.10))
     (goblint-cil (>= 2.0.3)) ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint.
-    (batteries (>= 3.5.0))
+    (batteries (>= 3.5.1))
     (zarith (>= 1.8))
     (yojson (>= 2.0.0))
     (qcheck-core (>= 0.19))

diff --git a/goblint.opam b/goblint.opam
@@ -22,7 +22,7 @@ depends: [
   "dune" {>= "3.7"}
   "ocaml" {>= "4.10"}
   "goblint-cil" {>= "2.0.3"}
-  "batteries" {>= "3.5.0"}
+  "batteries" {>= "3.5.1"}
   "zarith" {>= "1.8"}
   "yojson" {>= "2.0.0"}
   "qcheck-core" {>= "0.19"}

diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml
@@ -475,7 +475,7 @@ let createCFG (file: file) =
     );
   if Messages.tracing then Messages.trace "cfg" "CFG building finished.\n\n";
   if get_bool "dbg.verbose" then
-    ignore (Pretty.eprintf "cfgF (%a), cfgB (%a)\n" GobHashtbl.pretty_statistics (GobHashtbl.magic_stats cfgF) GobHashtbl.pretty_statistics (GobHashtbl.magic_stats cfgB));
+    ignore (Pretty.eprintf "cfgF (%a), cfgB (%a)\n" GobHashtbl.pretty_statistics (NH.stats cfgF) GobHashtbl.pretty_statistics (NH.stats cfgB));
   cfgF, cfgB, skippedByEdge
 
 let createCFG = Timing.wrap "createCFG" createCFG

diff --git a/src/solvers/postSolver.ml b/src/solvers/postSolver.ml
@@ -154,13 +154,7 @@ struct
 
   module VH = Hashtbl.Make (S.Var)
   (* starts as Hashtbl for quick lookup *)
-  let starth =
-    (* VH.of_list S.starts *) (* TODO: BatHashtbl.Make.of_list is broken, use after new Batteries release *)
-    let starth = VH.create (List.length S.starts) in
-    List.iter (fun (x, d) ->
-        VH.replace starth x d
-      ) S.starts;
-    starth
+  let starth = VH.of_list S.starts
 
   let system x =
     match S.system x, VH.find_option starth x with

diff --git a/src/util/std/gobHashtbl.ml b/src/util/std/gobHashtbl.ml
@@ -1,9 +1,5 @@
 module Pretty = GoblintCil.Pretty
 
-let magic_stats h =
-  let h: _ Hashtbl.t = Obj.magic h in (* Batteries Hashtables don't expose stats yet...: https://github.com/ocaml-batteries-team/batteries-included/pull/1079 *)
-  Hashtbl.stats h
-
 let pretty_statistics () (s: Hashtbl.statistics) =
   let load_factor = float_of_int s.num_bindings /. float_of_int s.num_buckets in
   Pretty.dprintf "bindings=%d buckets=%d max_length=%d histo=%a load=%f" s.num_bindings s.num_buckets s.max_bucket_length (Pretty.docList (Pretty.dprintf "%d")) (Array.to_list s.bucket_histogram) load_factor