Skip to content
Snippets Groups Projects
Commit 217d4fa1 authored by David Bühler's avatar David Bühler
Browse files

[from] Removes now unused functions [find_deps_*_no_transitivity].

parent 7f02892e
No related branches found
No related tags found
No related merge requests found
...@@ -36,37 +36,6 @@ sig ...@@ -36,37 +36,6 @@ sig
val cleanup_and_save : kernel_function -> Function_Froms.t -> Function_Froms.t val cleanup_and_save : kernel_function -> Function_Froms.t -> Function_Froms.t
end 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 compute_using_prototype_for_state state kf assigns =
let varinfo = Kernel_function.get_vi kf in let varinfo = Kernel_function.get_vi kf in
let return_deps,deps = let return_deps,deps =
......
...@@ -55,14 +55,6 @@ val compute_using_prototype_for_state : ...@@ -55,14 +55,6 @@ val compute_using_prototype_for_state :
Function_Froms.froms 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 (** Functor computing the functional dependencies, according to the three
modules above. *) modules above. *)
module Make (To_Use: To_Use) : sig module Make (To_Use: To_Use) : sig
......
...@@ -115,9 +115,7 @@ let () = ...@@ -115,9 +115,7 @@ let () =
(* Once this function has been moved to Eva, remove the dependency of Inout (* Once this function has been moved to Eva, remove the dependency of Inout
from From. *) from From. *)
Db.From.find_deps_no_transitivity_state := Db.From.find_deps_no_transitivity_state :=
(fun s e -> (fun s e -> Eva.Results.(in_cvalue_state s |> expr_deps e));
let deps = From_compute.find_deps_no_transitivity s e in
Function_Froms.Deps.to_zone deps);
ignore ( ignore (
Db.register_compute "From.compute_all" Db.register_compute "From.compute_all"
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment