diff --git a/dune-project b/dune-project index 81c8d2f091..37e81f4199 100644 --- 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 index 669b2d9c40..b5f1f360dc 100644 --- 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 index 8f98a48e84..7b673f99bc 100644 --- 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 index f96ca832a1..e01560c752 100644 --- 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 index c14bafc0cb..c93244eb47 100644 --- 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