diff --git a/src/plugins/slicing/fct_slice.ml b/src/plugins/slicing/fct_slice.ml index 8668de2d3271d908e306ba63930708f0bc71bc7e..22285f900b9f9a04bf5aa331cdbef9bd32c215b2 100644 --- a/src/plugins/slicing/fct_slice.ml +++ b/src/plugins/slicing/fct_slice.ml @@ -54,9 +54,7 @@ let exists_fun_callers fpred kf = then false (* no way to call the initial [kf]. *) else begin table := Kernel_function.Set.add kf !table ; - List.exists - (fun kf -> exists_fun_callers kf) - (Eva.Results.callers kf) + List.exists exists_fun_callers (Eva.Results.callers kf) end in exists_fun_callers kf @@ -1454,12 +1452,11 @@ let merge_fun_callers get_list get_value merge is_top acc kf = raise StopMerging (* acceleration when top is reached *) in let rec merge_fun_callers kf = - let merge_fun_caller kf = merge_fun_callers kf in let vf = Kernel_function.get_vi kf in if not (Cil_datatype.Varinfo.Set.mem vf !table) then begin table := Cil_datatype.Varinfo.Set.add vf !table ; List.iter (fun x -> merge (get_value x)) (get_list kf) ; - List.iter merge_fun_caller (Eva.Results.callers kf) + List.iter merge_fun_callers (Eva.Results.callers kf) end (* else no way to add something, the [kf] contribution is already accumulated. *) diff --git a/src/plugins/slicing/slicingCmds.ml b/src/plugins/slicing/slicingCmds.ml index dfd6377fa2ec09a694c177155f960e226efdc84c..cdfb8be1be922c17ed06c8e95349136ae6d1fcfe 100644 --- a/src/plugins/slicing/slicingCmds.ml +++ b/src/plugins/slicing/slicingCmds.ml @@ -55,6 +55,11 @@ let apply_all ~propagate_to_callers = let get_select_kf (fvar, _select) = Globals.Functions.get fvar +let get_lval_zone ?(access=Locations.Read) stmt lval = + let open Eva.Results in + before stmt |> eval_address lval |> as_zone ~access + |> default Locations.Zone.bottom + (** Utilities for [kinstr]. *) module Kinstr: sig val iter_from_func : (stmt -> unit) -> kernel_function -> unit @@ -76,12 +81,8 @@ struct (* returns [read_zone] joined to [Zone.t read] by [lv], [Zone.t written] by [lv] *) (* The modified locations are [looking_for], those address are function of [deps]. *) - let zloc, deps = - Eva.Results.( - before stmt |> eval_address lv |> as_zone ~access:Locations.Write |> - default Locations.Zone.bottom, - before stmt |> address_deps lv) - in + let zloc = get_lval_zone ~access:Locations.Write stmt lv in + let deps = Eva.Results.(before stmt |> address_deps lv) in Locations.Zone.join read_zone deps, zloc in let call_process lv f args _loc = @@ -320,10 +321,7 @@ let select_stmt_lval set mark lval_str ~before ki ~eval kf = let lval = !Db.Properties.Interp.term_lval_to_lval ~result:None lval_term in - let zone = - Eva.Results.(before eval |> eval_address lval |> as_zone) |> - Result.value ~default:Locations.Zone.bottom - in + let zone = get_lval_zone eval lval in Locations.Zone.join zone acc) lval_str Locations.Zone.bottom @@ -353,10 +351,7 @@ let select_lval_rw set mark ~rd ~wr ~eval kf ki_opt= let lval_term = !Db.Properties.Interp.term_lval kf lval_str in let lval = !Db.Properties.Interp.term_lval_to_lval ~result:None lval_term in let access = if for_writing then Locations.Write else Locations.Read in - let zone = - Eva.Results.(before eval |> eval_address lval |> as_zone ~access) |> - Result.value ~default:Locations.Zone.bottom - in + let zone = get_lval_zone ~access eval lval in Locations.Zone.join zone acc) lval_str Locations.Zone.bottom in SlicingParameters.debug ~level:3