diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml index 80f4b5bf37b87afa44d1429bb27433cfa1622105..365cbf36d5e5dfec6b09b31ed1089312760095f4 100644 --- a/src/kernel_services/plugin_entry_points/db.ml +++ b/src/kernel_services/plugin_entry_points/db.ml @@ -20,21 +20,8 @@ (* *) (**************************************************************************) -open Cil_types open Extlib -let register r f = r := f - -let register_compute name deps r f = - let name = "!Db." ^ name in - let compute, self = State_builder.apply_once name deps f in - r := compute; - self - -let register_guarded_compute is_computed r f = - let compute () = if not (is_computed ()) then f () in - r := compute - module Main = struct include Hook.Make() let play = mk_fun "Main.play" diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli index fd6fbf6f4d07f03fe8b6eb672aa3c83b45d106ab..e7d04befcc2991a6b84725468d1f43cd09b83286 100644 --- a/src/kernel_services/plugin_entry_points/db.mli +++ b/src/kernel_services/plugin_entry_points/db.mli @@ -45,26 +45,6 @@ line) *) -open Cil_types - -(* ************************************************************************* *) -(** {2 Registering} *) -(* ************************************************************************* *) - -val register: 'a ref -> 'a -> unit -(** Plugins must register values with this function. *) - -val register_compute: - string -> - State.t list -> - (unit -> unit) ref -> (unit -> unit) -> State.t - -val register_guarded_compute: - (unit -> bool) -> - (unit -> unit) ref -> (unit -> unit) -> unit -(** @before 26.0-Iron there was a string parameter (first position) that was - only used for Journalization, that has been removed. *) - (** Frama-C main interface. @since Lithium-20081201 @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)