diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index ab8aea9acf16656c6ce84c8cb09682526a4c4f6b..431a6194222ae6bfb327c047a0b10ba671ee8439 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -29,10 +29,12 @@ open Format
 
 let initialized_extensions = ref false
 let ref_print_extension = ref (fun _ _ _ _ -> assert false)
+let ref_print_short_extension = ref (fun _ _ _ _ -> assert false)
 
-let set_extension_handler ~print =
+let set_extension_handler ~print ~short_print =
   assert (not !initialized_extensions) ;
   ref_print_extension := print ;
+  ref_print_short_extension := short_print ;
   initialized_extensions := true ;
   ()
 
@@ -40,26 +42,27 @@ let ref_deprecated_extension_handler = ref (fun _ _ _ -> assert false)
 let set_deprecated_extension_handler ~handler =
   ref_deprecated_extension_handler := handler
 
-module Behavior_extensions = struct
+module Acsl_extensions = struct
   let deprecated_register name =
     !ref_deprecated_extension_handler name
 
   let pp (printer) fmt {ext_name; ext_kind} =
-    let pp = !ref_print_extension ext_name in
-    Format.fprintf fmt "@[<hov 2>%s %a;@]" ext_name (pp printer) ext_kind
+    !ref_print_extension ext_name printer fmt ext_kind
 
+  let pp_short (printer) fmt {ext_name; ext_kind} =
+    !ref_print_short_extension ext_name printer fmt ext_kind
 end
 let register_behavior_extension name =
-  Behavior_extensions.deprecated_register name Ext_contract
+  Acsl_extensions.deprecated_register name Ext_contract
 
 let register_code_annot_extension name =
-  Behavior_extensions.deprecated_register name (Ext_code_annot Ext_here)
+  Acsl_extensions.deprecated_register name (Ext_code_annot Ext_here)
 
 let register_loop_annot_extension name =
-  Behavior_extensions.deprecated_register name (Ext_code_annot Ext_next_loop)
+  Acsl_extensions.deprecated_register name (Ext_code_annot Ext_next_loop)
 
 let register_global_extension name =
