diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 339744070b2ce9c7b7f58482accc4c2b03a2ca7b..6eb4e0d120f666ee9cd726cf8afee6eff7c3485e 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -628,19 +628,6 @@ module Value = struct
   let access =  mk_fun "Value.access"
   let access_expr =  mk_fun "Value.access_expr"
 
-  (** Type for a Value builtin function *)
-
-  type builtin_type = unit -> typ * typ list
-  type builtin =
-      state ->
-      (Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->
-      Value_types.call_result
-
-  exception Outside_builtin_possibilities
-  let register_builtin = mk_fun "Value.register_builtin"
-  let registered_builtins = mk_fun "Value.registered_builtins"
-  let mem_builtin = mk_fun "Value.mem_builtin"
-
   let use_spec_instead_of_definition =
     mk_fun "Value.use_spec_instead_of_definition"
 
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 30c474f13e54fc9f343a44f0492a507f23476459..51a0b971add1479d07077ffe433626b167bf4c08 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -175,40 +175,6 @@ module Value : sig
 
   (** {3 Parameterization} *)
 
-  exception Outside_builtin_possibilities
-
-  (* Type of a C function interpreted by a builtin:
-     return type and list of argument types. *)
-  type builtin_type = unit -> typ * typ list
-
-  (** Type for an Eva builtin function *)
-  type builtin =
-    (** Memory state at the beginning of the function *)
-    state ->
-    (** Args for the function: the expressions corresponding to the formals
-        of the functions at the call site, the actual value of those formals,
-        and a more precise view of those formals using offsetmaps (for eg.
-        structs)  *)
-    (Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->
-    Value_types.call_result
-
-  val register_builtin:
-    (string -> ?replace:string -> ?typ:builtin_type -> builtin -> unit) ref
-  (** [!register_builtin name ?replace ?typ f] registers an abstract function
-      [f] to use everytime a C function named [name] of type [typ] is called in
-      the program.  If [replace] is supplied and option [-eva-builtins-auto] is
-      active, calls to [replace] will also be substituted by the builtin.  See
-      also option [-eva-builtin] *)
-
-  val registered_builtins: (unit -> (string * builtin) list) ref
-  (** Returns a list of the pairs (name, builtin) registered via
-      [register_builtin].
-      @since Aluminium-20160501 *)
-
-  val mem_builtin: (string -> bool) ref
-  (** returns whether there is an abstract function registered by
-      {!register_builtin} with the given name. *)
-
   val use_spec_instead_of_definition: (kernel_function -> bool) ref
   (** To be called by derived analyses to determine if they must use
       the body of the function (if available), or only its spec. Used for
diff --git a/src/plugins/aorai/aorai_eva_analysis.enabled.ml b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
index 6677062252912351507f77c28f5e9a6ae6e0851a..c1e43ded459a6475ef5b00f4854620914fd5201a 100644
--- a/src/plugins/aorai/aorai_eva_analysis.enabled.ml
+++ b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
@@ -41,7 +41,7 @@ let show_val fmt (expr, v, _) =
 
 let show_aorai_state = "Frama_C_show_aorai_state"
 
-let builtin_show_aorai_state state args =
+let _builtin_show_aorai_state state args =
   if not (Aorai_option.Deterministic.get()) then begin
     Aorai_option.warning
       ~current:true "%s can only display info for deterministic automata"
@@ -67,9 +67,6 @@ let () =
   Cil_builtins.add_custom_builtin
     (fun () -> (show_aorai_state,Cil.voidType,[],true))
 
-let () =
-  !Db.Value.register_builtin show_aorai_state builtin_show_aorai_state
-
 let add_slevel_annotation vi kind =
   match kind with
   | Aorai_visitors.Aux_funcs.(Pre _ | Post _) ->
diff --git a/src/plugins/metrics/metrics_base.ml b/src/plugins/metrics/metrics_base.ml
index e1cc6633a3aaf5a0da94b4553690eb766ec501cc..36624ef260bbbd07334c9c915dd589f59173926d 100644
--- a/src/plugins/metrics/metrics_base.ml
+++ b/src/plugins/metrics/metrics_base.ml
@@ -365,7 +365,7 @@ let get_filename fdef =
 ;;
 
 let consider_function ~libc vinfo =
-  not (!Db.Value.mem_builtin vinfo.vname
+  not (false
        || Ast_info.is_frama_c_builtin vinfo.vname
        || Cil_builtins.is_unused_builtin vinfo
       ) && (libc || not (Cil.is_in_libc vinfo.vattr))
diff --git a/src/plugins/value/domains/cvalue/builtins.ml b/src/plugins/value/domains/cvalue/builtins.ml
index ba5c2f99bb99deed6fa3ad25c6140ab5359c25db..4767c0a69f5de34be850afaff5f549a182cac1dd 100644
--- a/src/plugins/value/domains/cvalue/builtins.ml
+++ b/src/plugins/value/domains/cvalue/builtins.ml
@@ -24,6 +24,14 @@ open Cil_types
 open Cvalue
 
 exception Invalid_nb_of_args of int
+exception Outside_builtin_possibilities
+
+type builtin_type = unit -> typ * typ list
+
+type builtin =
+  Cvalue.Model.t ->
+  (Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->
+  Value_types.call_result
 
 (* 'Always' means the builtin will always be used to replace a function
    with its name. 'OnAuto' means that the function will be replaced only
@@ -45,25 +53,14 @@ end
 module BuiltinsOverride = State_builder.Set_ref (Kernel_function.Set) (Info)
 
 let register_builtin name ?replace ?typ f =
+  Value_parameters.register_builtin name;
   Hashtbl.replace table name (f, typ, None, Always);
   match replace with
   | None -> ()
   | Some fname -> Hashtbl.replace table fname (f, typ, Some name, OnAuto)
 
-let () = Db.Value.register_builtin := register_builtin
-
 (* The functions in _builtin must only return the 'Always' builtins *)
 
-let registered_builtins () =
-  let l =
-    Hashtbl.fold
-      (fun name (f, _, _, u) acc -> if u = Always then (name, f) :: acc else acc)
-      table []
-  in
-  List.sort (fun (name1, _) (name2, _) -> String.compare name1 name2) l
-
-let () = Db.Value.registered_builtins := registered_builtins
-
 let builtin_names_and_replacements () =
   let stand_alone, replacements =
     Hashtbl.fold (fun name (_, _, replaced_by, _) (acc1, acc2) ->
@@ -104,14 +101,6 @@ let () =
          raise Cmdline.Exit
        end)
 
-let mem_builtin name =
-  try
-    let _, _, _, u = Hashtbl.find table name in
-    u = Always
-  with Not_found -> false
-
-let () = Db.Value.mem_builtin := mem_builtin
-
 (* Returns the specification of a builtin, used to evaluate preconditions
    and to transfer the states of other domains. *)
 let find_builtin_specification kf =
@@ -229,7 +218,6 @@ let clobbered_set_from_ret state ret =
 
 type call = (Precise_locs.precise_location, Cvalue.V.t) Eval.call
 type result = Cvalue.Model.t * Locals_scoping.clobbered_set
-type builtin = Db.Value.builtin
 
 open Eval
 
@@ -257,7 +245,7 @@ let compute_builtin name builtin state actuals =
       "Invalid number of arguments for builtin %s: %d expected, %d found"
       name n (List.length actuals);
     raise Db.Value.Aborted
-  | Db.Value.Outside_builtin_possibilities ->
+  | Outside_builtin_possibilities ->
     Value_parameters.warning ~once:true ~current:true
       "Call to builtin %s failed, aborting." name;
     raise Db.Value.Aborted
diff --git a/src/plugins/value/domains/cvalue/builtins.mli b/src/plugins/value/domains/cvalue/builtins.mli
index cc4241afa041e9ccdfff55956c648f07f0e26c56..0a84df5cd32691fb6a555b2a1c317b6a4606bbd9 100644
--- a/src/plugins/value/domains/cvalue/builtins.mli
+++ b/src/plugins/value/domains/cvalue/builtins.mli
@@ -24,6 +24,14 @@
     equivalent in C *)
 
 exception Invalid_nb_of_args of int
+exception Outside_builtin_possibilities
+
+type builtin_type = unit -> Cil_types.typ * Cil_types.typ list
+
+type builtin =
+  Cvalue.Model.t ->
+  (Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->
+  Value_types.call_result
 
 (** [register_builtin name ?replace ?typ f] registers the ocaml function [f]
     as a builtin to be used instead of the C function of name [name].
@@ -33,7 +41,7 @@ exception Invalid_nb_of_args of int
     the C function is checked before using the builtin. *)
 val register_builtin:
   string -> ?replace:string ->
-  ?typ:Db.Value.builtin_type -> Db.Value.builtin -> unit
+  ?typ:builtin_type -> builtin -> unit
 
 (** Prepares the builtins to be used for an analysis. Must be called at the
     beginning of each Eva analysis. Warns about builtins of incompatible types,
@@ -46,7 +54,6 @@ val prepare_builtins: unit -> unit
     of [ret] whose contents may contain local variables. *)
 val clobbered_set_from_ret: Cvalue.Model.t -> Cvalue.V.t -> Base.SetLattice.t
 
-type builtin
 type call = (Precise_locs.precise_location, Cvalue.V.t) Eval.call
 type result = Cvalue.Model.t * Locals_scoping.clobbered_set
 
diff --git a/src/plugins/value/domains/cvalue/builtins_split.ml b/src/plugins/value/domains/cvalue/builtins_split.ml
index 9c9d6c0cc1d8a48e5e182c7f6a7f52b82f2fb621..57da04a6ea298c8d9f7b723ae37ed9abc5441169 100644
--- a/src/plugins/value/domains/cvalue/builtins_split.ml
+++ b/src/plugins/value/domains/cvalue/builtins_split.ml
@@ -46,7 +46,7 @@ let frama_c_cardinal state actuals =
     Kernel.abort ~current:true "Incorrect argument for Frama_C_cardinal"
 
 let () =
-  !Db.Value.register_builtin "Frama_C_abstract_cardinal" frama_c_cardinal
+  Builtins.register_builtin "Frama_C_abstract_cardinal" frama_c_cardinal
 
 (** Minimum or maximum of an integer abstract value, Top_int otherwise.
     Also not monotonic. *)
@@ -70,8 +70,8 @@ let frama_c_min_max f state actuals =
     Kernel.abort ~current:true "Incorrect argument for Frama_C_min/max"
 
 let () =
-  !Db.Value.register_builtin "Frama_C_abstract_min" (frama_c_min_max fst);
-  !Db.Value.register_builtin "Frama_C_abstract_max" (frama_c_min_max snd);
+  Builtins.register_builtin "Frama_C_abstract_min" (frama_c_min_max fst);
+  Builtins.register_builtin "Frama_C_abstract_max" (frama_c_min_max snd);
 ;;
 
 (** Splitting values *)
@@ -222,8 +222,8 @@ let aux_split f state actuals =
     }
 
 let () =
-  !Db.Value.register_builtin "Frama_C_builtin_split" (aux_split split_v)
+  Builtins.register_builtin "Frama_C_builtin_split" (aux_split split_v)
 let () =
-  !Db.Value.register_builtin "Frama_C_builtin_split_pointer" (aux_split split_pointer)
+  Builtins.register_builtin "Frama_C_builtin_split_pointer" (aux_split split_pointer)
 let () =
-  !Db.Value.register_builtin "Frama_C_builtin_split_all" (aux_split split_all)
+  Builtins.register_builtin "Frama_C_builtin_split_all" (aux_split split_all)
diff --git a/src/plugins/value/domains/cvalue/builtins_watchpoint.ml b/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
index 4fede94153ea77aa6b983329bda6e16fa1657f5f..d9437db43ada64475246d1141d78da3715043b33 100644
--- a/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
+++ b/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
@@ -55,14 +55,14 @@ let add_watch make_watch state actuals =
         let size = Cvalue.V.project_ival size in
         Int.mul Int.eight (Ival.project_int size)
       with V.Not_based_on_null | Ival.Not_Singleton_Int ->
-        raise Db.Value.Outside_builtin_possibilities
+        raise Builtins.Outside_builtin_possibilities
     in
     let number =
       try
         let number = Cvalue.V.project_ival number in
         Ival.project_int number
       with V.Not_based_on_null | Ival.Not_Singleton_Int ->
-        raise Db.Value.Outside_builtin_possibilities
+        raise Builtins.Outside_builtin_possibilities
     in
     let loc_bits = Locations.loc_bytes_to_loc_bits dst in
     let loc = Locations.make_loc loc_bits (Int_Base.inject size) in
@@ -90,7 +90,7 @@ let make_watch_cardinal target_value =
     Cardinal (Integer.to_int (Ival.project_int target_value))
   with V.Not_based_on_null | Ival.Not_Singleton_Int
      | Z.Overflow (* from Integer.to_int *) ->
-    raise Db.Value.Outside_builtin_possibilities
+    raise Builtins.Outside_builtin_possibilities
 
 let () =
   Builtins.register_builtin "Frama_C_watch_value" (add_watch make_watch_value)
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 122835c78c2f664423edae6235400c83c89f93d9..92c00c5a46efcef6e79241e5bba2c5cdb62afbf4 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -885,6 +885,10 @@ let () = add_precision_dep ILevel.parameter
 let () = ILevel.add_update_hook (fun _ i -> Int_set.set_small_cardinal i)
 let () = ILevel.set_range 4 256
 
+let builtins = ref Datatype.String.Set.empty
+let register_builtin name = builtins := Datatype.String.Set.add name !builtins
+let mem_builtin name = Datatype.String.Set.mem name !builtins
+
 let () = Parameter_customize.set_group precision_tuning
 let () = Parameter_customize.argument_may_be_fundecl ()
 module BuiltinsOverrides =
@@ -895,12 +899,12 @@ module BuiltinsOverrides =
       let of_string ~key:kf ~prev:_ nameopt =
         begin match nameopt with
           | Some name ->
-            if not (!Db.Value.mem_builtin name) then
+            if not (mem_builtin name) then
               abort "option '-eva-builtin %a:%s': undeclared builtin '%s'@.\
                      declared builtins: @[%a@]"
                 Kernel_function.pretty kf name name
                 (Pretty_utils.pp_list ~sep:",@ " Format.pp_print_string)
-                (List.map fst (!Db.Value.registered_builtins ()))
+                (Datatype.String.Set.elements !builtins)
           | _ -> abort
                    "option '-eva-builtin':@ \
                     no builtin associated to function '%a',@ use '%a:<builtin>'"
@@ -921,7 +925,7 @@ let () = add_correctness_dep BuiltinsOverrides.parameter
 
 (* Exported in Eva.mli. *)
 let use_builtin key name =
-  if !Db.Value.mem_builtin name
+  if mem_builtin name
   then BuiltinsOverrides.add (key, Some name)
   else raise Not_found
 
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 23816c0c964ecdba0fa6d034e11a0410bdbee094..3093b5189391b71e3186b13d35f5a32d2fe1eee6 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -218,6 +218,9 @@ val dkey_callbacks : category
 (** Debug category used to print the usage of widenings. *)
 val dkey_widening : category
 
+(** Registers available cvalue builtins for the -eva-builtin option. *)
+val register_builtin: string -> unit
+
 (** Registers available domain names for the -eva-domains option. *)
 val register_domain: name:string -> descr:string -> unit