diff --git a/src/plugins/value/engine/evaluation.ml b/src/plugins/value/engine/evaluation.ml index aaef33f5418aaa61710b7e891c1916d054a622cb..10974ea5bb1026d3f8f8089856549ec0eaf13ca4 100644 --- a/src/plugins/value/engine/evaluation.ml +++ b/src/plugins/value/engine/evaluation.ml @@ -1623,7 +1623,7 @@ module Make Self.abort ~current:true "Calls through function pointers are not supported without the cvalue \ domain."; - if Mark_noresults.no_memoization_enabled () then + if Function_calls.partial_results () then Self.abort ~current:true "Function pointer evaluates to anything. Try deactivating \ option(s) -eva-no-results and -eva-no-results-function." diff --git a/src/plugins/value/engine/function_calls.ml b/src/plugins/value/engine/function_calls.ml index 7c368ffcbae75ebe3692dc56160438b35fbe1548..f4e68e27934f1498b7287b9f616e3ef08dc3db96 100644 --- a/src/plugins/value/engine/function_calls.ml +++ b/src/plugins/value/engine/function_calls.ml @@ -26,6 +26,12 @@ open Eval let save_results f = Parameters.ResultsAll.get () && not (Parameters.NoResultsFunctions.mem f) +(* Signal that some results are not stored. The gui or some API calls + may fail ungracefully. *) +let partial_results () = + not (Parameters.ResultsAll.get ()) || + not (Parameters.NoResultsFunctions.is_empty ()) + let info name : (module State_builder.Info_with_size) = (module struct diff --git a/src/plugins/value/engine/function_calls.mli b/src/plugins/value/engine/function_calls.mli index c7efe940d8855a9e75c262d02d27a52fcf2f103e..f5fa13a02dc30d3a60c27a5077eee353da743ce3 100644 --- a/src/plugins/value/engine/function_calls.mli +++ b/src/plugins/value/engine/function_calls.mli @@ -25,6 +25,10 @@ open Cil_types (** True if the results should be saved for the given function. *) val save_results: fundec -> bool +(** True if some results are not stored due to options -eva-no-results + or -eva-no-results-function. *) +val partial_results: unit -> bool + (** What is used for the analysis of a given function: - a Cvalue builtin (and other domains use the specification) - the function specification diff --git a/src/plugins/value/gui_files/register_gui.ml b/src/plugins/value/gui_files/register_gui.ml index fda18017f390f47ab0a3da7bd9929391f795de2a..1b1e29838b3e3fded78fadfd3b8e77b969acba45 100644 --- a/src/plugins/value/gui_files/register_gui.ml +++ b/src/plugins/value/gui_files/register_gui.ml @@ -43,7 +43,7 @@ module UsedVarState = let used_var = UsedVarState.memo (fun var -> - Mark_noresults.no_memoization_enabled () || + Function_calls.partial_results () || try let f = fst (Globals.entry_point ()) in let inputs = !Db.Inputs.get_external f in diff --git a/src/plugins/value/utils/mark_noresults.ml b/src/plugins/value/utils/mark_noresults.ml index f679f39b8bad2d0148e1771357d6cb1e508bd16d..62993f4ad6c265b12d7b7112b0c66e5d23f9cae8 100644 --- a/src/plugins/value/utils/mark_noresults.ml +++ b/src/plugins/value/utils/mark_noresults.ml @@ -29,13 +29,6 @@ let () = Db.Value.no_results := (fun fd -> not (should_memorize_function fd) || not (Parameters.Domains.mem "cvalue")) -(* Signal that some results are not stored. The gui, or some calls to - Db.Value, may fail ungracefully *) -let no_memoization_enabled () = - not (Parameters.ResultsAll.get ()) || - not (Parameters.NoResultsFunctions.is_empty ()) - - (* Local Variables: diff --git a/src/plugins/value/utils/mark_noresults.mli b/src/plugins/value/utils/mark_noresults.mli index 2710d864476daa6534727114716eb87ca7434ea4..90ce19fac0aa3e9d74b1b93322aa1c200e906908 100644 --- a/src/plugins/value/utils/mark_noresults.mli +++ b/src/plugins/value/utils/mark_noresults.mli @@ -22,6 +22,3 @@ (** Are the states of the function analysis saved? *) val should_memorize_function: Cil_types.fundec -> bool - -(** Signal that some analysis results are not stored. *) -val no_memoization_enabled: unit -> bool