diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml index 9a875ee9477b613bcdac6980795be2c9d242d04e..76b7fa9c5d6a08bcc0c6ca452460187c0e9ca830 100644 --- a/src/plugins/from/from_compute.ml +++ b/src/plugins/from/from_compute.ml @@ -36,37 +36,6 @@ sig val cleanup_and_save : kernel_function -> Function_Froms.t -> Function_Froms.t end -let rec find_deps_no_transitivity state expr = - (* The value of the expression [expr], just before executing the statement - [instr], is a function of the values of the returned zones. *) - match expr.enode with - | AlignOfE _| AlignOf _| SizeOfStr _ |SizeOfE _| SizeOf _ | Const _ - -> Function_Froms.Deps.bottom - | AddrOf lv | StartOf lv -> - let deps, _ = !Db.Value.lval_to_loc_with_deps_state (* loc ignored *) - state - ~deps:Zone.bottom - lv - in - Function_Froms.Deps.from_data_deps deps - | CastE (_, e)|UnOp (_, e, _) -> - find_deps_no_transitivity state e - | BinOp (_, e1, e2, _) -> - Function_Froms.Deps.join - (find_deps_no_transitivity state e1) - (find_deps_no_transitivity state e2) - | Lval v -> - find_deps_lval_no_transitivity state v - -and find_deps_lval_no_transitivity state lv = - let ind_deps, direct_deps, _exact = - !Db.Value.lval_to_zone_with_deps_state - state ~for_writing:false ~deps:(Some Zone.bottom) lv - in - From_parameters.debug "find_deps_lval_no_trs:@\n deps:%a@\n direct_deps:%a" - Zone.pretty ind_deps Zone.pretty direct_deps; - { Function_Froms.Deps.data = direct_deps; indirect = ind_deps } - let compute_using_prototype_for_state state kf assigns = let varinfo = Kernel_function.get_vi kf in let return_deps,deps = diff --git a/src/plugins/from/from_compute.mli b/src/plugins/from/from_compute.mli index d66e9312f4920256752b91ce16e00dc2fb86067a..e53256d9f9a1cf43ca0b5aefa5c42c5b36f8a72a 100644 --- a/src/plugins/from/from_compute.mli +++ b/src/plugins/from/from_compute.mli @@ -55,14 +55,6 @@ val compute_using_prototype_for_state : Function_Froms.froms -(** Direct computation of the dependencies on expressions, offsets and - lvals. The state at the statement is taken from Values_To_Use *) -val find_deps_no_transitivity : - Db.Value.state -> exp -> Function_Froms.Deps.t -val find_deps_lval_no_transitivity : - Db.Value.state -> lval -> Function_Froms.Deps.t - - (** Functor computing the functional dependencies, according to the three modules above. *) module Make (To_Use: To_Use) : sig diff --git a/src/plugins/from/functionwise.ml b/src/plugins/from/functionwise.ml index e397a4d3dbedee8475acaf33ba0ee3c9677fe909..fed913033aa883471918032861ca60a8ab72715a 100644 --- a/src/plugins/from/functionwise.ml +++ b/src/plugins/from/functionwise.ml @@ -115,9 +115,7 @@ let () = (* 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 -> - let deps = From_compute.find_deps_no_transitivity s e in - Function_Froms.Deps.to_zone deps); + (fun s e -> Eva.Results.(in_cvalue_state s |> expr_deps e)); ignore ( Db.register_compute "From.compute_all"