diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index a091fe04227fc0d4464dabc11898e6314867fbaa..a35cbf068533b07824f911b6b715480f7570e117 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -674,38 +674,13 @@ module Value = struct
end
module From = struct
-
exception Not_lval
- let access = mk_fun "From.access"
let find_deps_no_transitivity = mk_fun "From.find_deps_no_transitivity"
let find_deps_no_transitivity_state =
mk_fun "From.find_deps_no_transitivity_state"
let find_deps_term_no_transitivity_state =
mk_fun "From.find_deps_term_no_transitivity_state"
- let compute = mk_fun "From.compute"
- let compute_all = mk_fun "From.compute_all"
- let compute_all_calldeps = mk_fun "From.compute_all_calldeps"
- let is_computed = mk_fun "From.is_computed"
- let pretty = mk_fun "From.pretty"
- let get = mk_fun "From.get"
- let self = ref State.dummy
- let display = mk_fun "From.display"
-
- module Record_From_Callbacks =
- Hook.Build
- (struct
- type t =
- (Kernel_function.t Stack.t) *
- Function_Froms.Memory.t Stmt.Hashtbl.t *
- (Kernel_function.t * Function_Froms.Memory.t) list
- Stmt.Hashtbl.t
- end)
-
- module Callwise = struct
- let iter = mk_fun "From.Callwise.iter"
- let find = mk_fun "From.Callwise.find"
- end
end
(* ************************************************************************* *)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 2ba86cfddf58dda836d6fce0e768bfa3d7fe71e9..7b072132ade4ebb828bd4e1e81d72b8a45c9af5f 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -513,20 +513,6 @@ module From : sig
*)
exception Not_lval
- val compute_all : (unit -> unit) ref
- val compute_all_calldeps : (unit -> unit) ref
-
- val compute : (kernel_function -> unit) ref
-
- val is_computed: (kernel_function -> bool) ref
- (** Check whether the from analysis has been performed for the given
- function.
- @return true iff the analysis has been performed *)
-
- val get : (kernel_function -> Function_Froms.t) ref
- val access : (Locations.Zone.t -> Function_Froms.Memory.t
- -> Locations.Zone.t) ref
-
val find_deps_no_transitivity : (stmt -> exp -> Locations.Zone.t) ref
val find_deps_no_transitivity_state :
@@ -536,29 +522,10 @@ module From : sig
val find_deps_term_no_transitivity_state :
(Cvalue.Model.t -> term -> Value_types.logic_dependencies) ref
- val self: State.t ref
-
- (** {3 Pretty printing} *)
-
- val pretty : (Format.formatter -> kernel_function -> unit) ref
- val display : (Format.formatter -> unit) ref
-
- (** {3 Callback} *)
-
- module Record_From_Callbacks:
- Hook.Iter_hook with type param =
- Kernel_function.t Stack.t *
- Function_Froms.Memory.t Stmt.Hashtbl.t *
- (Kernel_function.t * Function_Froms.Memory.t) list
- Stmt.Hashtbl.t
-
- (** {3 Access to callwise-stored data} *)
-
- module Callwise : sig
- val iter : ((kinstr -> Function_Froms.t -> unit) -> unit) ref
- val find : (kinstr -> Function_Froms.t) ref
- end
end
+[@@alert db_deprecated
+ "Db.From is deprecated and will be removed in a future version \
+ of Frama-C. Please use the From module or the Eva API instead."]
(* ************************************************************************* *)
(** {2 Properties} *)
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 0adbbd5ebd2178991f430073708a86c7c5f6503d..3b01353a856e3a5e391be69702788182fad68504 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -669,6 +669,11 @@ module Logic_inout: sig
pre:Cvalue.Model.t -> here:Cvalue.Model.t ->
Cil_types.predicate -> Locations.Zone.t option
+ (** [term_deps state t] computes the logic dependencies needed to evaluate
+ the term [t] in cvalue state [state].
+ Returns None on either an evaluation error or on unsupported construct. *)
+ val term_deps: Cvalue.Model.t -> Cil_types.term -> Locations.Zone.t option
+
(** Returns the list of behaviors of the given function that are active for
the given initial state. *)
val valid_behaviors:
diff --git a/src/plugins/eva/legacy/logic_inout.ml b/src/plugins/eva/legacy/logic_inout.ml
index e4b4c543a701109dc90c688a4f202ce58c430887..7ae89d1e63344cad129208aff8220dfd5ef1e1da 100644
--- a/src/plugins/eva/legacy/logic_inout.ml
+++ b/src/plugins/eva/legacy/logic_inout.ml
@@ -31,16 +31,19 @@ let predicate_deps ~pre ~here predicate =
let logic_deps = Eval_terms.predicate_deps env predicate in
Option.map join_logic_deps logic_deps
-let term_deps stmt t =
+let term_deps state t =
try
- let state = Results.(before stmt |> get_cvalue_model) in
let env = Eval_terms.env_only_here state in
let r = Eval_terms.eval_term ~alarm_mode:Eval_terms.Ignore env t in
let zone = join_logic_deps r.Eval_terms.ldeps in
Some zone
with Eval_terms.LogicEvalError _ -> None
-let () = Logic_interp.To_zone.compute_term_deps := term_deps
+let compute_term_deps stmt t =
+ let state = Results.(before stmt |> get_cvalue_model) in
+ term_deps state t
+
+let () = Logic_interp.To_zone.compute_term_deps := compute_term_deps
let valid_behaviors kf state =
let funspec = Annotations.funspec kf in
diff --git a/src/plugins/eva/legacy/logic_inout.mli b/src/plugins/eva/legacy/logic_inout.mli
index 7e478d9b4c5cada150d08b830a78cdd701c3e283..d79e25f77ba717488ff74f6d3fa8ad728eabbee7 100644
--- a/src/plugins/eva/legacy/logic_inout.mli
+++ b/src/plugins/eva/legacy/logic_inout.mli
@@ -34,6 +34,11 @@ val predicate_deps:
pre:Cvalue.Model.t -> here:Cvalue.Model.t ->
Cil_types.predicate -> Locations.Zone.t option
+(** [term_deps state t] computes the logic dependencies needed to evaluate
+ the term [t] in cvalue state [state].
+ Returns None on either an evaluation error or on unsupported construct. *)
+val term_deps: Cvalue.Model.t -> Cil_types.term -> Locations.Zone.t option
+
(** Returns the list of behaviors of the given function that are active for
the given initial state. *)
val valid_behaviors:
diff --git a/src/plugins/eva/register.ml b/src/plugins/eva/register.ml
index 197393e0a5592251d9aaf9201d072a6e3617a309..adac4dbcfe34b33c748c23dcd324795782e8bcf5 100644
--- a/src/plugins/eva/register.ml
+++ b/src/plugins/eva/register.ml
@@ -54,6 +54,12 @@ let find_deps_term_no_transitivity_state state t =
r.Eval_terms.ldeps
with Eval_terms.LogicEvalError _ -> raise Db.From.Not_lval
+let find_deps_no_transitivity stmt expr =
+ Results.(before stmt |> expr_deps expr)
+
+let find_deps_no_transitivity_state state expr =
+ Results.(in_cvalue_state state |> expr_deps expr)
+
let eval_predicate ~pre ~here p =
let open Eval_terms in
let env = env_annot ~pre ~here () in
@@ -77,6 +83,8 @@ let () =
Db.Value.valid_behaviors := Logic_inout.valid_behaviors;
Db.From.find_deps_term_no_transitivity_state :=
find_deps_term_no_transitivity_state;
+ Db.From.find_deps_no_transitivity := find_deps_no_transitivity;
+ Db.From.find_deps_no_transitivity_state := find_deps_no_transitivity_state;
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/from/From.ml b/src/plugins/from/From.ml
new file mode 100644
index 0000000000000000000000000000000000000000..f1faee921ea76b7b1469f25d9d8b51aa3fd6e066
--- /dev/null
+++ b/src/plugins/from/From.ml
@@ -0,0 +1,38 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+let self = Functionwise.self
+let compute = Functionwise.compute
+let compute_all = Functionwise.compute_all
+let is_computed = Functionwise.is_computed
+let get = Functionwise.get
+let pretty = Functionwise.pretty
+
+let access zone mem = Function_Froms.Memory.find mem zone
+
+let display fmt = From_register.display (Some fmt)
+
+let compute_all_calldeps = Callwise.compute_all_calldeps
+module Callwise = struct
+ let iter = Callwise.iter
+ let find = Callwise.find
+end
diff --git a/src/plugins/from/From.mli b/src/plugins/from/From.mli
new file mode 100644
index 0000000000000000000000000000000000000000..ba438f58b2c6f41247336c98f4e111409d45fdbb
--- /dev/null
+++ b/src/plugins/from/From.mli
@@ -0,0 +1,47 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+(** {3 Analysis} *)
+
+val is_computed : kernel_function -> bool
+val compute : kernel_function -> unit
+val compute_all : unit -> unit
+
+val get : Cil_types.kernel_function -> Function_Froms.froms
+val access : Locations.Zone.t -> Function_Froms.Memory.t -> Locations.Zone.t
+
+val self : State.t
+
+(** {3 Pretty-printing} *)
+
+val pretty : Format.formatter -> kernel_function -> unit
+val display : Format.formatter -> unit
+
+(** {3 Callsite-wise analysis} *)
+
+val compute_all_calldeps : unit -> unit
+module Callwise : sig
+ val iter : (Cil_types.kinstr -> Function_Froms.froms -> unit) -> unit
+ val find : Cil_types.kinstr -> Function_Froms.froms
+end
diff --git a/src/plugins/from/callwise.ml b/src/plugins/from/callwise.ml
index 41a49e2e0a289dd89aa561ba2584d8fb2bc09b5c..efbfe6b8fa1ef07fe7cc7b34d24503f247be033c 100644
--- a/src/plugins/from/callwise.ml
+++ b/src/plugins/from/callwise.ml
@@ -183,22 +183,17 @@ let () =
Eva.Cvalue_callbacks.register_call_hook call_for_individual_froms;
Eva.Cvalue_callbacks.register_call_results_hook record_for_individual_froms
-
-let force_compute_all_calldeps ()=
- if Eva.Analysis.is_computed () then
- Project.clear
- ~selection:(State_selection.with_dependencies Eva.Analysis.self)
- ();
- Eva.Analysis.compute ()
-
-(* Registration for call-wise from *)
-let () =
- Db.register_guarded_compute
- Tbl.is_computed
- Db.From.compute_all_calldeps
- force_compute_all_calldeps;
- Db.From.Callwise.iter := Tbl.iter;
- Db.From.Callwise.find := Tbl.find
+let iter = Tbl.iter
+let find = Tbl.find
+
+let compute_all_calldeps () =
+ if not (Tbl.is_computed ()) then begin
+ if Eva.Analysis.is_computed () then
+ Project.clear
+ ~selection:(State_selection.with_dependencies Eva.Analysis.self)
+ ();
+ Eva.Analysis.compute ()
+ end
(*
Local Variables:
diff --git a/src/plugins/from/callwise.mli b/src/plugins/from/callwise.mli
index 26d419c142dccc3e30658ed11ae9fcb3b920b60e..299637c55d68960045d17b7fbc54f4de24d56741 100644
--- a/src/plugins/from/callwise.mli
+++ b/src/plugins/from/callwise.mli
@@ -22,7 +22,8 @@
(** Computation of callwise functional dependencies. The results are computed
while the value analysis runs, and the results are usually much more
- precise than the functionwise results.
+ precise than the functionwise results. *)
- Nothing is exported here, the API can be found in the
- Db.From.Callwise module *)
+val compute_all_calldeps : unit -> unit
+val iter : (Cil_types.kinstr -> Function_Froms.froms -> unit) -> unit
+val find : Cil_types.kinstr -> Function_Froms.froms
diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index 0805d3aef48555180c59ab2099575d29c51bb89d..14f127e123d57181ee9a74c02a66775eeeecc107 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -28,6 +28,15 @@ open Locations
exception Call_did_not_take_place
+module Record_From_Callbacks =
+ Hook.Build
+ (struct
+ type t =
+ (Kernel_function.t Stack.t) *
+ Function_Froms.Memory.t Stmt.Hashtbl.t *
+ (Kernel_function.t * Function_Froms.Memory.t) list Stmt.Hashtbl.t
+ end)
+
module type To_Use =
sig
val get_from_call : kernel_function -> stmt -> Function_Froms.t
@@ -363,7 +372,7 @@ struct
(List.length formal_args)
(List.length args_froms))
end;
- if not (Db.From.Record_From_Callbacks.is_empty ())
+ if not (Record_From_Callbacks.is_empty ())
then
states_with_formals :=
(kf, !state_with_formals) :: !states_with_formals;
@@ -408,7 +417,7 @@ struct
| Some s -> s);
with Call_did_not_take_place -> state
in
- if not (Db.From.Record_From_Callbacks.is_empty ())
+ if not (Record_From_Callbacks.is_empty ())
then
Stmt.Hashtbl.replace
callwise_states_with_formals
@@ -582,7 +591,7 @@ struct
in
let module Compute = Dataflows.Simple_forward(Fenv)(Dataflow_arg) in
let ret_id = Kernel_function.find_return kf in
- if not (Db.From.Record_From_Callbacks.is_empty ())
+ if not (Record_From_Callbacks.is_empty ())
then begin
From_parameters.feedback "Now calling From callbacks";
let states =
@@ -590,7 +599,7 @@ struct
in
Compute.iter_on_result (fun k record ->
Stmt.Hashtbl.add states k record.deps_table);
- Db.From.Record_From_Callbacks.apply
+ Record_From_Callbacks.apply
(call_stack, states, Dataflow_arg.callwise_states_with_formals)
end;
let _poped = Stack.pop call_stack in
diff --git a/src/plugins/from/from_register.ml b/src/plugins/from/from_register.ml
index 61a61f23ed3bab0bf24cd21deaad33401ef4743c..60810a55a3fb47818beb310bae56fc7c4acb55e8 100644
--- a/src/plugins/from/from_register.ml
+++ b/src/plugins/from/from_register.ml
@@ -23,7 +23,7 @@
open Cil_types
let pretty_with_indirect fmt v =
- let deps = !Db.From.get v in
+ let deps = Functionwise.get v in
Function_Froms.pretty_with_type_indirect (Kernel_function.get_type v) fmt deps
let display fmtopt =
@@ -37,7 +37,7 @@ let display fmtopt =
let pretty =
if From_parameters.ShowIndirectDeps.get ()
then pretty_with_indirect
- else !Db.From.pretty
+ else Functionwise.pretty
in
match fmtopt with
| None ->
@@ -63,7 +63,7 @@ module MapStmtCalls = Map.Make(SortCalls)
let iter_callwise_calls_sorted f =
let hkf = Kernel_function.Hashtbl.create 17 in
let kglobal = ref None in
- !Db.From.Callwise.iter
+ Callwise.iter
(fun ki d ->
match ki with
| Kglobal -> kglobal := Some d
@@ -148,28 +148,18 @@ let main () =
if From_parameters.ForceDeps.get () then
From_parameters.ForceDeps.output
(fun () ->
- !Db.From.compute_all ();
+ Functionwise.compute_all ();
print_deps ();
);
if From_parameters.ForceCallDeps.get () then
From_parameters.ForceCallDeps.output
(fun () ->
- !Db.From.compute_all_calldeps ();
+ Callwise.compute_all_calldeps ();
if not_quiet then print_calldeps ();
)
let () = Db.Main.extend main
-let access_from zone mem = Function_Froms.Memory.find mem zone
-
-(* Registration for most Db.From functions is done at the end of the
- Functionwise and Callwise modules *)
-let () =
- Db.From.display := (fun fmt -> display (Some fmt));
- Db.From.access := access_from;
-
-
-
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/plugins/from/from_register.mli b/src/plugins/from/from_register.mli
index cc955b0d1e20900dadc0eb4fe6c187ea3f9986ed..5e563bbed1499a2cbadc36ed47c60998a990cb0a 100644
--- a/src/plugins/from/from_register.mli
+++ b/src/plugins/from/from_register.mli
@@ -20,5 +20,6 @@
(* *)
(**************************************************************************)
-(** Registration of the From plugin in Frama-C main loop.
- Nothing is exported in this module *)
+(** Registration of the From plugin in Frama-C main loop. *)
+
+val display : Format.formatter option -> unit
diff --git a/src/plugins/from/functionwise.ml b/src/plugins/from/functionwise.ml
index fed913033aa883471918032861ca60a8ab72715a..ee80d0cc402bcdc114ff443b86b4773b55e4a4c9 100644
--- a/src/plugins/from/functionwise.ml
+++ b/src/plugins/from/functionwise.ml
@@ -86,43 +86,29 @@ module To_Use = struct
end
module From = From_compute.Make(To_Use)
+let () = force_compute := From.compute
-let () =
- force_compute := From.compute
+let self = Tbl.self
+
+let compute kf = ignore (To_Use.memo kf)
let force_compute_all () =
- Eva.Analysis.compute ();
- Callgraph.Uses.iter_in_rev_order
- (fun kf ->
- if Kernel_function.is_definition kf && Eva.Results.is_called kf
- then !Db.From.compute kf)
-
-(* Db Registration for function-wise from *)
-let () =
- Db.From.self := Tbl.self;
- Db.From.is_computed := Tbl.mem;
- Db.From.compute :=
- (fun kf -> ignore (To_Use.memo kf));
- Db.From.get := To_Use.memo;
- Db.From.pretty :=
- (fun fmt v ->
- let deps = To_Use.memo v in
- Function_Froms.pretty_with_type (Kernel_function.get_type v) fmt deps);
- Db.From.find_deps_no_transitivity :=
- (fun stmt expr ->
- Eva.Results.(before stmt |> expr_deps expr));
- (* Once this function has been moved to Eva, remove the dependency of Inout
- from From. *)
- Db.From.find_deps_no_transitivity_state :=
- (fun s e -> Eva.Results.(in_cvalue_state s |> expr_deps e));
-
- ignore (
- Db.register_compute "From.compute_all"
- [Tbl.self]
- Db.From.compute_all
- force_compute_all);
+ Eva.Analysis.compute () ;
+ Callgraph.Uses.iter_in_rev_order @@ fun kf ->
+ let is_definition = Kernel_function.is_definition kf in
+ if is_definition && Eva.Results.is_called kf then compute kf
+
+let compute_all =
+ let name = "From.compute_all" in
+ State_builder.apply_once name [Tbl.self] force_compute_all |> fst
+
+let is_computed = Tbl.mem
+
+let get = To_Use.memo
+let pretty fmt v =
+ Function_Froms.pretty_with_type (Kernel_function.get_type v) fmt (get v)
(*
Local Variables:
diff --git a/src/plugins/from/functionwise.mli b/src/plugins/from/functionwise.mli
index 5d51ae4b1af5f30c1b103f204c1d52d93546dfe0..1e6e14f2d3cd2aae6cdf9db00cef00e3b9743add 100644
--- a/src/plugins/from/functionwise.mli
+++ b/src/plugins/from/functionwise.mli
@@ -21,6 +21,13 @@
(**************************************************************************)
(** Computation of functional dependencies. In this module, the results are
- computed from the synthetic results of the value analysis.
+ computed from the synthetic results of the value analysis. *)
- Nothing is exported here, the API can be found in the Db.From module *)
+open Cil_types
+
+val self : State.t
+val compute : kernel_function -> unit
+val compute_all : unit -> unit
+val is_computed : kernel_function -> bool
+val get : Cil_types.kernel_function -> Function_Froms.froms
+val pretty : Format.formatter -> kernel_function -> unit
diff --git a/src/plugins/from/gui/from_register_gui.ml b/src/plugins/from/gui/from_register_gui.ml
index c547b6da336edc04b350a69e222ba2fdc97a37e2..75408de49df139215a4ee3df1b4d46dc4b00f24b 100644
--- a/src/plugins/from/gui/from_register_gui.ml
+++ b/src/plugins/from/gui/from_register_gui.ml
@@ -32,9 +32,9 @@ let main (main_ui:Design.main_window_extension_points) =
begin
try
let kf = Globals.Functions.get v in
- if !Db.From.is_computed kf then
+ if From.is_computed kf then
main_ui#pretty_information
- "@[Functional dependencies:@\n%a@]@." !Db.From.pretty kf
+ "@[Functional dependencies:@\n%a@]@." From.pretty kf
with Not_found -> ()
end
| _ -> ();
diff --git a/src/plugins/pdg/build.ml b/src/plugins/pdg/build.ml
index 34dfb781a9acc918cf7bbffb2cd0f28718053bbd..2a6758a85fdadc7dc979c97669c3b738cd45f517 100644
--- a/src/plugins/pdg/build.ml
+++ b/src/plugins/pdg/build.ml
@@ -621,7 +621,7 @@ let get_lval_infos lval stmt =
Use the state at ki (before assign)
and returns the new state (after assign). *)
let process_asgn pdg state stmt lval exp =
- let r_dpds = !Db.From.find_deps_no_transitivity stmt exp in
+ let r_dpds = Eva.Results.(before stmt |> expr_deps exp) in
let r_decl = Cil.extract_varinfos_from_exp exp in
let (l_loc, exact, l_dpds, l_decl) = get_lval_infos lval stmt in
let key = Key.stmt_key stmt in
@@ -636,7 +636,7 @@ let process_asgn pdg state stmt lval exp =
(** Add a PDG node and its dependencies for each explicit call argument. *)
let process_args pdg st stmt argl =
let process_one_arg arg =
- let dpds = !Db.From.find_deps_no_transitivity stmt arg in
+ let dpds = Eva.Results.(before stmt |> expr_deps arg) in
let decl_dpds = Cil.extract_varinfos_from_exp arg in
(dpds, decl_dpds)
in let arg_dpds = List.map process_one_arg argl in
@@ -717,7 +717,7 @@ let process_call pdg state stmt lvaloption funcexp argl _loc =
| _ -> assert false
in
let mixed_froms =
- try let froms = !Db.From.Callwise.find (Kstmt stmt) in Some froms
+ try let froms = From.Callwise.find (Kstmt stmt) in Some froms
with Not_found -> None (* don't have callwise analysis (-calldeps option) *)
in
let process_simple_call acc called_kf =
@@ -728,7 +728,7 @@ let process_call pdg state stmt lvaloption funcexp argl _loc =
match mixed_froms with
| Some _ -> state_with_inputs (* process outputs later *)
| None -> (* don't have callwise analysis (-calldeps option) *)
- let froms = !Db.From.get called_kf in
+ let froms = From.get called_kf in
let state_for_this_call =
call_outputs pdg state_before_call state_with_inputs
stmt lvaloption froms funcexp_dpds
@@ -763,7 +763,7 @@ let process_call pdg state stmt lvaloption funcexp argl _loc =
* and register the statements that are control-dependent on it.
*)
let process_condition ctrl_dpds_infos pdg state stmt condition =
- let loc_cond = !Db.From.find_deps_no_transitivity stmt condition in
+ let loc_cond = Eva.Results.(before stmt |> expr_deps condition) in
let decls_cond = Cil.extract_varinfos_from_exp condition in
let controlled_stmts = CtrlDpds.get_if_controlled_stmts ctrl_dpds_infos stmt in
@@ -819,7 +819,7 @@ let process_return _current_function pdg state stmt ret_exp =
let last_state =
match ret_exp with
| Some exp ->
- let loc_exp = !Db.From.find_deps_no_transitivity stmt exp in
+ let loc_exp = Eva.Results.(before stmt |> expr_deps exp) in
let decls_exp = Cil.extract_varinfos_from_exp exp in
add_retres pdg state stmt loc_exp decls_exp
| None ->
@@ -963,7 +963,7 @@ let compute_pdg_for_f kf =
let froms = match f_stmts with
| [] ->
Pdg_state.store_last_state pdg.states init_state;
- let froms = !Db.From.get kf in
+ let froms = From.get kf in
Some (froms)
| start :: _ ->
let ctrl_dpds_infos = CtrlDpds.compute kf in
diff --git a/src/plugins/pdg/register.ml b/src/plugins/pdg/register.ml
index 8217fb8ccc0794e95ec2b72c7178730c50fa990c..b13b6da852cfbcf7bd3c8c1aa34cc56ef3420b31 100644
--- a/src/plugins/pdg/register.ml
+++ b/src/plugins/pdg/register.ml
@@ -28,7 +28,7 @@ let () =
(fun () ->
State_dependency_graph.add_codependencies
~onto:Pdg_tbl.self
- [ !Db.From.self ])
+ [ From.self ])
let deps =
[Pdg_tbl.self; Pdg_parameters.BuildAll.self; Pdg_parameters.BuildFct.self]
diff --git a/src/plugins/scope/zones.ml b/src/plugins/scope/zones.ml
index ba308e499fa2110d4aef18bbe2f29c18c890d9e8..78134d802f236c54ba91f58004e23205a0925241 100644
--- a/src/plugins/scope/zones.ml
+++ b/src/plugins/scope/zones.ml
@@ -40,7 +40,7 @@ module Data = struct
let diff = Locations.Zone.diff (* over-approx *)
let pretty fmt z = Format.fprintf fmt "@[<h 1>%a@]" Locations.Zone.pretty z
- let exp_zone stmt exp = !Db.From.find_deps_no_transitivity stmt exp
+ let exp_zone stmt exp = Eva.Results.(before stmt |> expr_deps exp)
end
module Ctx = struct
@@ -160,12 +160,12 @@ let process_call data_after stmt lvaloption funcexp args _loc =
in
let used, data =
try
- let froms = !Db.From.Callwise.find (Kstmt stmt) in
+ let froms = From.Callwise.find (Kstmt stmt) in
process_one_call data_after stmt lvaloption froms
with Not_found -> (* don't have callwise (-calldeps option) *)
let do_call acc kf =
(* notice that we use the same old data for each possible call *)
- (process_one_call data_after stmt lvaloption (!Db.From.get kf))::acc
+ (process_one_call data_after stmt lvaloption (From.get kf))::acc
in
let l = List.fold_left do_call [] called_functions in
(* in l, we have one result for each possible function called *)
diff --git a/src/plugins/slicing/fct_slice.ml b/src/plugins/slicing/fct_slice.ml
index 43be72e63ec8990bfab89552dde3857cebd463e6..520907fcaed2ed9ebb8201f4dcf2b4c0fe27dc18 100644
--- a/src/plugins/slicing/fct_slice.ml
+++ b/src/plugins/slicing/fct_slice.ml
@@ -957,7 +957,7 @@ let add_change_call_action ff call call_info f_to_call actions =
(** This function doesn't use the PDG call dependencies on purpose !
* See explanations in [add_spare_call_inputs] *)
let get_called_needed_input called_kf need_out0 needed_out_zone =
- let froms = !Db.From.get called_kf in
+ let froms = From.get called_kf in
let from_table = froms.Function_Froms.deps_table in
let acc_in_zones out (default, from_out) in_zones =
if Locations.Zone.valid_intersects needed_out_zone out then
diff --git a/src/plugins/slicing/slicingCmds.ml b/src/plugins/slicing/slicingCmds.ml
index 65c51a49d3de59b54b75d4d0fba00e3dc7794acc..7bdf6c01161551dac897a8076f0e7664630573f4 100644
--- a/src/plugins/slicing/slicingCmds.ml
+++ b/src/plugins/slicing/slicingCmds.ml
@@ -86,10 +86,10 @@ struct
in
let call_process lv f args _loc =
(* returns [Zone.t read] by [lv, f, args], [Zone.t written] by [lv] *)
- let read_zone = !Db.From.find_deps_no_transitivity stmt f in
+ let read_zone = Eva.Results.(before stmt |> expr_deps f) in
let add_args arg inputs =
- Locations.Zone.join inputs
- (!Db.From.find_deps_no_transitivity stmt arg) in
+ Locations.Zone.join inputs Eva.Results.(before stmt |> expr_deps arg)
+ in
let read_zone = List.fold_right add_args args read_zone in
let read_zone,write_zone =
match lv with
@@ -101,16 +101,16 @@ struct
| Switch (exp,_,_,_)
| If (exp,_,_,_) ->
(* returns [Zone.t read] by condition [exp], [Zone.bottom] *)
- !Db.From.find_deps_no_transitivity stmt exp, Locations.Zone.bottom
+ Eva.Results.(before stmt |> expr_deps exp), Locations.Zone.bottom
| Instr (Set (lv,exp,_)) ->
(* returns [Zone.t read] by [exp, lv], [Zone.t written] by [lv] *)
- let read_zone = !Db.From.find_deps_no_transitivity stmt exp in
+ let read_zone = Eva.Results.(before stmt |> expr_deps exp) in
lval_process read_zone stmt lv
| Instr (Local_init (v, AssignInit i, _)) ->
let rec collect zone i =
match i with
| SingleInit e ->
- Locations.Zone.join zone (!Db.From.find_deps_no_transitivity stmt e)
+ Locations.Zone.join zone Eva.Results.(before stmt |> expr_deps e)
| CompoundInit (_,l) ->
List.fold_left
(fun acc (_,i) -> collect acc i) zone l
diff --git a/tests/pdg/dyn_dpds.ml b/tests/pdg/dyn_dpds.ml
index 4907cf29314c0d98ef989c991d66b70567bc1493..402616dac4b83282d03f51ba07270078fd889677 100644
--- a/tests/pdg/dyn_dpds.ml
+++ b/tests/pdg/dyn_dpds.ml
@@ -8,12 +8,8 @@ zgrviewer tests/pdg/dyn_dpds_2.dot ;
let get_zones str_data (stmt, kf) =
let lval_term = !Db.Properties.Interp.term_lval kf str_data in
let lval = !Db.Properties.Interp.term_lval_to_lval ~result:None lval_term in
- let loc =
- !Db.From.find_deps_no_transitivity
- stmt
- (Cil.new_exp ~loc:Cil_datatype.Location.unknown (Cil_types.Lval lval))
- in
- loc
+ let exp = Cil.new_exp ~loc:Cil_datatype.Location.unknown (Cil_types.Lval lval) in
+ Eva.Results.(before stmt |> expr_deps exp)
let main _ =
let memo_debug = Kernel.Debug.get () in