[Eva] api: Add dependencies calculus

src/plugins/value/Eva.mli

@@ -68,6 +68,10 @@ module Results: sig
   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
+  
   (* Evaluation *)
   val eval_var : Cil_types.varinfo -> request -> value evaluation
   val eval_lval : Cil_types.lval -> request -> value evaluation

src/plugins/value/register.mli

@@ -20,6 +20,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** Functions of the Value plugin registered in {!Db}.
+(** Functions of the Value plugin registered in {!Db}. Only two functions
+    are exported. *)
 
-    Nothing is 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

src/plugins/value/utils/results.ml

@@ -357,7 +357,7 @@ struct
 
   (* Evaluation *)
 
-  let eval_lval lval req=
+  let eval_lval lval req =
     let eval state = A.Eval.copy_lvalue state lval in
     LValue (Response.map eval (get req))
 
@@ -486,6 +486,22 @@ struct
     match r with
     | `Bottom -> true
     | `Top | `Value () -> false
+
+  (* Dependencies *)
+
+  let lval_deps lval req =
+    let compute_deps cvalue =
+      Register.eval_deps_lval (cvalue, Locals_scoping.bottom ()) lval
+    in
+    req |> as_cvalue_model |>
+    Result.fold ~error:(fun _ -> Locations.Zone.bottom) ~ok:compute_deps
+
+  let expr_deps exp req =
+    let compute_deps cvalue =
+      Register.eval_deps (cvalue, Locals_scoping.bottom ()) exp
+    in
+    req |> as_cvalue_model |>
+    Result.fold ~error:(fun _ -> Locations.Zone.bottom) ~ok:compute_deps
 end
 
 
@@ -519,6 +535,17 @@ let as_cvalue_model req =
   E.as_cvalue_model req
 
 
+(* Depedencies *)
+
+let expr_deps exp req =
+  let module E = Make () in
+  E.expr_deps exp req
+
+let lval_deps lval req =
+  let module E = Make () in
+  E.lval_deps lval req
+
+
 (* Evaluation *)
 
 module type Lvaluation =

src/plugins/value/utils/results.mli

@@ -71,6 +71,10 @@ val fold_callstacks : (callstack -> request -> 'a -> 'a) -> 'a -> request -> 'a
 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
+
 (* Evaluation *)
 val eval_var : Cil_types.varinfo -> request -> value evaluation
 val eval_lval : Cil_types.lval -> request -> value evaluation