[Slicing] Minor simplifications in the use of Eva results.

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. *)

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