diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml index 6a32a3c734ddb06acaa93935d3bdc31c4f660342..7d2158054e05a56b04550aa05e91a8682c092de4 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 ca8f224ed55a4c9137428e20a80de92b26ebbd20..8228f31cab7a7468b810d570725e34d139f82560 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 9a0a589a1e372b5742c068f56c21ed2d6c7402ae..bbc61c05b0217eed796622029e61d10e6f2f6b1b 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 () =