[Eva] api: separate lval_deps and address_deps

src/plugins/value/Eva.mli

@@ -70,8 +70,9 @@ module Results: sig
   val as_cvalue_model : request -> Cvalue.Model.t result
   
   (* Dependencies *)
-  val expr_deps : Cil_types.exp -> request -> Locations.Zone.t
-  val lval_deps : Cil_types.lval -> request -> Locations.Zone.t
+  val expr_deps : Cil_types.exp -> request -> Locations.Zone.t (* The zone of bits read to evaluate the expression, including adresses computation *)
+  val lval_deps : Cil_types.lval -> request -> Locations.Zone.t (* The zone of bits read to evaluate the lvalue, including lvalue zone itself *)
+  val address_deps : Cil_types.lval -> request -> Locations.Zone.t (* The zone of bits read to evaluate the lvalue, excluding the lvalue zone itself *)
   
   (* Evaluation *)
   val eval_var : Cil_types.varinfo -> request -> value evaluation

src/plugins/value/register.mli

@@ -23,7 +23,6 @@
 (** Functions of the Value plugin registered in {!Db}. Only two functions
     are exported. *)
 
-val eval_deps : Cvalue.Model.t * Locals_scoping.clobbered_set ->
-  Cil_types.exp -> Locations.Zone.t
-val eval_deps_lval : Cvalue.Model.t * Locals_scoping.clobbered_set ->
-  Cil_types.lval -> Locations.Zone.t
+val eval_deps : Cvalue_domain.State.t -> Cil_types.exp -> Locations.Zone.t
+val eval_deps_lval : Cvalue_domain.State.t -> Cil_types.lval -> Locations.Zone.t
+val eval_deps_addr : Cvalue_domain.State.t -> Cil_types.lval -> Locations.Zone.t

src/plugins/value/utils/results.ml

@@ -511,6 +511,14 @@ struct
     in
     req |> as_cvalue_model |>
     Result.fold ~error:(fun _ -> Locations.Zone.bottom) ~ok:compute_deps
+
+  let address_deps lval req =
+    let compute_deps cvalue =
+      Register.eval_deps_addr (cvalue, Locals_scoping.bottom ()) lval
+    in
+    req |> as_cvalue_model |>
+    Result.fold ~error:(fun _ -> Locations.Zone.bottom) ~ok:compute_deps
+
 end
 
 
@@ -554,6 +562,10 @@ let lval_deps lval req =
   let module E = Make () in
   E.lval_deps lval req
 
+let address_deps lval req =
+  let module E = Make () in
+  E.address_deps lval req
+
 
 (* Evaluation *)
 

src/plugins/value/utils/results.mli

@@ -72,8 +72,9 @@ val equality_class : Cil_types.exp -> request -> Cil_types.exp list result
 val as_cvalue_model : request -> Cvalue.Model.t result
 
 (* Dependencies *)
-val expr_deps : Cil_types.exp -> request -> Locations.Zone.t
-val lval_deps : Cil_types.lval -> request -> Locations.Zone.t
+val expr_deps : Cil_types.exp -> request -> Locations.Zone.t (* The zone of bits read to evaluate the expression, including adresses computation *)
+val lval_deps : Cil_types.lval -> request -> Locations.Zone.t (* The zone of bits read to evaluate the lvalue, including lvalue zone itself *)
+val address_deps : Cil_types.lval -> request -> Locations.Zone.t (* The zone of bits read to evaluate the lvalue, excluding the lvalue zone itself *)
 
 (* Evaluation *)
 val eval_var : Cil_types.varinfo -> request -> value evaluation