diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index 6bff15e6b264e8bf6cdf6da1dc6495455eb4aeed..7fdc8f1b60197e450b134a4f2fbabcb596c46c79 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -183,7 +183,7 @@
       ];
     List.iter (fun (x, y) -> Hashtbl.add type_kw x y)
       ["integer", INTEGER; "real", REAL; "boolean", BOOLEAN; ];
-    (fun s loc ->
+    (fun ~plugin s loc ->
       try
         (Hashtbl.find all_kw s)
         loc
@@ -191,14 +191,14 @@
         let res =
           match Logic_env.extension_category s with
           | exception Not_found -> None
-          | Cil_types.Ext_contract -> Some (EXT_CONTRACT s)
+          | Cil_types.Ext_contract -> Some (EXT_CONTRACT (s, plugin))
           | Cil_types.Ext_global ->
             begin
               match Logic_env.is_extension_block s with
-              | false -> Some (EXT_GLOBAL s)
-              | true -> Some (EXT_GLOBAL_BLOCK s)
+              | false -> Some (EXT_GLOBAL (s, plugin))
+              | true -> Some (EXT_GLOBAL_BLOCK (s, plugin))
             end
-          | Cil_types.Ext_code_annot _ -> Some (EXT_CODE_ANNOT s)
+          | Cil_types.Ext_code_annot _ -> Some (EXT_CODE_ANNOT (s, plugin))
         in
         match res with
         | None ->
@@ -315,10 +315,10 @@
         Kernel.warning ~once:true ~wkey:Kernel.wkey_plugin_not_loaded ~source
           "Ignoring extension '%s' for unloaded plug-in %s" s plugin;
       IDENTIFIER_EXT s
-    | EXT_CODE_ANNOT s
-    | EXT_GLOBAL s
-    | EXT_GLOBAL_BLOCK s
-    | EXT_CONTRACT s ->
+    | EXT_CODE_ANNOT (s, _)
+    | EXT_GLOBAL (s, _)
+    | EXT_GLOBAL_BLOCK (s, _)
+    | EXT_CONTRACT (s, _) ->
       let plugin_from = Logic_env.extension_from s in
       if plugin_from = plugin && plugin = "kernel" then
         Kernel.abort ~source
@@ -379,7 +379,7 @@ rule token = parse
   | '\\' (rIdentifier as plugin) "::" (rIdentifier as name) {
      let loc = Lexing.(lexeme_start_p lexbuf, lexeme_end_p lexbuf) in
      let cabsloc = Cil_datatype.Location.of_lexing_loc loc in
-     let tok = identifier name cabsloc in
+     let tok = identifier ~plugin:(Some plugin) name cabsloc in
      check_ext_plugin (fst cabsloc) plugin tok
      }
   | '\\' rIdentifier { bs_identifier lexbuf }
@@ -389,7 +389,7 @@ rule token = parse
       let loc = Lexing.(lexeme_start_p lexbuf, lexeme_end_p lexbuf) in
       let cabsloc = Cil_datatype.Location.of_lexing_loc loc in
       let s = lexeme lexbuf in
-      let curr_tok = identifier s cabsloc in
+      let curr_tok = identifier ~plugin:None s cabsloc in
       if curr_tok = CHECK || curr_tok = ADMIT then begin
         let next_tok =
           token { lexbuf with refill_buff = lexbuf.refill_buff }
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index ce9c3e2bedab3ff85e5b869b53f5050a32189c99..b45a800a8afa03bcb0ed21d4f8966e50d10e0eea 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -290,7 +290,7 @@
 %token CHECK_ENSURES CHECK_EXITS CHECK_CONTINUES CHECK_BREAKS CHECK_RETURNS
 %token ADMIT_REQUIRES ADMIT_LOOP ADMIT_INVARIANT ADMIT_LEMMA
 %token ADMIT_ENSURES ADMIT_EXITS ADMIT_CONTINUES ADMIT_BREAKS ADMIT_RETURNS
-%token <string> EXT_CODE_ANNOT EXT_GLOBAL EXT_GLOBAL_BLOCK EXT_CONTRACT
+%token <string * string option> EXT_CODE_ANNOT EXT_GLOBAL EXT_GLOBAL_BLOCK EXT_CONTRACT
 %token EXITS BREAKS CONTINUES RETURNS
 %token VOLATILE READS WRITES
 %token LOGIC PREDICATE INDUCTIVE AXIOM LEMMA LBRACE RBRACE
@@ -948,10 +948,10 @@ full_identifier:
 | EXT_SPEC_INCLUDE { "include" }
 | EXT_SPEC_AT { "at" }
 | EXT_SPEC_LET { "let" }
-| id = EXT_CODE_ANNOT { id }
-| id = EXT_CONTRACT { id }
-| id = EXT_GLOBAL { id }
-| id = EXT_GLOBAL_BLOCK { id }
+| id = EXT_CODE_ANNOT { fst id }
+| id = EXT_CONTRACT { fst id }
+| id = EXT_GLOBAL { fst id }
+| id = EXT_GLOBAL_BLOCK { fst id }
 | id = IDENTIFIER_EXT { id }
 ;
 
@@ -1181,7 +1181,7 @@ clause_kw:
 | FREES {"frees"}
 | COMPLETE {"complete"}
 | DISJOINT {"disjoint"}
-| EXT_CONTRACT { $1 }
+| EXT_CONTRACT { fst $1 }
 | id=IDENTIFIER_EXT { id }
 | EOF { "end of annotation" }
 ;
@@ -1253,8 +1253,9 @@ ne_simple_clauses:
 | unknown_extension SEMICOLON simple_clauses { snd $3 }
 | EXT_CONTRACT extension_content SEMICOLON simple_clauses
     { let allocation,assigns,post_cond,extended = snd $4 in
-      let processed = Logic_env.preprocess_extension $1 $2 in
-      allocation,assigns,post_cond,($1,processed)::extended
+      let name, plugin = $1 in
+      let processed = Logic_env.preprocess_extension name $2 in
+      allocation,assigns,post_cond,(name, plugin, processed)::extended
     }
 | post_cond_kind lexpr clause_kw { missing $loc($2) ";" $3 }
 | allocation clause_kw { missing $loc($1) ";" $2 }
@@ -1474,12 +1475,12 @@ loop_variant:
 loop_grammar_extension:
 | LOOP EXT_CODE_ANNOT extension_content SEMICOLON {
   let open Cil_types in
-  let ext = $2 in
+  let ext, plugin = $2 in
   try
     begin match Logic_env.extension_category ext with
       | Ext_code_annot (Ext_next_loop | Ext_next_both) ->
         let processed = Logic_env.preprocess_extension ext $3 in
-        (ext, processed)
+        (ext, plugin, processed)
       | Ext_code_annot (Ext_here | Ext_next_stmt) ->
         raise
           (Not_well_formed
@@ -1523,12 +1524,12 @@ code_annotation:
 | EXT_CODE_ANNOT extension_content SEMICOLON
   { fun bhvs ->
     let open Cil_types in
-    let ext = $1 in
+    let ext, plugin = $1 in
     try
       begin match Logic_env.extension_category ext with
         | Ext_code_annot (Ext_here | Ext_next_stmt | Ext_next_both) ->
           let processed = Logic_env.preprocess_extension ext $2 in
-          Logic_ptree.AExtended(bhvs,false,(ext,processed))
+          Logic_ptree.AExtended(bhvs,false,(ext,plugin,processed))
         | Ext_code_annot Ext_next_loop ->
           raise
             (Not_well_formed
@@ -1565,14 +1566,16 @@ decl:
 
 ext_decl:
 | EXT_GLOBAL extension_content SEMICOLON {
-     let processed = Logic_env.preprocess_extension $1 $2 in
-     Ext_lexpr($1, processed)
+    let name, plugin = $1 in
+     let processed = Logic_env.preprocess_extension name $2 in
+     Ext_lexpr(name, plugin, processed)
    }
 | EXT_GLOBAL_BLOCK any_identifier LBRACE ext_decls RBRACE {
+    let name, plugin = $1 in
     let processed_id,processed_block =
-       Logic_env.preprocess_extension_block $1 ($2,$4)
+       Logic_env.preprocess_extension_block name ($2,$4)
     in
-    Ext_extension($1,processed_id,processed_block)
+    Ext_extension(name, plugin, processed_id, processed_block)
    }
 ;
 
@@ -1961,7 +1964,7 @@ post_cond:
 
 is_acsl_spec:
 | post_cond  { snd $1 }
-| EXT_CONTRACT   { $1 }
+| EXT_CONTRACT { fst $1 }
 | ASSIGNS    { "assigns" }
 | ALLOCATES  { "allocates" }
 | FREES      { "frees" }
@@ -1976,9 +1979,9 @@ is_acsl_spec:
 ;
 
 is_acsl_decl_or_code_annot:
-| EXT_CODE_ANNOT { $1 }
-| EXT_GLOBAL     { $1 }
-| EXT_GLOBAL_BLOCK     { $1 }
+| EXT_CODE_ANNOT { fst $1 }
+| EXT_GLOBAL { fst $1 }
+| EXT_GLOBAL_BLOCK { fst $1 }
 | IDENTIFIER_EXT { $1 }
 | ASSUMES   { "assumes" }
 | ASSERT    { "assert" }
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index c3ba156d600c93787ce2fa69b00a4c3c27597b36..4b4f9d87c78930f558bf7506762ec896cdaf69d4 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -9820,7 +9820,7 @@ and doBody local_env (blk: Cabs.block) : chunk =
                      s.Logic_ptree.spec_behavior,
                    true
                  | CODE_ANNOT
-                     (Logic_ptree.AExtended(_,is_loop,(name,_)),loc) ->
+                     (Logic_ptree.AExtended(_,is_loop,(name,_,_)),loc) ->
                    let source = fst loc in
                    (match Logic_env.extension_category name, is_loop with
                     | exception Not_found ->
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index b29782e0d6ccd48ac59fba7baeb9ecfcef499a44..7b9f5506e3435bef060c446572af72728c942a58 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1691,6 +1691,7 @@ and spec = {
 and acsl_extension = {
   ext_id : int;
   ext_name : string;
+  ext_plugin : string option; (**  @since Frama-C+dev *)
   ext_loc : location;
   ext_has_status : bool;
   ext_kind : acsl_extension_kind
diff --git a/src/kernel_services/ast_printing/logic_print.ml b/src/kernel_services/ast_printing/logic_print.ml
index 1baf4f4f3d24ae5afca9c1fcf72f2d4c5b073b7d..d38113e34761974fe117d869378c99da211d2e46 100644
--- a/src/kernel_services/ast_printing/logic_print.ml
+++ b/src/kernel_services/ast_printing/logic_print.ml
@@ -313,9 +313,9 @@ let print_model_annot fmt ty =
 let rec print_extended_decl fmt d =
   let aux fmt d = print_extended_decl fmt d.extended_node in
   match d with
-  | Ext_lexpr(name,d) ->
+  | Ext_lexpr(name, _plugin, d) ->
     fprintf fmt "@[<2>%s@ %a@]" name (pp_list ~sep:",@ " print_lexpr) d
-  | Ext_extension(name,id,d) ->
+  | Ext_extension(name, _plugin, id,d) ->
     fprintf fmt "@[<2>%s@ %s@ {@\n%a@]@\n}" name id
       (pp_list ~sep:"@\n" aux) d
 
@@ -458,7 +458,7 @@ let print_spec fmt spec =
        ~sep:"@\n" ~suf:"@\n" (pp_list ~sep:",@ " pp_print_string))
     spec.spec_disjoint_behaviors
 
-let print_extension fmt (name, ext) =
+let print_extension fmt (name, _plugin, ext) =
   fprintf fmt "%s %a" name (pp_list ~sep:",@ " print_lexpr) ext
 
 let print_code_annot fmt ca =
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 4aca4612649883b0cf76235bf72965e323d5e18f..ca54c24ac69723247430795f79b62d6dcc3e3d25 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -1794,7 +1794,7 @@ and visitCilExtended vis orig =
   let visit = Extensions.visit orig.ext_name in
   let e' = doVisitCil vis id (visit vis) childrenCilExtended orig.ext_kind in
   if Visitor_behavior.is_fresh vis#behavior then
-    Logic_const.new_acsl_extension orig.ext_name orig.ext_loc
+    Logic_const.new_acsl_extension orig.ext_name orig.ext_plugin orig.ext_loc
       orig.ext_has_status e'
   else if orig.ext_kind == e' then orig else {orig with ext_kind = e'}
 
diff --git a/src/kernel_services/ast_queries/logic_const.ml b/src/kernel_services/ast_queries/logic_const.ml
index 5b66f11b696ed3809673e9bd66235797a7df8f05..2e52b0fdd7422f5b8717fc37f2842f275d7cbb5d 100644
--- a/src/kernel_services/ast_queries/logic_const.ml
+++ b/src/kernel_services/ast_queries/logic_const.ml
@@ -58,8 +58,14 @@ let refresh_predicate p = { p with ip_id = PredicateId.next () }
 let new_identified_term t =
   { it_id = TermId.next (); it_content = t }
 
-let new_acsl_extension ext_name ext_loc ext_has_status ext_kind =
-  {ext_id = ExtendedId.next (); ext_name; ext_loc; ext_has_status; ext_kind}
+let new_acsl_extension ext_name ext_plugin ext_loc ext_has_status ext_kind = {
+  ext_id = ExtendedId.next ();
+  ext_name;
+  ext_plugin;
+  ext_loc;
+  ext_has_status;
+  ext_kind
+}
 
 let fresh_term_id = TermId.next
 
diff --git a/src/kernel_services/ast_queries/logic_const.mli b/src/kernel_services/ast_queries/logic_const.mli
index 01448f53738a7a080ca6f81193aea6ab149c537e..9de783d06437065910db64bf5408d00cf3713e1a 100644
--- a/src/kernel_services/ast_queries/logic_const.mli
+++ b/src/kernel_services/ast_queries/logic_const.mli
@@ -67,9 +67,11 @@ val new_predicate: ?kind:predicate_kind -> predicate -> identified_predicate
 (** creates a new acsl_extension with a fresh id.
     @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf>
     @since Chlorine-20180501
+    @begore the function took one less argument, [string option] which is now
+    used to set the [ext_plugin] field.
 *)
-val new_acsl_extension:
-  string -> location -> bool -> acsl_extension_kind -> acsl_extension
+val new_acsl_extension: string -> string option -> location -> bool ->
+  acsl_extension_kind -> acsl_extension
 
 (** Gives a new id to an existing predicate.
     @since Oxygen-20120901
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index e7f3e3ff6034f52f5fdb9f572988c1adb18615b7..df9afc27af75111599cbe57f90b42aeddc7c178d 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -3783,14 +3783,14 @@ struct
       old_behaviors
       behaviors
 
-  let type_extended ~typing_context ~loc (name,ps) =
+  let type_extended ~typing_context ~loc (name, plugin, ps) =
     let loc = match ps with
       | [] -> loc
       | p::_ -> p.lexpr_loc
     in
     if Extensions.is_extension name then
       let status , kind = Extensions.typer name ~typing_context ~loc ps in
-      Logic_const.new_acsl_extension name loc status kind
+      Logic_const.new_acsl_extension name plugin loc status kind
     else
       C.error
         loc "No type-checking function registered for extension %s" name
@@ -3996,8 +3996,8 @@ struct
         let env = loop_annot_env () in
         let ctxt = base_ctxt env in
         Cil_types.AAssigns(behav, type_assign ctxt ~accept_formal:true env a)
-      | AExtended (behav, is_loop, (name, _ as ext)) ->
         let kind = Logic_env.extension_category name in
+      | AExtended (behav, is_loop, (name, plugin, _ as ext)) ->
         let pre_state, post_state =
           match kind,is_loop with
           | exception Not_found ->
@@ -4497,18 +4497,18 @@ struct
       let wvi_opt = get_volatile_fct checks_writes_fct wr_opt in
       Some (Dvolatile (tsets, rvi_opt, wvi_opt, [], loc))
 
-    | LDextended (Ext_lexpr(kind, content)) ->
+    | LDextended (Ext_lexpr(name, plugin, content)) ->
       let typing_context = base_ctxt (Lenv.empty ()) in
-      let status,tcontent = Extensions.typer kind ~typing_context ~loc content in
-      let textended = Logic_const.new_acsl_extension kind loc status tcontent in
+      let status,tcontent = Extensions.typer name ~typing_context ~loc content in
+      let textended = Logic_const.new_acsl_extension name plugin loc status tcontent in
       Some (Dextended (textended, [], loc))
 
-    | LDextended (Ext_extension (kind, name, content)) ->
+    | LDextended (Ext_extension (name, plugin, kind, content)) ->
       let typing_context = base_ctxt (Lenv.empty ()) in
       let status,tcontent =
-        Extensions.typer_block kind ~typing_context ~loc (name,content)
+        Extensions.typer_block name ~typing_context ~loc (kind,content)
       in
-      let textended = Logic_const.new_acsl_extension kind loc status tcontent in
+      let textended = Logic_const.new_acsl_extension name plugin loc status tcontent in
       Some (Dextended (textended, [], loc))
 
   let annot = C.on_error
diff --git a/src/kernel_services/parsetree/logic_ptree.ml b/src/kernel_services/parsetree/logic_ptree.ml
index b079330d0ef0a6dc51ea6b1b3f75a75ac76f004e..7fbcc3cde091a58741bb1fec8fccc73149fdc916 100644
--- a/src/kernel_services/parsetree/logic_ptree.ml
+++ b/src/kernel_services/parsetree/logic_ptree.ml
@@ -165,7 +165,10 @@ and lexpr_node =
 type toplevel_predicate =
   { tp_kind: Cil_types.predicate_kind; tp_statement: lexpr }
 
-type extension = string * lexpr list
+(** ACSL extension.
+    @before Frama-C+dev Was of type [string * lexpr list].
+*)
+type extension = string * string option * lexpr list
 
 (** type invariant. *)
 type type_annot =  {inv_name: string;
@@ -282,9 +285,14 @@ and allocation =
 (** variant of a loop or a recursive function. *)
 and variant = lexpr * string option
 
+
+(** Global ACSL extension. *)
 and global_extension =
-  | Ext_lexpr of string * lexpr list
-  | Ext_extension of string * string * extended_decl list
+  | Ext_lexpr of string * string option * lexpr list
+  (** @before Frama-C+dev Was of type [string * lexpr list]. *)
+
+  | Ext_extension of string * string option * string * extended_decl list
+  (** @before Frama-C+dev Was of type [string * string * extended_decl list]. *)
 
 and extended_decl = {
   extended_node : global_extension;
diff --git a/src/plugins/eva/utils/eva_annotations.ml b/src/plugins/eva/utils/eva_annotations.ml
index 91f28919b04a085bd7ace65aef587e3b7708fb92..0823af80570e8802e8039d2f73f09353f3a0a135 100644
--- a/src/plugins/eva/utils/eva_annotations.ml
+++ b/src/plugins/eva/utils/eva_annotations.ml
@@ -114,7 +114,10 @@ struct
   let add ~emitter stmt annot =
     let loc = Cil_datatype.Stmt.loc stmt in
     let param = M.export annot in
-    let extension = Logic_const.new_acsl_extension name loc false param in
+    let plugin = Some "eva" in
+    let extension =
+      Logic_const.new_acsl_extension name plugin loc false param
+    in
     let annot_node = Cil_types.AExtended ([], kind = Loop, extension) in
     let code_annotation = Logic_const.new_code_annotation annot_node in
     Annotations.add_code_annot emitter stmt code_annotation