diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 13259d5a56cf1cbc129ac1842053fbaf8d629cec..98b6fab58ce1955d19dcccb283aefa15013c40a9 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -27,6 +27,15 @@ open Cil_datatype
 open Printer_api
 open Format
 
+let initialized_extensions = ref false
+let ref_print_extension = ref (fun _ _ _ _ -> assert false)
+
+let set_extension_handler ~print =
+  assert (not !initialized_extensions) ;
+  ref_print_extension := print ;
+  initialized_extensions := true ;
+  ()
+
 module Behavior_extensions = struct
 
   let printer_tbl = Hashtbl.create 5
diff --git a/src/kernel_services/ast_printing/cil_printer.mli b/src/kernel_services/ast_printing/cil_printer.mli
index 3edbd8bc09e81650ba7cc7a2caff541df00960ce..04e4206ae373e21068b9c5668a19b3b1e35cf37c 100644
--- a/src/kernel_services/ast_printing/cil_printer.mli
+++ b/src/kernel_services/ast_printing/cil_printer.mli
@@ -73,6 +73,17 @@ val print_global: Cil_types.global -> bool
 (** Is the given global displayed by the pretty-printer.
     @since Aluminium-20160501 *)
 
+(**/**)
+
+val set_extension_handler:
+  print:(string -> Printer_api.extensible_printer_type -> Format.formatter ->
+         Cil_types.acsl_extension_kind -> unit) ->
+  unit
+(** Used to setup a reference related to the handling of ACSL extensions.
+    If your name is not [Acsl_extension], do not call this
+    @since Frama-C+dev
+*)
+
 (*
 Local Variables:
 compile-command: "make -C ../../.."
diff --git a/src/kernel_services/ast_queries/acsl_extension.ml b/src/kernel_services/ast_queries/acsl_extension.ml
index 3354d9e42e67bd2742d56b7fc60a873fc69ff164..f59ee45bf2ffff79fc074cb3b48b8c8d7c7227a9 100644
--- a/src/kernel_services/ast_queries/acsl_extension.ml
+++ b/src/kernel_services/ast_queries/acsl_extension.ml
@@ -103,3 +103,17 @@ let register_code_annot_next_loop =
   Extensions.register (Ext_code_annot Ext_next_loop)
 let register_code_annot_next_both =
   Extensions.register (Ext_code_annot Ext_next_both)
+
+(* Setup global references *)
+
+let () =
+  Logic_env.set_extension_handler
+    ~category:Extensions.category
+    ~is_extension: Extensions.is_extension ;
+  Logic_typing.set_extension_handler
+    ~is_extension: Extensions.is_extension
+    ~typer: Extensions.typing ;
+  Cil.set_extension_handler
+    ~visit: Extensions.visit ;
+  Cil_printer.set_extension_handler
+    ~print: Extensions.print
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index d52be341225739de126ccc744555a101393a6d96..d17d73e3598e21292f648b5dded85be2158cc58f 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -757,6 +757,15 @@ let alphatrue _ = true
 
 let visitor_tbl = Hashtbl.create 5
 
+let initialized_extensions = ref false
+let ref_visit_extension = ref (fun _ _ _ -> assert false)
+
+let set_extension_handler ~visit =
+  assert (not !initialized_extensions) ;
+  ref_visit_extension := visit ;
+  initialized_extensions := true ;
+  ()
+
 let register_behavior_extension name ext = Hashtbl.add visitor_tbl name ext
 
 (* sm/gn: cil visitor interface for traversing Cil trees. *)
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 71441398d0f3295ff00892f83f4c7a5b59b37a5d..61d314736e209f61c78a373b35d0cb16518fba85 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -2283,6 +2283,15 @@ val pp_ikind_ref: (Format.formatter -> ikind -> unit) ref
 val pp_attribute_ref: (Format.formatter -> attribute -> unit) ref
 val pp_attributes_ref: (Format.formatter -> attribute list -> unit) ref
 
+val set_extension_handler:
+  visit:(string -> cilVisitor -> acsl_extension_kind ->
+         acsl_extension_kind visitAction) ->
+  unit
+(** Used to setup a reference related to the handling of ACSL extensions.
+    If your name is not [Acsl_extension], do not call this
+    @since Frama-C+dev
+*)
+
 (*
 Local Variables:
 compile-command: "make -C ../../.."
diff --git a/src/kernel_services/ast_queries/logic_env.ml b/src/kernel_services/ast_queries/logic_env.ml
index 5c09918e303db103dbf6ea685ef0c85b6638eb26..341ab6de574c2ce265ae27ad0967dabb87b8df99 100644
--- a/src/kernel_services/ast_queries/logic_env.ml
+++ b/src/kernel_services/ast_queries/logic_env.ml
@@ -24,6 +24,18 @@
 
 open Cil_types
 
+let initialized_extensions = ref false
+let ref_is_extension = ref (fun _ -> assert false)
+let ref_extension_category = ref (fun _ -> assert false)
+
+let set_extension_handler ~category ~is_extension =
+  assert (not !initialized_extensions) ;
+  ref_is_extension := is_extension ;
+  ref_extension_category := category ;
+  initialized_extensions := true ;
+  ()
+
+
 let extensions = ref Datatype.String.Map.empty
 
 let is_extension s = Datatype.String.Map.mem s !extensions
diff --git a/src/kernel_services/ast_queries/logic_env.mli b/src/kernel_services/ast_queries/logic_env.mli
index afa488e5c8e8770e01b7c23807a6807a3df0fb41..2207c731d99d57431e2bd4288bdb245e71f658e1 100644
--- a/src/kernel_services/ast_queries/logic_env.mli
+++ b/src/kernel_services/ast_queries/logic_env.mli
@@ -204,6 +204,15 @@ val builtin_types_as_typenames: unit -> unit
 
 (** {2 Internal use} *)
 
+val set_extension_handler:
+  category:(string -> ext_category option) ->
+  is_extension:(string -> bool) ->
+  unit
+(** Used to setup references related to the handling of ACSL extensions.
+    If your name is not [Acsl_extension], do not call this
+    @since Frama-C+dev
+*)
+
 val init_dependencies: State.t -> unit
 (** Used to postpone dependency of Lenv global tables wrt Cil_state, which
     is initialized afterwards. *)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 08b217e0cc326183800bd3c00694e7c0eb695e18..586294e2a0d73ae0a4c62d8198be4fab76fea915 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -524,6 +524,17 @@ type typing_context = {
   on_error: 'a 'b. ('a -> 'b) -> (unit -> unit) -> 'a -> 'b
 }
 
+let initialized_extensions = ref false
+let ref_is_extension = ref (fun _ -> assert false)
+let ref_type_extension = ref (fun _ _ _ _ -> assert false)
+
+let set_extension_handler ~is_extension ~typer =
+  assert (not !initialized_extensions) ;
+  ref_is_extension := is_extension ;
+  ref_type_extension := typer ;
+  initialized_extensions := true ;
+  ()
+
 module Extensions = struct
   let typer_tbl = Hashtbl.create 5
   let find_typer name = Hashtbl.find typer_tbl name
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index e6c6c5460f6373b9a5681550d8ec601875ac4e5d..5d6bb73f7ff2eeded39bcf4c86e8050985d15757 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -371,6 +371,18 @@ val enter_post_state: Lenv.t -> termination_kind -> Lenv.t
 val post_state_env: termination_kind -> logic_type -> Lenv.t
 
 
+(** {2 Internal use} *)
+
+val set_extension_handler:
+  is_extension:(string -> bool) ->
+  typer:(string -> typing_context -> location -> Logic_ptree.lexpr list ->
+         (bool * acsl_extension_kind)) ->
+  unit
+(** Used to setup references related to the handling of ACSL extensions.
+    If your name is not [Acsl_extension], do not call this
+    @since Frama-C+dev
+*)
+
 (*
 Local Variables:
 compile-command: "make -C ../../.."