[Eva] rename API functions

src/plugins/eva/Eva.mli

@@ -969,7 +969,7 @@ module Export: sig
   (* -------------------------------------------------------------------------- *)
 
   (** Generates a predicate characterizing the domain of the l-value. *)
-  val eval_value :
+  val export_value :
     loc:location -> ?name:string list -> lval -> Results.request -> predicate
 
   (**
@@ -981,7 +981,7 @@ module Export: sig
      left-hand-side are not visited, but their inner l-values are visited; any
      l-value from the right-hand-side of the instruction is also visited.
   *)
-  val eval_instr :
+  val export_stmt :
     ?callstack:Callstack.t -> ?name:string list -> stmt -> predicate list
 
   (** Emitter used for generating domain assertions. *)

src/plugins/eva/utils/export.ml

@@ -161,7 +161,7 @@ let domain lv value =
 (* --- Evalutation                                                        --- *)
 (* -------------------------------------------------------------------------- *)
 
-let eval_value ~loc ?name lv request =
+let export_value ~loc ?name lv request =
   Results.eval_lval lv request
   |> domain lv
   |> predicate ?name ~loc
@@ -233,7 +233,7 @@ let collect stmt =
   end ;
   acc#flush
 
-let eval_instr ?callstack ?name stmt =
+let export_stmt ?callstack ?name stmt =
   let request =
     let r = Results.before stmt in
     match callstack with
@@ -274,7 +274,7 @@ let generator () : visitor =
           begin
             List.iter
               (Annotations.add_assert emitter ~kf stmt)
-              (eval_instr stmt) ;
+              (export_stmt stmt) ;
             Annotations.iter_code_annot
               (fun e ca ->
                  if Emitter.equal e emitter then

src/plugins/eva/utils/export.mli

@@ -29,7 +29,7 @@ open Cil_types
 (* -------------------------------------------------------------------------- *)
 
 (** Generates a predicate characterizing the domain of the l-value. *)
-val eval_value :
+val export_value :
   loc:location -> ?name:string list -> lval -> Results.request -> predicate
 
 (**
@@ -41,7 +41,7 @@ val eval_value :
    left-hand-side are not visited, but their inner l-values are visited; any
    l-value from the right-hand-side of the instruction is also visited.
 *)
-val eval_instr :
+val export_stmt :
   ?callstack:Callstack.t -> ?name:string list -> stmt -> predicate list
 
 (** Emitter used for generating domain assertions. *)