[Eva] Simplifies the exported interface of Eval_terms.

Changes the Inout plugin accordingly.

src/plugins/inout/operational_inputs.ml

@@ -374,26 +374,18 @@ module Computer(Fenv:Dataflows.FUNCTION_ENV)(X:sig
          | AAssert (_, p)
          | AInvariant (_, true, p) ->
            begin
-             let env =
-               Eva.Eval_terms.env_annot
-                 ~pre:X.kf_pre_state
-                 ~here:(X.stmt_state stmt)
-                 ()
+             let pre = X.kf_pre_state
+             and here = X.stmt_state stmt in
+             let deps =
+               Eva.Eval_terms.annot_predicate_deps ~pre ~here p.tp_statement
              in
-             match Eva.Eval_terms.predicate_deps env p.tp_statement with
+             match deps with
              | None ->
                (* To be sound, we should perform a join with the top zone here.
                   We do nothing instead because the latter behavior would
                   directly disable memexec. *)
                ()
-             | Some logic_deps ->
-               let p_zone =
-                 Cil_datatype.Logic_label.Map.fold
-                   (fun _ -> Zone.join)
-                   logic_deps
-                   Zone.bottom
-               in
-               store_non_terminating_logic_inputs p_zone
+             | Some p_zone -> store_non_terminating_logic_inputs p_zone
            end
          | _ -> ())
       stmt

src/plugins/value/Eva.mli

@@ -268,20 +268,13 @@ module Value_parameters: sig
 end
 
 module Eval_terms: sig
-  type labels_states = Cvalue.Model.t Cil_datatype.Logic_label.Map.t
-
-  (** Evaluation environment. Currently available are function Pre and Post, or
-      the environment to evaluate an annotation *)
-  type eval_env
-  val env_annot :
-    ?c_labels:labels_states -> pre:Cvalue.Model.t -> here:Cvalue.Model.t ->
-    unit -> eval_env
-  (** Dependencies needed to evaluate a term or a predicate *)
-  type logic_deps = Locations.Zone.t Cil_datatype.Logic_label.Map.t
-  (** [predicate_deps env p] computes the logic dependencies needed to evaluate
-      [p] in the given evaluation environment [env].
-      @return None on either an evaluation error or on unsupported construct. *)
-  val predicate_deps: eval_env -> Cil_types.predicate -> logic_deps option
+  (** [annot_predicate_deps ~pre ~here p] computes the logic dependencies needed
+      to evaluate the predicate [p] in a code annotation in cvalue state [here],
+      in a function whose pre-state is [pre].
+      Returns None on either an evaluation error or on unsupported construct. *)
+  val annot_predicate_deps:
+    pre:Cvalue.Model.t -> here:Cvalue.Model.t ->
+    Cil_types.predicate -> Locations.Zone.t option
 end
 
 module Unit_tests: sig

src/plugins/value/legacy/eval_terms.ml

@@ -2745,6 +2745,16 @@ and predicate_deps env pred =
   try Some (do_eval env pred)
   with LogicEvalError _ -> None
 
+let annot_predicate_deps ~pre ~here predicate =
+  let env = env_annot ~pre ~here () in
+  let logic_deps = predicate_deps env predicate in
+  let join logic_deps =
+    Cil_datatype.Logic_label.Map.fold
+      (fun _ -> Locations.Zone.join)
+      logic_deps
+      Locations.Zone.bottom
+  in
+  Option.map join logic_deps
 
 (* -------------------------------------------------------------------------- *)
 (* --- Export                                                             --- *)

src/plugins/value/legacy/eval_terms.mli

@@ -49,22 +49,18 @@ val pretty_logic_evaluation_error :
 
 exception LogicEvalError of logic_evaluation_error
 
-[@@@ api_start]
 type labels_states = Cvalue.Model.t Cil_datatype.Logic_label.Map.t
 
 (** Evaluation environment. Currently available are function Pre and Post, or
-    the environment to evaluate an annotation *)
+    the environment to evaluate an annotation. *)
 type eval_env
-[@@@ api_end]
 
 val make_env: Model.t Abstract_domain.logic_environment -> Model.t -> eval_env
 
 val env_pre_f : pre:Model.t -> unit -> eval_env
-[@@@ api_start]
 val env_annot :
   ?c_labels:labels_states -> pre:Cvalue.Model.t -> here:Cvalue.Model.t ->
   unit -> eval_env
-[@@@ api_end]
 val env_post_f :
   ?c_labels:labels_states -> pre:Model.t -> post:Model.t ->
   result:varinfo option -> unit -> eval_env
@@ -75,10 +71,8 @@ val env_only_here: Model.t -> eval_env
 
 val env_current_state: eval_env -> Model.t
 
-[@@@ api_start]
 (** Dependencies needed to evaluate a term or a predicate *)
 type logic_deps = Locations.Zone.t Cil_datatype.Logic_label.Map.t
-[@@@ api_end]
 
 (** Three modes to handle the alarms when evaluating a logical term. *)
 type alarm_mode =
@@ -117,12 +111,22 @@ val eval_tlval_as_zone :
 val eval_predicate :
   eval_env -> predicate -> predicate_status
 
-[@@@ api_start]
 (** [predicate_deps env p] computes the logic dependencies needed to evaluate
     [p] in the given evaluation environment [env].
-    @return None on either an evaluation error or on unsupported construct. *)
+    Returns None on either an evaluation error or on unsupported construct. *)
 val predicate_deps: eval_env -> Cil_types.predicate -> logic_deps option
-[@@@ api_end]
 
 val reduce_by_predicate :
   eval_env -> bool -> predicate -> eval_env
+
+
+
+[@@@ api_start]
+(** [annot_predicate_deps ~pre ~here p] computes the logic dependencies needed
+    to evaluate the predicate [p] in a code annotation in cvalue state [here],
+    in a function whose pre-state is [pre].
+    Returns None on either an evaluation error or on unsupported construct. *)
+val annot_predicate_deps:
+  pre:Cvalue.Model.t -> here:Cvalue.Model.t ->
+  Cil_types.predicate -> Locations.Zone.t option
+[@@@ api_end]