diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index c31bf449d10e3ee411955db686833d98de9eb008..54301eebc1876625fdaf2c5f2e0d1576f159b570 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -382,15 +382,8 @@ module Logic_scope = struct
     else env
 end
 
-let emitter =
-  Emitter.create
-    "E_ACSL"
-    [ Emitter.Code_annot; Emitter.Funspec ]
-    ~correctness:[ Options.Gmp_only.parameter ]
-    ~tuning:[]
-
 let add_assert kf stmt annot =
-  Annotations.add_assert emitter ~kf stmt annot
+  Annotations.add_assert Options.emitter ~kf stmt annot
 
 let add_stmt ?(post=false) ?before env kf stmt =
   if not post then
diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli
index cd2719f04b2b8de1b1570229af92694fb98f4e59..9369474926d88b06dee38f1e0df23ee1bf5d1de7 100644
--- a/src/plugins/e-acsl/src/code_generator/env.mli
+++ b/src/plugins/e-acsl/src/code_generator/env.mli
@@ -190,8 +190,6 @@ val with_rte_and_result: f:(t -> 'a * t) -> t -> bool -> 'a * t
     This function does not handle exceptions at all. The user must handle them
     either directly in the [f] closure or around the call to the function. *)
 
-val emitter : Emitter.t
-
 module Local_vars: sig
   val push_new: t -> t
   val add: t -> Typing.number_ty -> t
diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
index ac7efd77e4b73037de041e75cacde0631cb07e44..2d60e2c9f17d740a719ba62e8ff9e7d00f9370bf 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -193,7 +193,7 @@ let generate_kf ~loc fname env ret_ty params_ty li =
   Globals.Functions.replace_by_definition spec fundec loc;
   (* create the kernel function itself *)
   let kf = Globals.Functions.get fundec.svar in
-  Annotations.register_funspec ~emitter:Env.emitter kf;
+  Annotations.register_funspec ~emitter:Options.emitter kf;
   (* closure generating the function's body.
      Delay its generation after filling the memoisation table (for termination
      of recursive function calls) *)
@@ -254,7 +254,7 @@ let generate_kf ~loc fname env ret_ty params_ty li =
     in
     Annotations.add_assigns
       ~keep_empty:false
-      Env.emitter
+      Options.emitter
       ~behavior:Cil.default_behavior_name
       kf
       (Writes [ assigned_var , From deps]);
diff --git a/src/plugins/e-acsl/src/options.ml b/src/plugins/e-acsl/src/options.ml
index 2b4558e81c17b76b6169c793ceea295da0ce776a..024e4ca438931873788cdbb096d8fed8dde42eba 100644
--- a/src/plugins/e-acsl/src/options.ml
+++ b/src/plugins/e-acsl/src/options.ml
@@ -158,7 +158,16 @@ let parameter_states =
     Functions.self;
     Instrument.self ]
 
-let emitter = Emitter.create "E-ACSL" [ Funspec ] ~correctness:[] ~tuning:[]
+let emitter =
+  Emitter.create
+    "E_ACSL"
+    [ Emitter.Code_annot; Emitter.Funspec ]
+    ~correctness:[ Functions.parameter;
+                   Instrument.parameter;
+                   Validate_format_strings.parameter ]
+    ~tuning:[ Gmp_only.parameter;
+              Valid.parameter;
+              Replace_libc_functions.parameter ]
 
 let must_visit () = Run.get ()