diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml index ff9852652b41d923f1cc0b266f08c38057601301..636bb2b290a258405f0210561cdf8fb01b4ed4c4 100644 --- a/src/kernel_services/plugin_entry_points/db.ml +++ b/src/kernel_services/plugin_entry_points/db.ml @@ -511,9 +511,6 @@ module Value = struct | Kglobal -> Cvalue.Model.is_reachable (globals_state ()) | Kstmt stmt -> is_reachable_stmt stmt - let is_called = mk_fun "Value.is_called" - let callers = mk_fun "Value.callers" - let eval_lval = ref (fun ?with_alarms:_ _ -> mk_labeled_fun "Value.eval_lval") let eval_expr = diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli index b87bf1fbf98c8298424d17e417e924eb77047074..2ef31cad628367c4c7c63c484df7929f52ebac0c 100644 --- a/src/kernel_services/plugin_entry_points/db.mli +++ b/src/kernel_services/plugin_entry_points/db.mli @@ -254,15 +254,6 @@ module Value : sig val is_reachable_stmt : stmt -> bool - (** {3 About kernel functions} *) - - val is_called: (kernel_function -> bool) ref - - val callers: (kernel_function -> (kernel_function*stmt list) list) ref - (** @return the list of callers with their call sites. Each function is - present only once in the list. *) - - (** {3 Locations of left values} *) val lval_to_loc : diff --git a/src/plugins/eva/register.ml b/src/plugins/eva/register.ml index 4bc58fcd1ff401fff40b6e3f4bbd442b1ef5dbd0..7fd5081fe77c76679b400b083619f092d505611e 100644 --- a/src/plugins/eva/register.ml +++ b/src/plugins/eva/register.ml @@ -33,15 +33,9 @@ let main () = let () = Db.Main.extend main - -let () = - Db.Value.is_called := Function_calls.is_called; - Db.Value.callers := Function_calls.callsites; - - - (* -------------------------------------------------------------------------- *) - (* Register Evaluation Functions *) - (* -------------------------------------------------------------------------- *) +(* -------------------------------------------------------------------------- *) +(* Register Evaluation Functions *) +(* -------------------------------------------------------------------------- *) open Eval diff --git a/src/plugins/eva/utils/eva_dynamic.ml b/src/plugins/eva/utils/eva_dynamic.ml index ebfdc9384ad7969a7b94b12b290d03c92ccc47f0..c623675e2d22d95923eb4b3a9817f0c91cd2a8ec 100644 --- a/src/plugins/eva/utils/eva_dynamic.ml +++ b/src/plugins/eva/utils/eva_dynamic.ml @@ -62,5 +62,6 @@ module RteGen = struct let mark_generated_rte () = let list = all_statuses () in let mark kf = List.iter (fun (_kind, set, _get) -> set kf true) list in - Globals.Functions.iter (fun kf -> if !Db.Value.is_called kf then mark kf) + Globals.Functions.iter + (fun kf -> if Function_calls.is_called kf then mark kf) end