diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 753a55e2ec41196fe602d53a700ab1123f7a33c4..2df5d4aedad3b67e35165bd7e03b9c2fe25217ae 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -993,5 +993,11 @@ module Annot: sig
      {!generated} emitter. They are all assigned a valid status by
      {!Analysis.emitter}.
   *)
-  val generator : unit -> Cil.cilVisitor
+  val generator : unit -> Visitor.frama_c_inplace
+
+  (**
+     Creates a visitor that can be used to remove all generated annotations from
+     {!generated} emitter. This will also remove their associated status.
+  *)
+  val cleaner : unit -> Visitor.frama_c_inplace
 end
diff --git a/src/plugins/eva/parameters.ml b/src/plugins/eva/parameters.ml
index 620f41b7048a09259677e0dc978cbb3e3e18c919..c706df45822af3e5c932b69e93aeaf20deefc685 100644
--- a/src/plugins/eva/parameters.ml
+++ b/src/plugins/eva/parameters.ml
@@ -1276,6 +1276,21 @@ module MallocLevel =
 let () = MallocLevel.set_range ~min:0 ~max:max_int
 let () = add_precision_dep MallocLevel.parameter
 
+(* -------------------------------------------------------------------------- *)
+(* --- Annotations Generator options                                      --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Annot =
+  Kernel_function_set
+    (struct
+      let option_name = "-eva-annot"
+      let arg_name = "f"
+      let help =
+        "Populate the specified functions with assertions \
+         representing the range of values computed by Eva \
+         on l-values read by the code, when available."
+    end)
+
 (* -------------------------------------------------------------------------- *)
 (* --- Deprecated options and aliases                                     --- *)
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/eva/parameters.mli b/src/plugins/eva/parameters.mli
index 90225279e4400d667c0f54230dc4301fff40a4e9..d43eed6b23cd8aae3d6ede54f717e060c989464e 100644
--- a/src/plugins/eva/parameters.mli
+++ b/src/plugins/eva/parameters.mli
@@ -170,6 +170,10 @@ val register_builtin: string -> unit
 (** Registers available domain names for the -eva-domains option. *)
 val register_domain: name:string -> descr:string -> unit
 
+(** Annotation Generator *)
+
+module Annot: Parameter_sig.Kernel_function_set
+
 [@@@ api_start]
 
 (** Configuration of the analysis. *)
diff --git a/src/plugins/eva/utils/annot.ml b/src/plugins/eva/utils/annot.ml
index c9901a5a86fb225c6fdfc474c035f6988e3c7c4f..b89c06cc110f6a73be3fc057c658af466418bbd8 100644
--- a/src/plugins/eva/utils/annot.ml
+++ b/src/plugins/eva/utils/annot.ml
@@ -28,6 +28,7 @@ open Cil_types
 
 module Ltype = Cil_datatype.Logic_type_ByName
 module Exp = Cil_builder.Exp
+type visitor = Visitor.frama_c_visitor
 
 type pred =
   | True
@@ -166,7 +167,7 @@ module Slv = Cil_datatype.LvalStructEq.Set
 
 class evaluator request =
   object(self)
-    inherit Visitor.generic_frama_c_visitor (Visitor_behavior.inplace ())
+    inherit Visitor.frama_c_inplace
 
     val mutable locked = Slv.empty
     val mutable domain : pred list = []
@@ -240,7 +241,7 @@ let eval_instr ?callstack ?name stmt =
     | None -> r
     | Some c -> Results.in_callstack c r in
   let engine = new evaluator request in
-  let _ = Cil.visitCilStmt (engine :> Cil.cilVisitor) stmt in
+  let _ = Visitor.visitFramacStmt (engine :> visitor) stmt in
   List.map (predicate ?name ~loc:(Cil_datatype.Stmt.loc stmt)) engine#flush
 
 (* -------------------------------------------------------------------------- *)
@@ -254,7 +255,7 @@ let generated = Emitter.create "Eva_domain"
 
 class generator =
   object(self)
-    inherit Visitor.generic_frama_c_visitor (Visitor_behavior.inplace ())
+    inherit Visitor.frama_c_inplace
 
     method! vlval _ = SkipChildren
     method! vexpr _ = SkipChildren
@@ -278,6 +279,56 @@ class generator =
 
   end
 
-let generator () = (new generator :> Cil.cilVisitor)
+let generator () = (new generator :> visitor)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Annotation Removal                                                 --- *)
+(* -------------------------------------------------------------------------- *)
+
+class cleaner =
+  object(self)
+    inherit Visitor.frama_c_inplace
+
+    method! vlval _ = SkipChildren
+    method! vexpr _ = SkipChildren
+
+    method !vstmt_aux stmt =
+      match self#current_kf with
+      | None -> Cil.SkipChildren
+      | Some kf ->
+        Annotations.iter_code_annot
+          (fun e ca ->
+             if Emitter.equal e generated then
+               Annotations.remove_code_annot e ~kf stmt ca
+          ) stmt ;
+        DoChildren
+
+  end
+
+let cleaner () = (new cleaner :> visitor)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Command Line Option                                                --- *)
+(* -------------------------------------------------------------------------- *)
+
+let main () =
+  if Analysis.is_computed () then
+    let ast = Ast.get () in
+    let cleaner = cleaner () in
+    Self.feedback ~ontty:`Transient "Cleaning annotations..." ;
+    Visitor.visitFramacFile cleaner ast ;
+    let generator = new generator in
+    Parameters.Annot.iter
+      begin fun kf ->
+        if Kernel_function.has_definition kf then
+          let fundec = Kernel_function.get_definition kf in
+          Self.feedback "Annotate %a" Kernel_function.pretty kf ;
+          ignore @@ Visitor.visitFramacFunction generator fundec
+        else
+          Self.warning "Can not annotate %a (no definition)"
+            Kernel_function.pretty kf ;
+      end
+
+let () = Boot.Main.extend main
 
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/eva/utils/annot.mli b/src/plugins/eva/utils/annot.mli
index 119055ac51596987847407451b672abe5937c253..2b322a32a0c04e381665d6d1ebbdcd4c97d68551 100644
--- a/src/plugins/eva/utils/annot.mli
+++ b/src/plugins/eva/utils/annot.mli
@@ -53,7 +53,13 @@ val generated : Emitter.t
    {!generated} emitter. They are all assigned a valid status by
    {!Analysis.emitter}.
 *)
-val generator : unit -> Cil.cilVisitor
+val generator : unit -> Visitor.frama_c_inplace
+
+(**
+   Creates a visitor that can be used to remove all generated annotations from
+   {!generated} emitter. This will also remove their associated status.
+*)
+val cleaner : unit -> Visitor.frama_c_inplace
 
 [@@@ api_end]