diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml index a34af07d560e13e353e898563565569f7d91672e..11e429d42db8d613075e2221437624747db08395 100644 --- a/src/plugins/value/engine/analysis.ml +++ b/src/plugins/value/engine/analysis.ml @@ -100,8 +100,8 @@ module Make (Abstract: Abstractions.S) = struct then let kf = Kernel_function.find_englobing_kf stmt in match status kf with - | Unreachable -> `Bottom - | Analyzed NoResults | SpecUsed | Builtin _ -> `Top + | Unreachable | SpecUsed | Builtin _ -> `Bottom + | Analyzed NoResults -> `Top | Analyzed (Complete | Partial) -> f stmt else `Top diff --git a/src/plugins/value/engine/analysis.mli b/src/plugins/value/engine/analysis.mli index c4fb144b74af003e291d8b1ef2e296308c065e90..789e483758683ceca1214b554257bd43c1f5d25e 100644 --- a/src/plugins/value/engine/analysis.mli +++ b/src/plugins/value/engine/analysis.mli @@ -128,11 +128,11 @@ type status = | SpecUsed (** The function specification has been used to interpret its calls: its body has not been analyzed. Any request at a statement of this - function will lead to a Top result. *) + function will lead to a Bottom result. *) | Builtin of string (** The builtin of the given name has been used to interpret the function: its body has not been analyzed. Any request at a statement of this - function will lead to a Top result. *) + function will lead to a Bottom result. *) | Analyzed of results (** The function body has been analyzed. *) diff --git a/src/plugins/value/gui_files/register_gui.ml b/src/plugins/value/gui_files/register_gui.ml index e99b3d3ea0215e14bf2ba44fcb56f4d0d4f53c74..31d005daf3e195dac525dbafe363ac52e7ba978c 100644 --- a/src/plugins/value/gui_files/register_gui.ml +++ b/src/plugins/value/gui_files/register_gui.ml @@ -172,7 +172,7 @@ let active_highlighter buffer localizable ~start ~stop = | Some color_area -> apply_tag buffer color_area start stop | None -> - if Gui_eval.results_kf_computed kf then begin + if Analysis.status kf <> Analyzed NoResults then begin let csf = Gui_callstacks_filters.focused_callstacks () in if Gui_callstacks_filters.is_reachable_stmt csf stmt then begin if Gui_callstacks_filters.is_non_terminating_instr csf stmt then diff --git a/src/plugins/value/utils/results.mli b/src/plugins/value/utils/results.mli index fac0e191f424ca56564d61be48dfd5406879737b..de423c3260fa3a6da2d8bcf3c7c9cb8fdb911092 100644 --- a/src/plugins/value/utils/results.mli +++ b/src/plugins/value/utils/results.mli @@ -60,7 +60,7 @@ - the function has not been reached by the analysis: all requests in the function will lead to a Bottom error. - a specification or a builtin has been used instead of analyzing the - function body: all requests in the function will lead to a Top error. + function body: all requests in the function will lead to a Bottom error. - results have not been saved, due to the [-eva-no-results] parameter: all requests in the function will lead to a Top error. *) val are_available: Cil_types.kernel_function -> bool