diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml
index 9b43b96fa2f12d3164b21b7c8e7a80b10182d0a8..eb872274dc205c8a459f01c9d4ec45714bce6b76 100644
--- a/src/plugins/value/engine/analysis.ml
+++ b/src/plugins/value/engine/analysis.ml
@@ -28,6 +28,15 @@ type computation_state = Self.computation_state =
let current_computation_state = Self.current_computation_state
let register_computation_hook = Self.register_computation_hook
let is_computed = Self.is_computed
+let self = Self.state
+
+type results = Function_calls.results = Complete | Partial | NoResults
+type status = Function_calls.analysis_status =
+ Unreachable | SpecUsed | Builtin of string | Analyzed of results
+let status = Function_calls.analysis_status
+
+let use_spec_instead_of_definition =
+ Function_calls.use_spec_instead_of_definition ?recursion_depth:None
let save_results kf =
try Function_calls.save_results (Kernel_function.get_definition kf)
@@ -38,13 +47,13 @@ module type Results = sig
type value
type location
- val get_global_state: unit -> state or_bottom
- val get_stmt_state : after:bool -> stmt -> state or_bottom
+ val get_global_state: unit -> state or_top_bottom
+ val get_stmt_state : after:bool -> stmt -> state or_top_bottom
val get_stmt_state_by_callstack:
?selection:callstack list ->
after:bool -> stmt -> state Value_types.Callstack.Hashtbl.t or_top_bottom
val get_initial_state:
- kernel_function -> state or_bottom
+ kernel_function -> state or_top_bottom
val get_initial_state_by_callstack:
?selection:callstack list ->
kernel_function -> state Value_types.Callstack.Hashtbl.t or_top_bottom
@@ -82,22 +91,31 @@ module Make (Abstract: Abstractions.S) = struct
include Abstract
include Compute_functions.Make (Abstract)
+ let find stmt f =
+ let kf = Kernel_function.find_englobing_kf stmt in
+ match status kf with
+ | Unreachable -> `Bottom
+ | Analyzed NoResults | SpecUsed | Builtin _ -> `Top
+ | Analyzed (Complete | Partial) -> f stmt
+
let get_stmt_state ~after stmt =
- let fundec = Kernel_function.(get_definition (find_englobing_kf stmt)) in
- if Mark_noresults.should_memorize_function fundec && is_computed ()
- then Abstract.Dom.Store.get_stmt_state ~after stmt
- else `Value Abstract.Dom.top
+ find stmt (Dom.Store.get_stmt_state ~after :> stmt -> Dom.t or_top_bottom)
- let get_global_state = Abstract.Dom.Store.get_global_state
+ let get_stmt_state_by_callstack ?selection ~after stmt =
+ find stmt (Abstract.Dom.Store.get_stmt_state_by_callstack ?selection ~after)
- let get_stmt_state_by_callstack =
- Abstract.Dom.Store.get_stmt_state_by_callstack
+ let get_global_state () =
+ (Abstract.Dom.Store.get_global_state () :> Dom.t or_top_bottom)
- let get_initial_state =
- Abstract.Dom.Store.get_initial_state
+ let get_initial_state kf =
+ if Function_calls.is_called kf
+ then (Abstract.Dom.Store.get_initial_state kf :> Dom.t or_top_bottom)
+ else `Bottom
- let get_initial_state_by_callstack =
- Abstract.Dom.Store.get_initial_state_by_callstack
+ let get_initial_state_by_callstack ?selection kf =
+ if Function_calls.is_called kf
+ then Abstract.Dom.Store.get_initial_state_by_callstack ?selection kf
+ else `Bottom
let eval_expr state expr = Eval.evaluate state expr >>=: snd
@@ -205,13 +223,3 @@ let () =
Project.register_after_set_current_hook
~user_only:true (fun _ -> reset_analyzer ());
Project.register_after_global_load_hook reset_analyzer
-
-let self = Self.state
-
-type results = Function_calls.results = Complete | Partial | NoResults
-type status = Function_calls.analysis_status =
- Unreachable | SpecUsed | Builtin of string | Analyzed of results
-let status = Function_calls.analysis_status
-
-let use_spec_instead_of_definition =
- Function_calls.use_spec_instead_of_definition ?recursion_depth:None
diff --git a/src/plugins/value/engine/analysis.mli b/src/plugins/value/engine/analysis.mli
index 98c2201b905cd1ea8911de7f2448766be0f3d384..bfaa372cc3a3d10a39654f9e43ba479ed873b12a 100644
--- a/src/plugins/value/engine/analysis.mli
+++ b/src/plugins/value/engine/analysis.mli
@@ -28,13 +28,13 @@ module type Results = sig
type value
type location
- val get_global_state: unit -> state or_bottom
- val get_stmt_state : after:bool -> stmt -> state or_bottom
+ val get_global_state: unit -> state or_top_bottom
+ val get_stmt_state : after:bool -> stmt -> state or_top_bottom
val get_stmt_state_by_callstack:
?selection:callstack list ->
after:bool -> stmt -> state Value_types.Callstack.Hashtbl.t or_top_bottom
val get_initial_state:
- kernel_function -> state or_bottom
+ kernel_function -> state or_top_bottom
val get_initial_state_by_callstack:
?selection:callstack list ->
kernel_function -> state Value_types.Callstack.Hashtbl.t or_top_bottom
diff --git a/src/plugins/value/gui_files/register_gui.ml b/src/plugins/value/gui_files/register_gui.ml
index 1b1e29838b3e3fded78fadfd3b8e77b969acba45..e99b3d3ea0215e14bf2ba44fcb56f4d0d4f53c74 100644
--- a/src/plugins/value/gui_files/register_gui.ml
+++ b/src/plugins/value/gui_files/register_gui.ml
@@ -528,7 +528,7 @@ module Select (Eval: Eval) = struct
| Kstmt stmt -> Eval.Analysis.get_stmt_state ~after:false stmt
in
match state with
- | `Bottom -> ()
+ | `Bottom | `Top -> ()
| `Value state ->
let funs, _ = Eval.Analysis.eval_function_exp state e in
match funs with
diff --git a/src/plugins/value/utils/results.ml b/src/plugins/value/utils/results.ml
index ca379c399f9185e5ba52b8673df08cc6ee6e01b3..dc59df6779d18c1270e8eecdabdf831f3118a79c 100644
--- a/src/plugins/value/utils/results.ml
+++ b/src/plugins/value/utils/results.ml
@@ -110,11 +110,13 @@ struct
let consolidated =
function
| `Bottom -> Bottom
+ | `Top -> Top
| `Value state -> Consolidated state
let singleton cs =
function
| `Bottom -> Bottom
+ | `Top -> Top
| `Value state -> ByCallstack [cs,state]
let by_callstack : request ->