diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 7331c3ef4f4a024edeee2ea731d258cfe6b2cd76..6a32a3c734ddb06acaa93935d3bdc31c4f660342 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -235,49 +235,6 @@ module Value = struct
let self = State_builder.Proxy.get proxy
let only_self = [ self ]
- let size = 256
-
- [@@@ alert "-db_deprecated"]
- type callstack = Eva_types.Callstack.callstack
-
- module States_by_callstack =
- Eva_types.Callstack.Hashtbl.Make(Cvalue.Model)
-
- module Table_By_Callstack =
- Cil_state_builder.Stmt_hashtbl(States_by_callstack)
- (struct
- let name = "Db.Value.Table_By_Callstack"
- let size = size
- let dependencies = [ self ]
- end)
- module Table =
- Cil_state_builder.Stmt_hashtbl(Cvalue.Model)
- (struct
- let name = "Db.Value.Table"
- let size = size
- let dependencies = [ self ]
- end)
-
- module AfterTable_By_Callstack =
- Cil_state_builder.Stmt_hashtbl(States_by_callstack)
- (struct
- let name = "Db.Value.AfterTable_By_Callstack"
- let size = size
- let dependencies = [ self ]
- end)
- module AfterTable =
- Cil_state_builder.Stmt_hashtbl(Cvalue.Model)
- (struct
- let name = "Db.Value.AfterTable"
- let size = size
- let dependencies = [ self ]
- end)
-
- let mark_as_computed () =
- Table_By_Callstack.mark_as_computed ()
-
- let is_computed () = Table_By_Callstack.is_computed ()
-
module Conditions_table =
Cil_state_builder.Stmt_hashtbl
(Datatype.Int)
@@ -306,164 +263,8 @@ module Value = struct
((i land mask_then) <> 0, (i land mask_else) <> 0)
with Not_found -> false, false
- module Called_Functions_By_Callstack =
- State_builder.Hashtbl(Kernel_function.Hashtbl)
- (States_by_callstack)
- (struct
- let name = "Db.Value.Called_Functions_By_Callstack"
- let size = 11
- let dependencies = only_self
- end)
-
- module Called_Functions_Memo =
- State_builder.Hashtbl(Kernel_function.Hashtbl)
- (Cvalue.Model)
- (struct
- let name = "Db.Value.Called_Functions_Memo"
- let size = 11
- let dependencies = [ Called_Functions_By_Callstack.self ]
- end)
-
-(*
- let pretty_table () =
- Table.iter
- (fun k v ->
- Kernel.log ~kind:Log.Debug
- "GLOBAL TABLE at %a: %a@\n"
- Kinstr.pretty k
- Cvalue.Model.pretty v)
-
- let pretty_table_raw () =
- Kinstr.Hashtbl.iter
- (fun k v ->
- Kernel.log ~kind:Log.Debug
- "GLOBAL TABLE at %a: %a@\n"
- Kinstr.pretty k
- Cvalue.Model.pretty v)
-*)
-
let no_results = mk_fun "Value.no_results"
- let update_callstack_table ~after stmt callstack v =
- let open Eva_types in
- let find,add =
- if after
- then AfterTable_By_Callstack.find, AfterTable_By_Callstack.add
- else Table_By_Callstack.find, Table_By_Callstack.add
- in
- try
- let by_callstack = find stmt in
- begin try
- let o = Callstack.Hashtbl.find by_callstack callstack in
- Callstack.Hashtbl.replace by_callstack callstack(Cvalue.Model.join o v)
- with Not_found ->
- Callstack.Hashtbl.add by_callstack callstack v
- end;
- with Not_found ->
- let r = Callstack.Hashtbl.create 7 in
- Callstack.Hashtbl.add r callstack v;
- add stmt r
-
- let merge_initial_state cs kf state =
- let open Eva_types in
- let by_callstack =
- try Called_Functions_By_Callstack.find kf
- with Not_found ->
- let h = Callstack.Hashtbl.create 7 in
- Called_Functions_By_Callstack.add kf h;
- h
- in
- try
- let old = Callstack.Hashtbl.find by_callstack cs in
- Callstack.Hashtbl.replace by_callstack cs (Cvalue.Model.join old state)
- with Not_found ->
- Callstack.Hashtbl.add by_callstack cs state
-
- let get_initial_state kf =
- assert (is_computed ()); (* this assertion fails during Eva analysis *)
- try Called_Functions_Memo.find kf
- with Not_found ->
- let state =
- try
- let open Eva_types in
- let by_callstack = Called_Functions_By_Callstack.find kf in
- Callstack.Hashtbl.fold
- (fun _cs state acc -> Cvalue.Model.join acc state)
- by_callstack Cvalue.Model.bottom
- with Not_found -> Cvalue.Model.bottom
- in
- Called_Functions_Memo.add kf state;
- state
-
- (* This function is used by the Inout plugin during Eva analysis, so it
- should not fail during Eva analysis, even if results are incomplete. *)
- let get_initial_state_callstack kf =
- try Some (Called_Functions_By_Callstack.find kf)
- with Not_found -> None
-
- let get_fundec_from_stmt stmt =
- let kf =
- try
- Kernel_function.find_englobing_kf stmt
- with Not_found ->
- Kernel.fatal "Unknown statement '%a'" Printer.pp_stmt stmt
- in
- try
- Kernel_function.get_definition kf
- with Kernel_function.No_Definition ->
- Kernel.fatal "No definition for function %a" Kernel_function.pretty kf
-
- let noassert_get_stmt_state ~after s =
- if !no_results (get_fundec_from_stmt s)
- then Cvalue.Model.top
- else
- let (find, add), find_by_callstack =
- if after
- then AfterTable.(find, add), AfterTable_By_Callstack.find
- else Table.(find, add), Table_By_Callstack.find
- in
- try find s
- with Not_found ->
- let ho = try Some (find_by_callstack s) with Not_found -> None in
- let state =
- match ho with
- | None -> Cvalue.Model.bottom
- | Some h ->
- Eva_types.Callstack.Hashtbl.fold (fun _cs state acc ->
- Cvalue.Model.join acc state
- ) h Cvalue.Model.bottom
- in
- add s state;
- state
-
- let get_stmt_state ?(after=false) s =
- assert (is_computed ()); (* this assertion fails during Eva analysis *)
- noassert_get_stmt_state ~after s
-
- let get_stmt_state_callstack ~after stmt =
- assert (is_computed ()); (* this assertion fails during Eva analysis *)
- try
- Some (if after then AfterTable_By_Callstack.find stmt else
- Table_By_Callstack.find stmt)
- with Not_found -> None
-
- exception Is_reachable
- let is_reachable_stmt stmt =
- if !no_results (get_fundec_from_stmt stmt)
- then true
- else
- let ho = try Some (Table_By_Callstack.find stmt) with Not_found -> None in
- match ho with
- | None -> false
- | Some h ->
- try
- Eva_types.Callstack.Hashtbl.iter
- (fun _cs state ->
- if Cvalue.Model.is_reachable state
- then raise Is_reachable) h;
- false
- with Is_reachable -> true
-
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 916ae36b4328776750f5f72cf7b72325ac7daf0d..ca8f224ed55a4c9137428e20a80de92b26ebbd20 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -115,9 +115,6 @@ module Value : sig
(** Internal state of the value analysis from projects viewpoint.
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
- val mark_as_computed: unit -> unit
- (** Indicate that the value analysis has been done already. *)
-
val compute : (unit -> unit) ref
(** Compute the value analysis using the entry point of the current
project. You may set it with {!Globals.set_entry_point}.
@@ -127,27 +124,6 @@ module Value : sig
an incorrect number of them is given.
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
- val is_computed: unit -> bool
- (** Return [true] iff the value analysis has been done.
- @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
-
- [@@@alert "-db_deprecated"]
-
- type callstack = Eva_types.Callstack.callstack
-
- module Table_By_Callstack:
- State_builder.Hashtbl with type key = stmt
- and type data = state Eva_types.Callstack.Hashtbl.t
- (** Table containing the results of the value analysis, ie.
- the state before the evaluation of each reachable statement. *)
-
- module AfterTable_By_Callstack:
- State_builder.Hashtbl with type key = stmt
- and type data = state Eva_types.Callstack.Hashtbl.t
- (** Table containing the state of the value analysis after the evaluation
- of each reachable and evaluable statement. Filled only if
- [Value_parameters.ResultsAfter] is set. *)
-
val condition_truth_value: stmt -> bool * bool
(** Provided [stmt] is an 'if' construct, [fst (condition_truth_value stmt)]
(resp. snd) is true if and only if the condition of the 'if' has been
@@ -199,26 +175,6 @@ module Value : sig
computed by the value analysis *)
val globals_use_supplied_state : unit -> bool
-
- (** {3 Getters} *)
- (** State of the analysis at various points *)
-
- val get_initial_state : kernel_function -> state
- val get_initial_state_callstack :
- kernel_function -> state Eva_types.Callstack.Hashtbl.t option
-
- val get_stmt_state_callstack:
- after:bool -> stmt -> state Eva_types.Callstack.Hashtbl.t option
-
- val get_stmt_state : ?after:bool -> stmt -> state
- (** [after] is false by default.
- @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
-
- (** {3 Reachability} *)
-
- val is_reachable_stmt : stmt -> 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
@@ -235,13 +191,6 @@ module Value : sig
val initial_state_only_globals : (unit -> state) ref
- val update_callstack_table: after:bool -> stmt -> callstack -> state -> unit
- (* Merge a new state in the table indexed by callstacks. *)
-
- val merge_initial_state : callstack -> kernel_function -> state -> unit
- (** Store an additional possible initial state for the given callstack as
- well as its values for actuals. *)
-
val initial_state_changed: (unit -> unit) ref
end
[@@alert db_deprecated
diff --git a/src/plugins/eva/domains/cvalue/cvalue_domain.ml b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
index c6f8db8b6f69c634ccfd265263e9bd025c290884..25010f6622a3f4115a873216ee42f7b95ebfe4e4 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
@@ -322,26 +322,15 @@ module State = struct
(* ------------------------------------------------------------------------ *)
module Store = struct
- module Storage =
- State_builder.Ref (Datatype.Bool)
- (struct
- let dependencies = [Self.state]
- let name = name ^ ".Storage"
- let default () = false
- end)
-
- let register_global_state b _ = Storage.set b
+
+ let register_global_state b s =
+ Cvalue_results.register_global_state b (Bottom.map fst s)
let register_initial_state callstack kf (state, _clob) =
- Db.Value.merge_initial_state callstack kf state
+ Cvalue_results.register_initial_state callstack kf state
let register_state_before_stmt callstack stmt (state, _clob) =
- Db.Value.update_callstack_table ~after:false stmt callstack state
+ Cvalue_results.register_state_before_stmt callstack stmt state
let register_state_after_stmt callstack stmt (state, _clob) =
- Db.Value.update_callstack_table ~after:true stmt callstack state
-
- let return state =
- if Cvalue.Model.(equal state bottom)
- then `Bottom
- else `Value (state, Locals_scoping.top ())
+ Cvalue_results.register_state_after_stmt callstack stmt state
let lift_tbl tbl =
let h = Callstack.Hashtbl.create 7 in
@@ -363,31 +352,39 @@ module State = struct
List.iter add list;
new_tbl
- let get_global_state () = return (Db.Value.globals_state ())
- let get_initial_state kf = return (Db.Value.get_initial_state kf)
+ let get_global_state () =
+ let+ state = Cvalue_results.get_global_state () in
+ state, Locals_scoping.top ()
+
+ let get_initial_state kf =
+ let+ state = Cvalue_results.get_initial_state kf in
+ state, Locals_scoping.top ()
+
let get_initial_state_by_callstack ?selection kf =
- if Storage.get ()
- then
- match Db.Value.get_initial_state_callstack kf with
- | Some tbl -> `Value (lift_tbl (select ?selection tbl))
- | None -> `Bottom
- else `Top
+ match Cvalue_results.get_initial_state_by_callstack ?selection kf with
+ | `Top -> `Top
+ | `Bottom -> `Bottom
+ | `Value tbl -> `Value (lift_tbl (select ?selection tbl))
let get_stmt_state ~after stmt =
- return (Db.Value.get_stmt_state ~after stmt)
+ let+ state = Cvalue_results.get_stmt_state ~after stmt in
+ state, Locals_scoping.top ()
let get_stmt_state_by_callstack ?selection ~after stmt =
- if Storage.get ()
- then
- match Db.Value.get_stmt_state_callstack ~after stmt with
- | Some tbl -> `Value (lift_tbl (select ?selection tbl))
- | None -> `Bottom
- else `Top
+ match Cvalue_results.get_stmt_state_by_callstack ?selection ~after stmt with
+ | `Top -> `Top
+ | `Bottom -> `Bottom
+ | `Value tbl -> `Value (lift_tbl (select ?selection tbl))
- let mark_as_computed = Db.Value.mark_as_computed
- let is_computed = Db.Value.is_computed
+ let mark_as_computed = Cvalue_results.mark_as_computed
+ let is_computed = Cvalue_results.is_computed
end
+ let get_state_before stmt =
+ match Cvalue_results.get_stmt_state ~after:false stmt with
+ | `Bottom -> Cvalue.Model.bottom
+ | `Value v -> v
+
let display ?fmt kf =
let open Cil_types in
(* Do not pretty Cil-generated variables or out-of-scope local variables *)
@@ -403,10 +400,8 @@ module State = struct
| _ -> true
in
try
- let values = Db.Value.get_stmt_state (Kernel_function.find_return kf) in
- let fst_values =
- Db.Value.get_stmt_state (Kernel_function.find_first_stmt kf)
- in
+ let values = get_state_before (Kernel_function.find_return kf) in
+ let fst_values = get_state_before (Kernel_function.find_first_stmt kf) in
if Cvalue.Model.is_reachable fst_values
&& not (Cvalue.Model.is_top fst_values)
then begin
diff --git a/src/plugins/eva/domains/cvalue/cvalue_results.ml b/src/plugins/eva/domains/cvalue/cvalue_results.ml
new file mode 100644
index 0000000000000000000000000000000000000000..ff5b3a59f72f9395d9e3f9c42973bdfdcecfc715
--- /dev/null
+++ b/src/plugins/eva/domains/cvalue/cvalue_results.ml
@@ -0,0 +1,37 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+include Domain_store.Make (Cvalue.Model)
+
+let is_reachable stmt =
+ match get_stmt_state_by_callstack ~after:false stmt with
+ | `Top -> true
+ | `Bottom -> false
+ | `Value h ->
+ let exception Reachable in
+ try
+ let raise_if_reachable _cs state =
+ if Cvalue.Model.is_reachable state then raise Reachable
+ in
+ Callstack.Hashtbl.iter raise_if_reachable h;
+ false
+ with Reachable -> true
diff --git a/src/plugins/eva/domains/cvalue/cvalue_results.mli b/src/plugins/eva/domains/cvalue/cvalue_results.mli
new file mode 100644
index 0000000000000000000000000000000000000000..a5c6b9be684c26b3710fd6346962243a0212e68d
--- /dev/null
+++ b/src/plugins/eva/domains/cvalue/cvalue_results.mli
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Recording of cvalue states during the analysis. *)
+include Domain_store.S with type t := Cvalue.Model.t
+
+(** Returns true if a cvalue state has been recorded for this statement
+ (and so the analysis has reached the statement).
+ If possible, please use {!Results.is_reachable} instead. *)
+val is_reachable: Cil_types.stmt -> bool
diff --git a/src/plugins/eva/gui/gui_eval.ml b/src/plugins/eva/gui/gui_eval.ml
index bc338ad9cd9f916018566fb902f00affa3b8defe..3205c66f1626cdcf9cfbafd72be6a11af0af5b2c 100644
--- a/src/plugins/eva/gui/gui_eval.ml
+++ b/src/plugins/eva/gui/gui_eval.ml
@@ -320,9 +320,10 @@ module Make (X: Analysis.S) = struct
}
let pre_kf kf callstack =
- match Db.Value.get_initial_state_callstack kf with
- | None -> Cvalue.Model.top (* should not happen *)
- | Some h ->
+ match Cvalue_results.get_initial_state_by_callstack kf with
+ | `Top -> Cvalue.Model.top (* should not happen *)
+ | `Bottom -> Cvalue.Model.bottom
+ | `Value h ->
try Callstack.Hashtbl.find h callstack
with Not_found -> Cvalue.Model.top (* should not happen either *)
diff --git a/src/plugins/eva/legacy/eval_annots.ml b/src/plugins/eva/legacy/eval_annots.ml
index ca814b26cfbc3252f2e1a491436c22efa230b1e5..faa20947665a0e49c570974ad724dd48108c30ae 100644
--- a/src/plugins/eva/legacy/eval_annots.ml
+++ b/src/plugins/eva/legacy/eval_annots.ml
@@ -59,7 +59,7 @@ let mark_unreachable () =
in
(* Mark standard code annotations *)
let do_code_annot stmt _emit ca =
- if not (Db.Value.is_reachable_stmt stmt) then begin
+ if not (Cvalue_results.is_reachable stmt) then begin
let kf = Kernel_function.find_englobing_kf stmt in
let ppts = Property.ip_of_code_annot kf stmt ca in
List.iter mark ppts;
@@ -70,7 +70,7 @@ let mark_unreachable () =
inherit Visitor.frama_c_inplace
method! vstmt_aux stmt =
- if not (Db.Value.is_reachable_stmt stmt) then begin
+ if not (Cvalue_results.is_reachable stmt) then begin
let mark_status kf =
(* Do not mark preconditions as dead if they are not analyzed in
non-dead code. Otherwise, the consolidation does strange things. *)
@@ -115,11 +115,13 @@ let c_labels kf cs =
let fdec = Kernel_function.get_definition kf in
let aux acc stmt =
if stmt.labels != [] then
- try
- let hstate = Db.Value.Table_By_Callstack.find stmt in
- let state = Callstack.Hashtbl.find hstate cs in
- Cil_datatype.Logic_label.Map.add (StmtLabel (ref stmt)) state acc
- with Not_found -> acc
+ match Cvalue_results.get_stmt_state_by_callstack ~after:false stmt with
+ | `Bottom | `Top -> acc
+ | `Value hstate ->
+ try
+ let state = Callstack.Hashtbl.find hstate cs in
+ Cil_datatype.Logic_label.Map.add (StmtLabel (ref stmt)) state acc
+ with Not_found -> acc
else acc
in
List.fold_left aux Cil_datatype.Logic_label.Map.empty fdec.sallstmts
@@ -128,20 +130,23 @@ let c_labels kf cs =
(* TODO: we can probably factor some code with the GUI *)
let eval_by_callstack kf stmt p =
(* This is actually irrelevant for alarms: they never use \old *)
- let pre = Db.Value.get_initial_state kf in
- let aux_callstack callstack state acc_status =
- let c_labels = c_labels kf callstack in
- let env = Eval_terms.env_annot ~c_labels ~pre ~here:state () in
- let status = Eval_terms.eval_predicate env p in
- let join = Eval_terms.join_predicate_status in
- match Bottom.join join acc_status (`Value status) with
- | `Value Unknown -> raise Exit (* shortcut *)
- | _ as r -> r
- in
- match Db.Value.get_stmt_state_callstack ~after:false stmt with
- | None -> (* dead; ignore, those will be marked 'unreachable' elsewhere *)
+ let pre = Cvalue_results.get_initial_state kf in
+ let here = Cvalue_results.get_stmt_state_by_callstack ~after:false stmt in
+ match pre, here with
+ | `Bottom, _
+ | _, (`Top | `Bottom) ->
+ (* Ignore dead statements, those will be marked 'unreachable' elsewhere *)
Unknown
- | Some states ->
+ | `Value pre, `Value states ->
+ let aux_callstack callstack state acc_status =
+ let c_labels = c_labels kf callstack in
+ let env = Eval_terms.env_annot ~c_labels ~pre ~here:state () in
+ let status = Eval_terms.eval_predicate env p in
+ let join = Eval_terms.join_predicate_status in
+ match Bottom.join join acc_status (`Value status) with
+ | `Value Unknown -> raise Exit (* shortcut *)
+ | _ as r -> r
+ in
try
match Callstack.Hashtbl.fold aux_callstack states `Bottom with
| `Bottom -> Eval_terms.Unknown (* probably never reached *)
diff --git a/src/plugins/eva/utils/eva_results.ml b/src/plugins/eva/utils/eva_results.ml
index ca27209b4fef6fc25f80b5b14e47f558a595dad5..606158151f651cc2197e55f78b3b4b26ecfc1ca4 100644
--- a/src/plugins/eva/utils/eva_results.ml
+++ b/src/plugins/eva/utils/eva_results.ml
@@ -25,13 +25,9 @@ open Cil_datatype
(* {2 Termination.} *)
let partition_terminating_instr stmt =
- let ho =
- try Some (Db.Value.AfterTable_By_Callstack.find stmt)
- with Not_found -> None
- in
- match ho with
- | None -> ([], [])
- | Some h ->
+ match Cvalue_results.get_stmt_state_by_callstack ~after:true stmt with
+ | `Bottom | `Top -> ([], [])
+ | `Value h ->
let terminating = ref [] in
let non_terminating = ref [] in
let add x xs = xs := x :: !xs in
@@ -73,25 +69,29 @@ let get_results () =
let vue = Emitter.get Eva_utils.emitter in
let main = Some (fst (Globals.entry_point ())) in
let module CS = Callstack in
- let copy_states iter =
- let h = Stmt.Hashtbl.create 128 in
- let copy stmt hstack = Stmt.Hashtbl.add h stmt (CS.Hashtbl.copy hstack) in
- iter copy;
- h
- in
- let before_states = copy_states Db.Value.Table_By_Callstack.iter in
- let after_states = copy_states Db.Value.AfterTable_By_Callstack.iter in
- let kf_initial_states =
- let h = Kernel_function.Hashtbl.create 128 in
- let copy kf =
- match Db.Value.get_initial_state_callstack kf with
- | None -> ()
- | Some hstack ->
- Kernel_function.Hashtbl.add h kf (CS.Hashtbl.copy hstack)
+ let before_states = Stmt.Hashtbl.create 128 in
+ let after_states = Stmt.Hashtbl.create 128 in
+ let kf_initial_states = Kernel_function.Hashtbl.create 128 in
+ let copy_states stmt =
+ let copy h ~after stmt =
+ match Cvalue_results.get_stmt_state_by_callstack ~after stmt with
+ | `Top | `Bottom -> ()
+ | `Value states -> Stmt.Hashtbl.add h stmt (CS.Hashtbl.copy states)
in
- Globals.Functions.iter copy;
- h
+ copy before_states ~after:false stmt;
+ copy after_states ~after:true stmt;
in
+ let copy_kf kf =
+ match Cvalue_results.get_initial_state_by_callstack kf with
+ | `Top | `Bottom -> ()
+ | `Value hstack ->
+ Kernel_function.Hashtbl.add kf_initial_states kf (CS.Hashtbl.copy hstack);
+ try
+ let fundec = Kernel_function.get_definition kf in
+ List.iter copy_states fundec.sallstmts
+ with Kernel_function.No_Definition -> ()
+ in
+ Globals.Functions.iter copy_kf;
let kf_callers = Function_calls.get_results () in
let initial_state = Db.Value.globals_state () in
let initial_args = Db.Value.fun_get_args () in
@@ -140,18 +140,21 @@ let set_results results =
| Some l -> Db.Value.fun_set_args l
end;
(* Pre- and post-states *)
- let aux_states ~after stmt (h:stmt_by_callstack) =
- let aux_callstack callstack state =
- Db.Value.update_callstack_table ~after stmt callstack state;
+ let register_states register (tbl: stmt_by_callstack Stmt.Hashtbl.t) =
+ let copy stmt (h:stmt_by_callstack) =
+ let aux_callstack callstack state =
+ register callstack stmt state;
+ in
+ Callstack.Hashtbl.iter aux_callstack h
in
- Callstack.Hashtbl.iter aux_callstack h
+ Stmt.Hashtbl.iter copy tbl
in
- Stmt.Hashtbl.iter (aux_states ~after:false) results.before_states;
- Stmt.Hashtbl.iter (aux_states ~after:true) results.after_states;
+ register_states Cvalue_results.register_state_before_stmt results.before_states;
+ register_states Cvalue_results.register_state_after_stmt results.after_states;
(* Kf initial state *)
let aux_initial_state kf h =
let aux_callstack callstack state =
- Db.Value.merge_initial_state callstack kf state
+ Cvalue_results.register_initial_state callstack kf state
in
Callstack.Hashtbl.iter aux_callstack h
in
@@ -172,7 +175,7 @@ let set_results results =
Cvalue_domain.State.Store.register_global_state b
(`Value Cvalue_domain.State.top);
Self.ComputationState.set Computed;
- Db.Value.mark_as_computed ();
+ Cvalue_results.mark_as_computed ();
;;
module HExt (H: Hashtbl.S) =
diff --git a/src/plugins/eva/utils/private.ml b/src/plugins/eva/utils/private.ml
index bb7d45ac49ff7e8a7bad98b07171ae33ef87585b..e4a368655a9c996dcafcb0369e4ba346cfa6549b 100644
--- a/src/plugins/eva/utils/private.ml
+++ b/src/plugins/eva/utils/private.ml
@@ -30,6 +30,7 @@ module Alarmset = Alarmset
module Analysis = Analysis
module Callstack = Callstack
module Cvalue_domain = Cvalue_domain
+module Cvalue_results = Cvalue_results
module Domain_builder = Domain_builder
module Eva_dynamic = Eva_dynamic
module Eva_results = Eva_results
diff --git a/src/plugins/eva/utils/private.mli b/src/plugins/eva/utils/private.mli
index 8fb57decf5b6c805f6776917c96f537c42709bc1..f70377152869169e4763bef80aca6d553384f555 100644
--- a/src/plugins/eva/utils/private.mli
+++ b/src/plugins/eva/utils/private.mli
@@ -34,6 +34,7 @@ module Alarmset = Alarmset
module Analysis = Analysis
module Callstack = Callstack
module Cvalue_domain = Cvalue_domain
+module Cvalue_results = Cvalue_results
module Domain_builder = Domain_builder
module Eva_dynamic = Eva_dynamic
module Eva_results = Eva_results
diff --git a/src/plugins/eva/utils/summary.ml b/src/plugins/eva/utils/summary.ml
index 5462206ea9e00f519b3b10d5c845c946f877bbf9..8cbda580583972f9c215f7d9e6306c37199d8127 100644
--- a/src/plugins/eva/utils/summary.ml
+++ b/src/plugins/eva/utils/summary.ml
@@ -180,7 +180,7 @@ let compute_fun_stats fundec =
List.iter (do_status alarm) l
in
let do_stmt stmt =
- let reachable = Db.Value.is_reachable_stmt stmt in
+ let reachable = Cvalue_results.is_reachable stmt in
Coverage.incr coverage ~reachable;
Annotations.iter_code_annot (do_annot stmt) stmt
in
@@ -256,7 +256,7 @@ let compute_statuses () =
in
let do_property ip =
let incr stmt statuses =
- if Db.Value.is_reachable_stmt stmt then
+ if Cvalue_results.is_reachable stmt then
match get_status ip with
| None -> ()
| Some status -> Statuses.incr statuses status