diff --git a/meta_annotate.ml b/meta_annotate.ml
index 451ef6de4b1fd5588484709074f0ef7484fb44b0..3037da982c5c334146c8637e1096e562182f2509 100644
--- a/meta_annotate.ml
+++ b/meta_annotate.ml
@@ -19,6 +19,7 @@
 (*  for more details (enclosed in the file LICENSE)                       *)
 (**************************************************************************)
 
+open Meta_utils
 open Meta_options
 open Meta_parse
 open Meta_dispatch
diff --git a/meta_bindings.ml b/meta_bindings.ml
index 741af90891a76d330aeec344cae876b3e4808674..a4a6edf1764595599b70d082f59eeff13a6a1adf 100644
--- a/meta_bindings.ml
+++ b/meta_bindings.ml
@@ -20,15 +20,14 @@
 (**************************************************************************)
 
 open Meta_options
+open Meta_utils
 open Logic_ptree
 open Logic_typing
 open Cil_types
 
-module Stmt_Hashtbl = Cil_datatype.Stmt.Hashtbl
-
 (* Gathered bindings *)
 let gathered_bindings = ref []
-let types = Hashtbl.create 5
+let types = Str_Hashtbl.create 5
 
 let setname base = base ^ "_set"
 let sizename base = base ^ "_size"
@@ -40,16 +39,16 @@ let capname base = base ^ "_capacity"
 *)
 let parse_bound tc loc quantifiers bn = match bn.lexpr_node with
   | PLvar bname ->
-    let content_type = begin match Hashtbl.find_opt types bname with
+    let content_type = begin match Str_Hashtbl.find_opt types bname with
       | Some x -> x
       | None -> tc.error loc "The name '%s' is used but not bound anywhere" bname
     end in
     let tabvar = tc.find_var (setname bname) in
-    let quantvar = begin match Hashtbl.find_opt quantifiers bname with
+    let quantvar = begin match Str_Hashtbl.find_opt quantifiers bname with
       | Some x -> x
       | None ->
         let res = Cil_const.make_logic_var_quant (bname ^ "_i") Linteger
-        in Hashtbl.add quantifiers bname res; res
+        in Str_Hashtbl.add quantifiers bname res; res
     end in
     let tlv = (TVar tabvar, TIndex (Logic_const.tvar quantvar, TNoOffset)) in
     Logic_const.term (TLval tlv) content_type
@@ -64,8 +63,8 @@ let parse_bind tc loc cvar_name gvar_name =
     | Ctype _ as lt -> lt
     | _ -> tc.error loc "Only C variables can be bound to names"
   end in
-  begin match Hashtbl.find_opt types gvar_name with
-    | None -> Hashtbl.add types gvar_name bdg_type
+  begin match Str_Hashtbl.find_opt types gvar_name with
+    | None -> Str_Hashtbl.add types gvar_name bdg_type
     | Some old_type ->
       if not @@ Logic_utils.is_same_type bdg_type old_type then
         tc.error loc
@@ -91,8 +90,8 @@ let from_id id =
 *)
 let after_parse tc pred quanthash =
   let open Logic_const in
