diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index ca1f2879aeaeb5d6adecd151bc330a36f6c49ac1..25d2834bf98632ebd688e1fb7cbe8d612e971784 100644
--- a/src/plugins/eva/Eva.mli
+++ b/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. *)
diff --git a/src/plugins/eva/utils/export.ml b/src/plugins/eva/utils/export.ml
index 835437c7dee9cd524ce089d3ac8a65cd454a9baf..7b5595771ce120eb8c83db5c41c83c123eb8a844 100644
--- a/src/plugins/eva/utils/export.ml
+++ b/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
diff --git a/src/plugins/eva/utils/export.mli b/src/plugins/eva/utils/export.mli
index 0bcb54409da260228cefd5d934dcccf090753237..574bf6e432965f7153cb2329a300ec2b82400da9 100644
--- a/src/plugins/eva/utils/export.mli
+++ b/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. *)