From 03888af3a71fe4dc2cadc50eda1186c04c9027d0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Thu, 27 Jul 2023 13:40:05 +0200 Subject: [PATCH] [Eva] Removes functions [is_called] and [callers] from deprecated Db.Value. --- src/kernel_services/plugin_entry_points/db.ml | 3 --- src/kernel_services/plugin_entry_points/db.mli | 9 --------- src/plugins/eva/register.ml | 12 +++--------- src/plugins/eva/utils/eva_dynamic.ml | 3 ++- 4 files changed, 5 insertions(+), 22 deletions(-) diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml index ff9852652b4..636bb2b290a 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 b87bf1fbf98..2ef31cad628 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 4bc58fcd1ff..7fd5081fe77 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 ebfdc9384ad..c623675e2d2 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 -- GitLab