-  let quantifiers = Hashtbl.fold (fun _ -> List.cons) quanthash [] in
-  let conditions = Hashtbl.fold (fun name var conds ->
+  let quantifiers = Str_Hashtbl.fold (fun _ -> List.cons) quanthash [] in
+  let conditions = Str_Hashtbl.fold (fun name var conds ->
       let mainterm = tvar var in
       let sizeterm = tc.find_var (sizename name) |> tvar in
       let supzero = prel (Rle, tinteger 0, mainterm) in
@@ -141,7 +140,7 @@ let add_ghost_code flags =
         Globals.Vars.add cvar sinit;
         GVar (cvar, sinit, unkloc) :: pre
   in
-  let globs = Hashtbl.fold (fun a b c -> (make_global a b) @ c) types [] in
+  let globs = Str_Hashtbl.fold (fun a b c -> (make_global a b) @ c) types [] in
   f.globals <- globs @ f.globals;
   (* Visit the file, resetting to_add when encoutering a function (since sids
    * are unique only within a function) and inserting values of to_add in
@@ -211,10 +210,7 @@ let gf () =
 let process_imeta vis = if !visit_inline then function
     | Ext_id id ->
       let lvar, name = from_id id in
-      let s = begin match vis#current_kinstr with
-        | Kglobal -> assert false
-        | Kstmt s -> s
-      end in
+      let s = Extlib.the vis#current_stmt in
       let gf = gf () in
       List.iter (fun (v : stmt) ->
           add_to_hash_list Stmt_Hashtbl.(find_opt, replace) to_add s v
diff --git a/meta_bindings.mli b/meta_bindings.mli
index 15eccb76dba695f5510452584940474d889e9d5e..d079ec2ff3571b01413ad2dcb3c79b9e90251f3b 100644
--- a/meta_bindings.mli
+++ b/meta_bindings.mli
@@ -21,14 +21,15 @@
 
 open Cil_types
 open Logic_typing
+open Meta_utils
 
-val types : (string, Cil_types.logic_type) Hashtbl.t
+val types : Cil_types.logic_type Str_Hashtbl.t
 val parse_bound : typing_context -> location ->
-  (string, logic_var) Hashtbl.t -> Logic_ptree.lexpr -> term
+  logic_var Str_Hashtbl.t -> Logic_ptree.lexpr -> term
 val parse_bind : typing_context -> location -> string -> string ->
   acsl_extension_kind
 val after_parse : typing_context -> predicate ->
-  (string, logic_var) Hashtbl.t -> predicate
+  logic_var Str_Hashtbl.t -> predicate
 val add_ghost_code : Meta_options.meta_flags -> unit
 
 val process_imeta: Acsl_extension.extension_visitor
diff --git a/meta_deduce.ml b/meta_deduce.ml
index 4b0a0e731e566e3de92df38e07e169852773fc87..e49b569bf6908454fb8ecdd37b2273b5bc2d168b 100644
--- a/meta_deduce.ml
+++ b/meta_deduce.ml
@@ -1,4 +1,5 @@
 open Cil_types
+open Meta_utils
 open Meta_options
 open Meta_parse
 
diff --git a/meta_dispatch.ml b/meta_dispatch.ml
index 7d68eb64a2091b774052b4e57028e58e65470987..020c04a0c7437d8f1f29d6c0fb2c0e2f4512d0df 100644
--- a/meta_dispatch.ml
+++ b/meta_dispatch.ml
@@ -20,6 +20,7 @@
 (**************************************************************************)
 
 open Cil_types
+open Meta_utils
 open Meta_parse
 open Meta_options
 
diff --git a/meta_dispatch.mli b/meta_dispatch.mli
index b70d07be512caa65603993a035e93b92dc63c788..3232d36291d53e0260d8e77ba37d14b2dbc115c7 100644
--- a/meta_dispatch.mli
+++ b/meta_dispatch.mli
@@ -20,6 +20,7 @@
 (**************************************************************************)
 
 open Cil_types
+open Meta_utils
 open Meta_parse
 open Meta_options
 
diff --git a/meta_options.ml b/meta_options.ml
index 09ab6019bf3eaca44d9db78709eb0f3eacdc6d8a..937e8b6f72eb9686165b9ee9379e88bcf6d591d8 100644
--- a/meta_options.ml
+++ b/meta_options.ml
@@ -107,14 +107,3 @@ type meta_flags = {
   keep_proof_files : bool;
   default_to_assert : bool;
 }
-
-let find_hash_list find_opt table key =
-  match find_opt table key with
-    | Some l -> l
-    | None -> []
-
-(* In a hashtable mapping key to lists of values, adds v to that list *)
-let add_to_hash_list (find_opt, replace) table key v =
-  let old_list = find_hash_list find_opt table key in
-  replace table key (v :: old_list)
-
diff --git a/meta_parse.ml b/meta_parse.ml
index 618d6340ed49eca22f6070545d69cc9d8759a50f..f5688bb037a4bd6e1fb96ef958de4524c63dffa3 100644
--- a/meta_parse.ml
+++ b/meta_parse.ml
@@ -23,6 +23,7 @@ open Logic_ptree
 open Logic_typing
 open Cil_types
 open Meta_options
+open Meta_utils
 
 (* Define builtins *)
 type context =
@@ -34,11 +35,6 @@ type context =
   | Postcond
   | Precond
 
-module StrSet = Datatype.String.Set
-module Str_Hashtbl = Datatype.String.Hashtbl
-module Stmt_Hashtbl = Cil_datatype.Stmt.Hashtbl
-module Fundec_Hashtbl = Cil_datatype.Fundec.Hashtbl
-
 type target =
   | TgAll
   | TgSet of StrSet.t
@@ -154,7 +150,7 @@ let meta_type_term termassoc quantifiers kf loc orig_ctxt meta_ctxt env expr =
  * a full custom predicate
 *)
 let process_meta_termassoc typing_context loc expr kf termassoc =
-  let quantifiers = Hashtbl.create 5 in
+  let quantifiers = Str_Hashtbl.create 5 in
   let meta_tc =
     {typing_context with
        type_predicate = (meta_type_predicate loc typing_context);
@@ -463,8 +459,9 @@ let metaproperties () =
       !gathered_props in
   begin match check_for_duplicates sorted_props with
     | None -> ()
-    | Some (m1, m2) -> Self.abort "The meta-property named %s is defined at \
-                                   least twice :@,Here: %a@,and here: %a" m1.mp_name Printer.pp_location m1.mp_loc
-                         Printer.pp_location m2.mp_loc
+    | Some (m1, m2) ->
+      Self.abort "The meta-property named %s is defined at \
+                  least twice :@,Here: %a@,and here: %a"
+        m1.mp_name Printer.pp_location m1.mp_loc Printer.pp_location m2.mp_loc
   end ;
   List.rev !gathered_props
diff --git a/meta_parse.mli b/meta_parse.mli
index a8d26d7960c9d6ca9ec609f95ff8bf43ec93780c..cc62307e7304f0804d51b601116209d0a0599deb 100644
--- a/meta_parse.mli
+++ b/meta_parse.mli
@@ -20,6 +20,7 @@
 (**************************************************************************)
 
 open Cil_types
+open Meta_utils
 
 type context =
   | Weak_invariant
@@ -30,11 +31,6 @@ type context =
   | Postcond
   | Precond
 
-module StrSet = Datatype.String.Set
-module Str_Hashtbl = Datatype.String.Hashtbl
-module Stmt_Hashtbl = Cil_datatype.Stmt.Hashtbl
-module Fundec_Hashtbl = Cil_datatype.Fundec.Hashtbl
-
 type target =
   | TgAll
   | TgSet of StrSet.t
diff --git a/meta_utils.ml b/meta_utils.ml
new file mode 100644
index 0000000000000000000000000000000000000000..41e812ea72445dc0ab3f00d8f6223e8680ee655d
--- /dev/null
+++ b/meta_utils.ml
@@ -0,0 +1,15 @@
+module StrSet = Datatype.String.Set
+module Str_Hashtbl = Datatype.String.Hashtbl
+module Stmt_Hashtbl = Cil_datatype.Stmt.Hashtbl
+module Fundec_Hashtbl = Cil_datatype.Fundec.Hashtbl
+
+let find_hash_list find_opt table key =
+  match find_opt table key with
+    | Some l -> l
+    | None -> []
+
+(* In a hashtable mapping key to lists of values, adds v to that list *)
+let add_to_hash_list (find_opt, replace) table key v =
+  let old_list = find_hash_list find_opt table key in
+  replace table key (v :: old_list)
+