[Eva] add Deps to the public API

src/plugins/eva/Eva.mli

@@ -178,6 +178,47 @@ module Callstack: sig
 
 end
 
+module Deps: sig
+
+  (** Memory dependencies of an expression. *)
+  type t = Function_Froms.Deps.deps = {
+    data: Locations.Zone.t;
+    (** Memory zone directly required to evaluate the given expression. *)
+    indirect: Locations.Zone.t;
+    (** Memory zone read to compute data addresses. *)
+  }
+
+  include Datatype.S with type t := t
+
+  val pretty_debug: Format.formatter -> t -> unit
+
+  (* Constructors *)
+
+  val top : t
+  val bottom : t
+  val data : Locations.Zone.t -> t
+  val indirect : Locations.Zone.t -> t
+
+  (* Conversion *)
+
+  val to_zone : t -> Locations.Zone.t
+
+  (* Mutators *)
+
+  val add_data : t -> Locations.Zone.t -> t
+  val add_indirect : t -> Locations.Zone.t -> t
+
+  (* Map *)
+
+  val map : (Locations.Zone.t -> Locations.Zone.t) -> t -> t
+
+  (* Lattice operators *)
+
+  val is_included : t -> t -> bool
+  val join : t -> t -> t
+  val narrow : t -> t -> t
+end
+
 module Results: sig
 
   (** Eva's result API is a new interface to access the results of an analysis,
@@ -335,14 +376,6 @@ module Results: sig
       evaluate the given lvalue, excluding the lvalue zone itself. *)
   val address_deps : Cil_types.lval -> request -> Locations.Zone.t
 
-  (** Memory dependencies of an expression. *)
-  type deps = Function_Froms.Deps.deps = {
-    data: Locations.Zone.t;
-    (** Memory zone directly required to evaluate the given expression. *)
-    indirect: Locations.Zone.t;
-    (** Memory zone read to compute data addresses. *)
-  }
-
   (** Taint of a memory zone, according to the taint domain. *)
   type taint =
     | Direct
@@ -361,7 +394,7 @@ module Results: sig
 
   (** Computes (an overapproximation of) the memory dependencies of an
       expression. *)
-  val expr_dependencies : Cil_types.exp -> request -> deps
+  val expr_dependencies : Cil_types.exp -> request -> Deps.t
 
   (** Evaluation *)
 

src/plugins/eva/api/general_requests.ml

@@ -327,7 +327,7 @@ module EvaTaints = struct
 
   let evaluate expr request =
     let (let+) = Option.bind in
-    let { data ; indirect } = expr_dependencies expr request in
+    let Deps.{ data ; indirect } = expr_dependencies expr request in
     let+ data = is_tainted data request |> Result.to_option in
     let+ indirect = is_tainted indirect request |> Result.to_option in
     Some (data, indirect)

src/plugins/eva/dune

@@ -112,7 +112,7 @@
  (mode (promote (only Eva.mli)))
  (deps
   gen-api.sh Eva.header
-  engine/analysis.mli types/callstack.mli utils/results.mli parameters.mli
+  engine/analysis.mli types/callstack.mli types/deps.mli utils/results.mli parameters.mli
   utils/eva_annotations.mli eval.mli domains/cvalue/builtins.mli
   utils/cvalue_callbacks.mli legacy/logic_inout.mli utils/eva_results.mli
   utils/unit_tests.mli)

src/plugins/eva/types/deps.mli

@@ -20,6 +20,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+[@@@ api_start]
+
 (** Memory dependencies of an expression. *)
 type t = Function_Froms.Deps.deps = {
   data: Locations.Zone.t;
@@ -57,3 +59,4 @@ val map : (Locations.Zone.t -> Locations.Zone.t) -> t -> t
 val is_included : t -> t -> bool
 val join : t -> t -> t
 val narrow : t -> t -> t
+[@@@ api_end]

src/plugins/eva/utils/results.ml

@@ -733,11 +733,6 @@ let address_deps lval request =
   let lval_to_loc lv = eval_address lv request |> as_precise_loc in
   Eva_utils.indirect_zone_of_lval lval_to_loc lval
 
-type deps = Function_Froms.Deps.deps = {
-  data: Locations.Zone.t;
-  indirect: Locations.Zone.t;
-}
-
 let expr_dependencies expr request =
   let lval_to_loc lv = eval_address lv request |> as_precise_loc in
   Eva_utils.deps_of_expr lval_to_loc expr

src/plugins/eva/utils/results.mli

@@ -177,14 +177,6 @@ val lval_deps : Cil_types.lval -> request -> Locations.Zone.t
     evaluate the given lvalue, excluding the lvalue zone itself. *)
 val address_deps : Cil_types.lval -> request -> Locations.Zone.t
 
-(** Memory dependencies of an expression. *)
-type deps = Function_Froms.Deps.deps = {
-  data: Locations.Zone.t;
-  (** Memory zone directly required to evaluate the given expression. *)
-  indirect: Locations.Zone.t;
-  (** Memory zone read to compute data addresses. *)
-}
-
 (** Taint of a memory zone, according to the taint domain. *)
 type taint =
   | Direct
@@ -203,7 +195,7 @@ val is_tainted : Locations.Zone.t -> request -> (taint, error) Result.t
 
 (** Computes (an overapproximation of) the memory dependencies of an
     expression. *)
-val expr_dependencies : Cil_types.exp -> request -> deps
+val expr_dependencies : Cil_types.exp -> request -> Deps.t
 
 (** Evaluation *)