From 17ec525b96538d6eb9b0a56e93b9fe2b6773f5bd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Wed, 2 Aug 2023 15:00:05 +0200 Subject: [PATCH] [Eva] Removes now unused function [no_results] from deprecated Db.Value. --- src/kernel_services/plugin_entry_points/db.ml | 2 -- src/kernel_services/plugin_entry_points/db.mli | 7 ------- src/plugins/eva/engine/function_calls.ml | 4 ---- 3 files changed, 13 deletions(-) diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml index 6a32a3c734d..7d2158054e0 100644 --- a/src/kernel_services/plugin_entry_points/db.ml +++ b/src/kernel_services/plugin_entry_points/db.ml @@ -263,8 +263,6 @@ module Value = struct ((i land mask_then) <> 0, (i land mask_else) <> 0) with Not_found -> false, false - let no_results = mk_fun "Value.no_results" - let compute = mk_fun "Value.compute" end diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli index ca8f224ed55..8228f31cab7 100644 --- a/src/kernel_services/plugin_entry_points/db.mli +++ b/src/kernel_services/plugin_entry_points/db.mli @@ -175,13 +175,6 @@ module Value : sig computed by the value analysis *) val globals_use_supplied_state : unit -> bool - val no_results: (fundec -> bool) ref - (** Returns [true] if the user has requested that no results should - be recorded for this function. If possible, hooks registered - on [Record_Value_Callbacks] and [Record_Value_Callbacks_New] - should not force their lazy argument *) - - (**/**) (** {3 Internal use only} *) diff --git a/src/plugins/eva/engine/function_calls.ml b/src/plugins/eva/engine/function_calls.ml index 9a0a589a1e3..bbc61c05b02 100644 --- a/src/plugins/eva/engine/function_calls.ml +++ b/src/plugins/eva/engine/function_calls.ml @@ -26,10 +26,6 @@ open Eval let save_results f = Parameters.ResultsAll.get () && not (Parameters.NoResultsFunctions.mem f) -let () = - Db.Value.no_results := - (fun fd -> not (save_results fd) || not (Parameters.Domains.mem "cvalue")) - (* Signal that some results are not stored. The gui or some API calls may fail ungracefully. *) let partial_results () = -- GitLab