diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli index 27f069ce7ee7902b858971a397596890cb19b400..a2f023223cc64c64b7beed58512b9a5a7f020415 100644 --- a/src/plugins/value/Eva.mli +++ b/src/plugins/value/Eva.mli @@ -35,6 +35,10 @@ 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 b] adds a builtin override for function [kf] to + builtin {!b}. *) + 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..cbbdd4865a7c0f7c17afb4e840b020fd295a7074 100644 --- a/src/plugins/value/value_parameters.ml +++ b/src/plugins/value/value_parameters.ml @@ -941,6 +941,8 @@ 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) let () = Parameter_customize.set_group precision_tuning module BuiltinsAuto = 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 ../../.."