-  Behavior_extensions.deprecated_register name Ext_global
+  Acsl_extensions.deprecated_register name Ext_global
 
 (* Internal attributes. Won't be pretty-printed *)
 let reserved_attributes = ref []
@@ -2748,8 +2751,11 @@ class cil_printer () = object (self)
       self#pp_acsl_keyword "requires"
       self#identified_predicate p
 
-  method extended fmt (ext : acsl_extension) =
-    Behavior_extensions.pp (self :> extensible_printer_type) fmt ext
+  method extended fmt ext =
+    Acsl_extensions.pp (self :> extensible_printer_type) fmt ext
+
+  method short_extended fmt ext =
+    Acsl_extensions.pp_short (self :> extensible_printer_type) fmt ext
 
   method post_cond fmt (k,p) =
     let kw = get_termination_kind_name k in
diff --git a/src/kernel_services/ast_printing/cil_printer.mli b/src/kernel_services/ast_printing/cil_printer.mli
index 3c7260976c27f9451335904d3dad188469fe58b9..bca6dd1a6ac74773858c35cb61a7527d5c6693a2 100644
--- a/src/kernel_services/ast_printing/cil_printer.mli
+++ b/src/kernel_services/ast_printing/cil_printer.mli
@@ -84,8 +84,10 @@ val print_global: Cil_types.global -> bool
 (**/**)
 
 val set_extension_handler:
-  print:(string -> Printer_api.extensible_printer_type -> Format.formatter ->
-         Cil_types.acsl_extension_kind -> unit) ->
+  print:(string -> Printer_api.extensible_printer_type ->
+         Format.formatter -> Cil_types.acsl_extension_kind -> unit) ->
+  short_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
diff --git a/src/kernel_services/ast_printing/printer_api.mli b/src/kernel_services/ast_printing/printer_api.mli
index edc38a8890da411df5bc4698814c770cad3837db..b377d619209b748b717be7efffaa57e09f18ae90 100644
--- a/src/kernel_services/ast_printing/printer_api.mli
+++ b/src/kernel_services/ast_printing/printer_api.mli
@@ -283,6 +283,7 @@ class type extensible_printer_type = object
   method assumes: Format.formatter -> identified_predicate -> unit
 
   method extended: Format.formatter -> Cil_types.acsl_extension -> unit
+  method short_extended: Format.formatter -> Cil_types.acsl_extension -> unit
 
   method funspec: Format.formatter -> funspec -> unit
 
@@ -444,6 +445,8 @@ module type S_pp = sig
   val pp_logic_label: Format.formatter -> logic_label -> unit
   val pp_builtin_logic_info: Format.formatter -> builtin_logic_info -> unit
   val pp_extended: Format.formatter -> acsl_extension -> unit
+  val pp_short_extended: Format.formatter -> acsl_extension -> unit
+  (** @since Frama-C+dev *)
   val pp_predicate_node: Format.formatter -> predicate_node -> unit
   val pp_predicate: Format.formatter -> predicate -> unit
   val pp_identified_predicate: Format.formatter -> identified_predicate -> unit
diff --git a/src/kernel_services/ast_printing/printer_builder.ml b/src/kernel_services/ast_printing/printer_builder.ml
index bba10960ff4b6230c9e9f06c7bf1ab1b3302d263..1d9ba02b1b68e8d275b3696c2d5735feb4f9ff16 100644
--- a/src/kernel_services/ast_printing/printer_builder.ml
+++ b/src/kernel_services/ast_printing/printer_builder.ml
@@ -85,6 +85,7 @@ struct
   let pp_logic_type_info fmt x = (printer ())#logic_type_info fmt x
   let pp_logic_ctor_info fmt x = (printer ())#logic_ctor_info fmt x
   let pp_extended fmt x = (printer())#extended fmt x
+  let pp_short_extended fmt x = (printer())#short_extended fmt x
   let pp_initinfo fmt x = (printer ())#initinfo fmt x
   let pp_logic_info fmt x = (printer ())#logic_info fmt x
   let pp_logic_constant fmt x = (printer ())#logic_constant fmt x
diff --git a/src/kernel_services/ast_queries/acsl_extension.ml b/src/kernel_services/ast_queries/acsl_extension.ml
index 93c4d883ef2977187d1973eb84be8e8a7ed4f7db..0d3a497fd012a1238b8300b935d622f095d71385 100644
--- a/src/kernel_services/ast_queries/acsl_extension.ml
+++ b/src/kernel_services/ast_queries/acsl_extension.ml
@@ -25,11 +25,13 @@ open Logic_typing
 open Logic_ptree
 
 type extension = {
+  category: ext_category ;
   status: bool ;
   preprocessor: extension_preprocessor ;
   typer: extension_typer ;
   visitor: extension_visitor ;
   printer: extension_printer ;
+  short_printer: extension_printer option
 }
 and extension_preprocessor =
   lexpr list -> lexpr list
@@ -41,49 +43,42 @@ and extension_printer =
   Printer_api.extensible_printer_type -> Format.formatter ->
   acsl_extension_kind -> unit
 
-(* Default extension *)
-
-let default_preprocessor = Extlib.id
-
-let default_typer typing_context loc l =
-  let _ = loc in
-  let typing = typing_context.type_predicate typing_context (Lenv.empty ()) in
-  Ext_preds (List.map typing l)
-
-let default_visitor _ _ = Cil.DoChildren
-
 let default_printer printer fmt = function
   | Ext_id i -> Format.fprintf fmt "%d" i
   | Ext_terms ts -> Pretty_utils.pp_list ~sep:",@ " printer#term fmt ts
   | Ext_preds ps -> Pretty_utils.pp_list ~sep:",@ " printer#predicate fmt ps
 
 let make
-  ?(status=false)
-  ?(preprocessor=default_preprocessor)
-  ?(typer=default_typer)
-  ?(visitor=default_visitor)
-  ?(printer=default_printer)
-  () = { status ; preprocessor ; typer ; visitor ; printer }
+    category
+    ?(preprocessor=Extlib.id)
+    typer
+    ?(visitor=fun _ _ -> Cil.DoChildren)
+    ?(printer=default_printer) ?short_printer status =
+  { category; status; preprocessor; typer; visitor; printer; short_printer }
 
 module Extensions = struct
   let ext_tbl = Hashtbl.create 5
 
   let find name =
-    try snd (Hashtbl.find ext_tbl name)
+    try Hashtbl.find ext_tbl name
     with Not_found ->
       Kernel.fatal ~current:true "unsupported clause of name '%s'" name
 
   let category name =
-    Extlib.opt_map fst (Hashtbl.find_opt ext_tbl name)
+    Extlib.opt_map (fun e -> e.category) (Hashtbl.find_opt ext_tbl name)
 
   let is_extension = Hashtbl.mem ext_tbl
 
-  let register category name info =
+  let register
+      cat name ?preprocessor typer ?visitor ?printer ?short_printer status =
+    let info =
+      make cat ?preprocessor typer ?visitor ?printer ?short_printer status
+    in
     if is_extension name then
       Kernel.warning ~wkey:Kernel.wkey_acsl_extension
         "Trying to register ACSL extension %s twice. Ignoring second extension"
         name
-    else Hashtbl.add ext_tbl name (category, info)
+    else Hashtbl.add ext_tbl name info
 
   let preprocess name = (find name).preprocessor
 
@@ -91,13 +86,31 @@ module Extensions = struct
     let ext_info = find name in
     let status = ext_info.status in
     let typer =  ext_info.typer in
-    status, (typer typing_context loc es)
+    let normal_error = ref false in
+    let has_error () = normal_error := true in
+    let wrapper =
+      typing_context.on_error (typer typing_context loc) has_error
+    in
+    try status, wrapper es
+    with
+    | (Log.AbortError _ | Log.AbortFatal _) as exn -> raise exn
+    | exn when not !normal_error ->
+      Kernel.fatal "Typechecking ACSL extension %s raised exception %s"
+        name (Printexc.to_string exn)
 
-  let print name = (find name).printer
   let visit name = (find name).visitor
+
+  let print name printer fmt kind =
+    let pp = (find name).printer printer in
+    Format.fprintf fmt "@[<hov 2>%s %a;@]" name pp kind
+
+  let short_print name printer fmt kind =
+    match (find name).short_printer with
+    | None -> Format.fprintf fmt "%s" name
+    | Some pp -> Format.fprintf fmt "%s: %a" name (pp printer) kind
 end
 
-(* Registration *)
+(* Registration functions *)
 
 let register_behavior =
   Extensions.register Ext_contract
@@ -126,6 +139,7 @@ let () =
     ~visit: Extensions.visit ;
   Cil_printer.set_extension_handler
     ~print: Extensions.print
+    ~short_print:Extensions.short_print
 
 (* For Deprecation: *)
 
@@ -133,14 +147,17 @@ let deprecated_replace name ext = Hashtbl.add Extensions.ext_tbl name ext
 
 let strong_cat = Hashtbl.create 5
 
+let default_typer _typing_context _loc _l = assert false
+
+
 let deprecated_find ?(strong=true) name cat op_name =
   match Hashtbl.find_opt Extensions.ext_tbl name with
   | None ->
     if strong then Hashtbl.add strong_cat name cat ;
-    (cat, make ())
-  | Some (found_cat, ext) ->
+    (make cat default_typer false)
+  | Some ext ->
     if strong && Hashtbl.mem strong_cat name then begin
-      if found_cat = cat then (cat, ext)
+      if ext.category = cat then ext
       else
         Kernel.fatal
           "Registring %s for %s: this extension already exists for another \
@@ -148,24 +165,20 @@ let deprecated_find ?(strong=true) name cat op_name =
           op_name name
     end else if strong then begin
       Hashtbl.add strong_cat name cat ;
-      (cat, ext)
-    end else
-      (found_cat, ext)
+      { ext with category = cat }
+    end else ext
 
 let deprecated_register_typing name cat status typer =
-  let cat, ext = deprecated_find name cat "typing" in
-  let ext = { ext with status ; typer } in
-  deprecated_replace name (cat, ext)
+  deprecated_replace name
+    { (deprecated_find name cat "typing") with status ; typer }
 
 let deprecated_register_printing name cat printer =
-  let cat, ext = deprecated_find ~strong:false name cat "printing" in
-  let ext = { ext with printer } in
-  deprecated_replace name (cat, ext)
+  deprecated_replace name
+    { (deprecated_find ~strong:false name cat "printing") with printer }
 
 let deprecated_register_visit name cat visitor =
-  let cat, ext = deprecated_find name cat "visit" in
-  let ext = { ext with visitor } in
-  deprecated_replace name (cat, ext)
+  deprecated_replace name
+    { (deprecated_find name cat "visit") with visitor }
 
 let () =
   Logic_typing.set_deprecated_extension_handler deprecated_register_typing ;
diff --git a/src/kernel_services/ast_queries/acsl_extension.mli b/src/kernel_services/ast_queries/acsl_extension.mli
index d766cd9e0771ad6f6a837d8e7c83e4e315535aa1..42e2a3b0636cdeb4096827977e8087120aaf8019 100644
--- a/src/kernel_services/ast_queries/acsl_extension.mli
+++ b/src/kernel_services/ast_queries/acsl_extension.mli
@@ -36,17 +36,38 @@ type extension_printer =
   Printer_api.extensible_printer_type -> Format.formatter ->
   acsl_extension_kind -> unit
 
-val make:
-  ?status:bool ->
-  ?preprocessor:extension_preprocessor ->
-  ?typer:extension_typer ->
+val register_behavior:
+  string -> ?preprocessor:extension_preprocessor -> extension_typer ->
   ?visitor:extension_visitor ->
-  ?printer:extension_printer ->
-  unit -> extension
-
-val register_behavior: string -> extension -> unit
-val register_global: string -> extension -> unit
-val register_code_annot: string -> extension -> unit
-val register_code_annot_next_stmt: string -> extension -> unit
-val register_code_annot_next_loop: string -> extension -> unit
-val register_code_annot_next_both: string -> extension -> unit
+  ?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
+  unit
+
+val register_global:
+  string -> ?preprocessor:extension_preprocessor -> extension_typer ->
+  ?visitor:extension_visitor ->
+  ?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
+  unit
+
+val register_code_annot:
+  string -> ?preprocessor:extension_preprocessor -> extension_typer ->
+  ?visitor:extension_visitor ->
+  ?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
+  unit
+
+val register_code_annot_next_stmt:
+  string -> ?preprocessor:extension_preprocessor -> extension_typer ->
+  ?visitor:extension_visitor ->
+  ?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
+  unit
+
+val register_code_annot_next_loop:
+  string -> ?preprocessor:extension_preprocessor -> extension_typer ->
+  ?visitor:extension_visitor ->
+  ?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
+  unit
+
+val register_code_annot_next_both:
+  string -> ?preprocessor:extension_preprocessor -> extension_typer ->
+  ?visitor:extension_visitor ->
+  ?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
+  unit
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 57775843694f86152917c9b86cc5bf81c8882a66..aa3797f02bfc318cbd4776a67deefc04969360eb 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -524,43 +524,35 @@ 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)
+module Extensions = struct
+  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 ;
-  ()
+  let is_extension name = !ref_is_extension name
 
-let ref_deprecated_extension_handler = ref (fun _ _ _ _  -> assert false)
-let set_deprecated_extension_handler ~handler =
-  ref_deprecated_extension_handler := handler
+  let typer name ~typing_context:typing_context ~loc =
+    !ref_type_extension name typing_context loc
 
-module Extensions = struct
-  let is_extension name = !ref_is_extension name
+  (* For deprecated functions *)
+  let ref_deprecated_extension_handler = ref (fun _ _ _ _  -> assert false)
 
   let deprecated_register name category status typer =
     let typer typing_context loc = typer ~typing_context ~loc in
     !ref_deprecated_extension_handler name category status typer
-
-  let typer name ~typing_context:typing_context ~loc p =
-    let typer = !ref_type_extension name in
-    let normal_error = ref false in
-    let has_error () = normal_error := true in
-    let wrapper =
-      typing_context.on_error (typer typing_context loc) has_error
-    in
-    try wrapper p
-    with
-    | (Log.AbortError _ | Log.AbortFatal _) as exn -> raise exn
-    | exn when not !normal_error ->
-      Kernel.fatal "Typechecking ACSL extension %s raised exception %s"
-        name (Printexc.to_string exn)
 end
 
+let set_extension_handler ~is_extension ~typer =
+  assert (not !Extensions.initialized_extensions) ;
+  Extensions.ref_is_extension := is_extension ;
+  Extensions.ref_type_extension := typer ;
+  Extensions.initialized_extensions := true ;
+  ()
+
+(* Deprecated ACSL extensions functions *)
+let set_deprecated_extension_handler ~handler =
+  Extensions.ref_deprecated_extension_handler := handler
+
 let register_behavior_extension name f =
   Extensions.deprecated_register name Ext_contract f
 
diff --git a/src/plugins/gui/filetree.ml b/src/plugins/gui/filetree.ml
index 6de5eb7f770e4a32d80c8f34ac81f9f89f7f50d1..92c21975c78aae90b60c2f0cb40f77779a794875 100644
--- a/src/plugins/gui/filetree.ml
+++ b/src/plugins/gui/filetree.ml
@@ -313,6 +313,7 @@ module MYTREE = struct
     }
 
   let global_name s = Pretty_utils.to_string Printer.pp_varname s
+  let extension_name e = Pretty_utils.to_string Printer.pp_short_extended e
 
   let ga_name = function
     | Dfun_or_pred (li, _) ->
@@ -325,7 +326,7 @@ module MYTREE = struct
     | Dtype_annot (li, _) -> Some (global_name li.l_var_info.lv_name)
     | Dmodel_annot (mf, _) -> Some (global_name mf.mi_name)
     | Dcustom_annot _ -> Some "custom clause"
-    | Dextended ({ext_name},_,_) -> Some ("ACSL extension " ^ ext_name)
+    | Dextended (e,_,_) -> Some ("ACSL extension " ^ (extension_name e))
 
   let make_list_globals hide sort_order globs =
     (* Association list binding names to globals. *)
diff --git a/src/plugins/value/utils/eva_annotations.ml b/src/plugins/value/utils/eva_annotations.ml
index ca5a1f0913e539e89c311b0516b7b7c62261cfb2..6e60ba02654ba94bab07162cf19fbb78e24e21be 100644
--- a/src/plugins/value/utils/eva_annotations.ml
+++ b/src/plugins/value/utils/eva_annotations.ml
@@ -78,11 +78,10 @@ struct
     print fmt (import lp)
 
   let () =
-    let ext = Acsl_extension.make ~typer ~printer () in
     if is_loop_annot then
-      Acsl_extension.register_code_annot_next_loop name ext
+      Acsl_extension.register_code_annot_next_loop name typer ~printer false
     else
-      Acsl_extension.register_code_annot_next_stmt name ext
+      Acsl_extension.register_code_annot_next_stmt name typer ~printer false
 
   let get stmt =
     let filter_add _emitter annot acc =
diff --git a/src/plugins/value/utils/widen_hints_ext.ml b/src/plugins/value/utils/widen_hints_ext.ml
index 90e2f8e3adad832e54e154584c10cbe571034da7..063e8317bbe79d0f3a6577aeceb5f7ac9d88304c 100644
--- a/src/plugins/value/utils/widen_hints_ext.ml
+++ b/src/plugins/value/utils/widen_hints_ext.ml
@@ -159,8 +159,8 @@ let printer _pp fmt ext =
       Format.fprintf fmt "<invalid widen_hints>"
 
 let () =
-  Acsl_extension.register_code_annot_next_both "widen_hints"
-    (Acsl_extension.make ~typer ~printer ())
+  Acsl_extension.register_code_annot_next_both
+    "widen_hints" typer ~printer false
 
 let get_widen_hints_annots stmt =
   Annotations.fold_code_annot
diff --git a/src/plugins/wp/RegionAnnot.ml b/src/plugins/wp/RegionAnnot.ml
index e3b44d751e2eb4042b1c45347a14f10c0051ab3d..7e99de63141c2fcf1d65a526785a3a8bd771b440 100644
--- a/src/plugins/wp/RegionAnnot.ml
+++ b/src/plugins/wp/RegionAnnot.ml
@@ -484,8 +484,8 @@ let register () =
   if Wp.Region.get () || Wp.Region_annot.get () ||
     List.exists specified (Wp.Model.get ())
   then
-    Acsl_extension.(register_behavior "region"
-      (make ~status:true ~typer:typecheck ~printer:pp_extension ()))
+    Acsl_extension.register_behavior
+      "region" typecheck ~printer:pp_extension false
 
 let () = Cmdline.run_after_configuring_stage register
 
diff --git a/src/plugins/wp/dyncall.ml b/src/plugins/wp/dyncall.ml
index 8ddd80fe51d2c6fb0fc8bd265bd16df621e11d33..06b27c6e5df7951b731e9bca88a990f5e5645581 100644
--- a/src/plugins/wp/dyncall.ml
+++ b/src/plugins/wp/dyncall.ml
@@ -261,9 +261,8 @@ let register =
     if (not !once) &&
        Wp_parameters.DynCall.get () then begin
       once := true;
-      let ext = Acsl_extension.make ~status:true ~typer:typecheck () in
-      Acsl_extension.register_code_annot_next_stmt "calls" ext;
-      Acsl_extension.register_behavior "instanceof" ext;
+      Acsl_extension.register_code_annot_next_stmt "calls" typecheck true ;
+      Acsl_extension.register_behavior "instanceof" typecheck true ;
     end
 
 let () = Cmdline.run_after_configuring_stage register
diff --git a/tests/spec/Extend.ml b/tests/spec/Extend.ml
index d29cffbb0720f3842389c9d921a8afd10db35673..99c5ea7064b6b8ad3de11702dafa936b3320e5e6 100644
--- a/tests/spec/Extend.ml
+++ b/tests/spec/Extend.ml
@@ -105,22 +105,15 @@ let type_bla typing_context _loc l =
   Ext_preds l
 
 let () =
-  Acsl_extension.(register_behavior "foo"
-    (make ~typer:type_foo ())) ;
-  Acsl_extension.(register_code_annot_next_loop "lfoo"
-    (make ~typer:type_foo ())) ;
-  Acsl_extension.(register_code_annot "ca_foo"
-    (make ~typer:type_foo ())) ;
-  Acsl_extension.(register_code_annot_next_stmt "ns_foo"
-    (make ~typer:type_foo ())) ;
-  Acsl_extension.(register_global "global_foo"
-    (make ~typer:type_foo ())) ;
-  Acsl_extension.(register_behavior "bar"
-    (make ~typer:type_bar ~printer:print_bar ~visitor:visit_bar ())) ;
-  Acsl_extension.(register_behavior "bla"
-    (make ~typer:type_bla ())) ;
-  Acsl_extension.(register_code_annot_next_both "baz"
-    (make ~typer:type_baz ()))
+  Acsl_extension.register_behavior "foo" type_foo false ;
+  Acsl_extension.register_code_annot_next_loop "lfoo" type_foo false ;
+  Acsl_extension.register_code_annot "ca_foo" type_foo false ;
+  Acsl_extension.register_code_annot_next_stmt "ns_foo" type_foo false ;
+  Acsl_extension.register_global "global_foo" type_foo false ;
+  Acsl_extension.register_behavior
+    "bar" type_bar ~printer:print_bar ~visitor:visit_bar false ;
+  Acsl_extension.register_behavior "bla" type_bla false ;
+  Acsl_extension.register_code_annot_next_both "baz" type_baz false
 
 let run () =
   Ast.compute ();
diff --git a/tests/spec/Extend_preprocess.ml b/tests/spec/Extend_preprocess.ml
index 32ff035e04f8d83b9837c407226b291b248c0fc9..a81bc3b7ce89960961445c1c4151127b78d7428b 100644
--- a/tests/spec/Extend_preprocess.ml
+++ b/tests/spec/Extend_preprocess.ml
@@ -2,16 +2,16 @@ open Logic_ptree
 open Logic_const
 
 (* For each kind of extension:
-    - behavior:        bhv
-    - next loop:       nl
-    - code annotation: ca
-    - next statement:  ns
-    - global:          gl
+   - behavior:        bhv
+   - next loop:       nl
+   - code annotation: ca
+   - next statement:  ns
+   - global:          gl
   replaces node "must_replace(x)" with "<kind>_ok(x)". The typing phase
   validates that we find the right "<kind>_ok" for each kind of extension:
-    - if a must_replaced is found, it fails,
-    - if the wrong kind is found, a "\false" is generated
-    - if everything is ok "\true" is generated
+   - if a must_replaced is found, it fails,
+   - if the wrong kind is found, a "\false" is generated
+   - if everything is ok "\true" is generated
 *)
 
 let validate kind call =
@@ -36,15 +36,17 @@ let preprocess_foo_ptree_element kind = function
 
 let preprocess_foo_ptree kind = List.map (preprocess_foo_ptree_element kind)
 
-let register registration kind =
-  let typer = ext_typing kind in
-  let preprocessor = preprocess_foo_ptree kind in
-  let ext = Acsl_extension.make ~typer ~preprocessor () in
-  registration (kind ^ "_foo") ext
+let register registration ?visitor ?printer ?short_printer kind =
+  let registration ?preprocessor typer =
+    registration
+      (kind ^ "_foo") ?preprocessor typer ?visitor ?printer ?short_printer false
+  in
+  registration ~preprocessor:(preprocess_foo_ptree kind) (ext_typing kind)
+
 
 let () =
   let open Acsl_extension in
-  register register_behavior "bhv" ;
+  register register_behavior "bhv";
   register register_code_annot_next_loop "nl";
   register register_code_annot "ca";
   register register_code_annot_next_stmt "ns";
diff --git a/tests/spec/Extend_short_print.i b/tests/spec/Extend_short_print.i
new file mode 100644
index 0000000000000000000000000000000000000000..62da2756985c2095d1740a21da9f89a676a81387
--- /dev/null
+++ b/tests/spec/Extend_short_print.i
@@ -0,0 +1,9 @@
+/* run.config
+EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+*/
+
+/*@
+  without_short \true ;
+  with_short \true ;
+*/
\ No newline at end of file
diff --git a/tests/spec/Extend_short_print.ml b/tests/spec/Extend_short_print.ml
new file mode 100644
index 0000000000000000000000000000000000000000..de0cb70361f8eb0a521088922696f1c8482f3d6b
--- /dev/null
+++ b/tests/spec/Extend_short_print.ml
@@ -0,0 +1,14 @@
+open Cil_types
+
+let typer _context _loc _tree = Ext_id 42
+let short_printer _printer fmt _kind = Format.fprintf fmt "some content"
+
+let () =
+  Acsl_extension.register_global "without_short" typer false ;
+  Acsl_extension.register_global "with_short" typer ~short_printer false
+
+let process_global _ = function
+  | Dextended(e, _, _) -> Kernel.feedback "%a" Cil_printer.pp_short_extended e
+  | _ -> ()
+
+let () = Db.Main.extend (fun () -> Annotations.iter_global process_global)
\ No newline at end of file
diff --git a/tests/spec/extend_extern.ml b/tests/spec/extend_extern.ml
index c2e055f5f905b06a08a036a646d5663cc456d9e2..50dc6941ce3f3691e515f2d9bc04f59f1db844c9 100644
--- a/tests/spec/extend_extern.ml
+++ b/tests/spec/extend_extern.ml
@@ -17,7 +17,7 @@ let typer typing_context loc lexprs =
 
 
 let () =
-  Acsl_extension.(register_global "why3" (make ~typer ()))
+  Acsl_extension.register_global "why3" typer false
 
 let main () =
   try
diff --git a/tests/spec/oracle/Extend_short_print.res.oracle b/tests/spec/oracle/Extend_short_print.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..fe5db7f43bb5a79133f053670e2301e6c677ed57
--- /dev/null
+++ b/tests/spec/oracle/Extend_short_print.res.oracle
@@ -0,0 +1,3 @@
+[kernel] Parsing tests/spec/Extend_short_print.i (no preprocessing)
+[kernel] with_short: some content
+[kernel] without_short