diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli index a2f023223cc64c64b7beed58512b9a5a7f020415..4de6198ed1a43b3c1d4a9c2d0a344b378eee5dc6 100644 --- a/src/plugins/value/Eva.mli +++ b/src/plugins/value/Eva.mli @@ -36,8 +36,9 @@ module Value_parameters: sig (** Returns the list (name, descr) of currently enabled abstract domains. *) val enabled_domains: unit -> (string * string) list - (** [use_builtin kf b] adds a builtin override for function [kf] to - builtin {!b}. *) + (** [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 diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml index cbbdd4865a7c0f7c17afb4e840b020fd295a7074..5d65b1fc3ead5c34499f2110007d339da7bdc13e 100644 --- a/src/plugins/value/value_parameters.ml +++ b/src/plugins/value/value_parameters.ml @@ -941,8 +941,12 @@ module BuiltinsOverrides = end) let () = add_precision_dep BuiltinsOverrides.parameter let () = BuiltinsOverrides.add_aliases ["-val-builtin"] -let use_builtin key value = - BuiltinsOverrides.add (key, Some value) + +(* 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 =