diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index 27f069ce7ee7902b858971a397596890cb19b400..4de6198ed1a43b3c1d4a9c2d0a344b378eee5dc6 100644
--- a/src/plugins/value/Eva.mli
+++ b/src/plugins/value/Eva.mli
@@ -35,6 +35,11 @@ end
 module Value_parameters: sig
   (** Returns the list (name, descr) of currently enabled abstract domains. *)
   val enabled_domains: unit -> (string * string) list
+
+  (** [use_builtin kf name] instructs the analysis to use the builtin [name]
+      to interpret calls to function [kf].
+      Raises [Not_found] if there is no builtin of name [name]. *)
+  val use_builtin: Cil_types.kernel_function -> string -> unit
 end
 
 module Eval_terms: sig
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 82e05def8e6ce595ed5383d0d079061118c936aa..cd4ef32136c15f52f83a89a6089bee1d4f98f126 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -918,13 +918,13 @@ module BuiltinsOverrides =
         begin match nameopt with
           | Some name ->
             if not (!Db.Value.mem_builtin name) then
-              abort "option '-val-builtin %a:%s': undeclared builtin '%s'@.\
+              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 ()))
           | _ -> abort
-                   "option '-val-builtin':@ \
+                   "option '-eva-builtin':@ \
                     no builtin associated to function '%a',@ use '%a:<builtin>'"
                    Kernel_function.pretty kf Kernel_function.pretty kf
         end;
@@ -942,6 +942,12 @@ module BuiltinsOverrides =
 let () = add_precision_dep BuiltinsOverrides.parameter
 let () = BuiltinsOverrides.add_aliases ["-val-builtin"]
 
+(* Exported in Eva.mli. *)
+let use_builtin key name =
+  if !Db.Value.mem_builtin name
+  then BuiltinsOverrides.add (key, Some name)
+  else raise Not_found
+
 let () = Parameter_customize.set_group precision_tuning
 module BuiltinsAuto =
   True
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 8375ac554c748bc7f4a861ea546502704e168937..495d7b1fa9a873b7736c2651944fe2a0f9843cf3 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -236,6 +236,10 @@ val register_domain: name:string -> descr:string -> unit
 (** Returns the list (name, descr) of currently enabled domains. *)
 val enabled_domains: unit -> (string * string) list
 
+(** [use_builtin kf b] adds a builtin override for function `kf` to
+    builtin `b`. *)
+val use_builtin: Cil_types.kernel_function -> string -> unit
+
 (*
 Local Variables:
 compile-command: "make -C ../../.."