diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index b86e9200489ea822f2dfb2315a2d5134b2bfd3b3..d31c8c679e07a341b20cddc5c021497c6a766392 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -207,7 +207,12 @@
             match Logic_env.extension_category s with
             | exception Not_found -> None
             | Cil_types.Ext_contract -> Some (EXT_CONTRACT s)
-            | Cil_types.Ext_global -> Some (EXT_GLOBAL s)
+            | Cil_types.Ext_global ->
+              begin
+                match Logic_env.is_extension_block s with
+                | false -> Some (EXT_GLOBAL s)
+                | true -> Some (EXT_GLOBAL_BLOCK s)
+              end
             | Cil_types.Ext_code_annot _ -> Some (EXT_CODE_ANNOT s)
           end
           else None
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 0bff4b69eda3bb3a77ca80cddbc3294ddbc2acfb..121ad96facc0f37bf6de65c4c7f03e57953649fb 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -107,6 +107,8 @@
 
   let loc_decl d = { decl_node = d; decl_loc = loc () }
 
+  let loc_ext d = { extended_node = d; extended_loc = loc () }
+
   let concat_froms a1 a2 =
     let compare_pair (b1,_) (b2,_) = is_same_lexpr b1 b2 in
     (* NB: the following has an horrible complexity, but the order of
@@ -253,7 +255,7 @@
 %token REQUIRES ENSURES ALLOCATES FREES ASSIGNS LOOP NOTHING SLICE IMPACT PRAGMA FROM
 %token CHECK_REQUIRES CHECK_LOOP CHECK_INVARIANT CHECK_LEMMA
 %token CHECK_ENSURES CHECK_EXITS CHECK_CONTINUES CHECK_BREAKS CHECK_RETURNS
-%token <string> EXT_CODE_ANNOT EXT_GLOBAL EXT_CONTRACT
+%token <string> EXT_CODE_ANNOT EXT_GLOBAL EXT_GLOBAL_BLOCK EXT_CONTRACT
 %token EXITS BREAKS CONTINUES RETURNS
 %token VOLATILE READS WRITES
 %token LOGIC PREDICATE INDUCTIVE AXIOMATIC AXIOM LEMMA LBRACE RBRACE
@@ -1532,13 +1534,34 @@ decl:
 | type_annot {LDtype_annot $1}
 | model_annot {LDmodel_annot $1}
 | logic_def  { $1 }
-| EXT_GLOBAL grammar_extension SEMICOLON {
-    let processed = Logic_env.preprocess_extension $1 $2 in
-	  LDextended ($1, processed)
-  }
+| ext_decl { LDextended $1 }
 | deprecated_logic_decl { $1 }
 ;
 
+ext_decl:
+| EXT_GLOBAL grammar_extension SEMICOLON {
+     let processed = Logic_env.preprocess_extension $1 $2 in
+     Ext_lexpr($1, processed)
+   }
+| EXT_GLOBAL_BLOCK any_identifier LBRACE ext_decls RBRACE {
+    let processed_id,processed_block =
+       Logic_env.preprocess_extension_block $1 ($2,$4)
+    in
+    Ext_extension($1,processed_id,processed_block)
+   }
+;
+
+ext_decls:
+| /* epsilon */
+    { [] }
+| ext_decl_loc ext_decls
+    { $1::$2 }
+;
+
+ext_decl_loc:
+| ext_decl { loc_ext $1 }
+;
+
 volatile_opt:
 | /* empty */ { None, None }
 | READS any_identifier volatile_opt
@@ -1893,6 +1916,7 @@ is_acsl_spec:
 is_acsl_decl_or_code_annot:
 | EXT_CODE_ANNOT { $1 }
 | EXT_GLOBAL     { $1 }
+| EXT_GLOBAL_BLOCK     { $1 }
 | ASSUMES   { "assumes" }
 | ASSERT    { "assert" }
 | CHECK     { "check" }
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index 805f4e06efe13270078d3163e9eca76ef90a9d8c..ed8914b346ec1c47a40f6f8dbb8cf3c21b932e12 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -442,28 +442,35 @@ let hash_list f l =
     | _ -> acc
   in aux 47 3 l
 
-let hash_ext_kind = function
-  | Ext_id i -> Datatype.Int.hash i
-  | Ext_terms terms -> 29 * (hash_list Logic_utils.hash_term terms)
-  | Ext_preds preds -> 47 * (hash_list Logic_utils.hash_predicate preds)
-
-let compare_ext_kind k1 k2 =
-  match k1, k2 with
-  | Ext_id i1, Ext_id i2 -> Datatype.Int.compare i1 i2
-  | Ext_id _, _ -> 1 | _, Ext_id _ -> -1
-  | Ext_terms terms1, Ext_terms terms2 ->
-    Extlib.list_compare Logic_utils.compare_term terms1 terms2
-  | Ext_terms _, _ -> 1 | _, Ext_terms _ -> -1
-  | Ext_preds p1, Ext_preds p2 ->
-    Extlib.list_compare Logic_utils.compare_predicate p1 p2
 
 module ExtMerging =
   Merging
     (struct
       type t = acsl_extension
-      let hash (e : acsl_extension) =
+      let rec hash (e : acsl_extension) =
+        let hash_ext_kind = function
+          | Ext_id i -> Datatype.Int.hash i
+          | Ext_terms terms -> 29 * (hash_list Logic_utils.hash_term terms)
+          | Ext_preds preds -> 47 * (hash_list Logic_utils.hash_predicate preds)
+          | Ext_annot (id, annots) -> Datatype.String.hash id + 5 * (hash_list hash annots)
+        in
         Datatype.String.hash e.ext_name + 5 * hash_ext_kind e.ext_kind
-      let compare (e1 : acsl_extension) (e2 : acsl_extension) =
+      let rec compare (e1 : acsl_extension) (e2 : acsl_extension) =
+        let compare_ext_kind k1 k2 =
+          match k1, k2 with
+          | Ext_id i1, Ext_id i2 -> Datatype.Int.compare i1 i2
+          | Ext_id _, _ -> 1 | _, Ext_id _ -> -1
+          | Ext_terms terms1, Ext_terms terms2 ->
+            Extlib.list_compare Logic_utils.compare_term terms1 terms2
+          | Ext_terms _, _ -> 1 | _, Ext_terms _ -> -1
+          | Ext_preds p1, Ext_preds p2 ->
+            Extlib.list_compare Logic_utils.compare_predicate p1 p2
+          | Ext_preds _, _ -> 1 | _, Ext_preds _ -> -1
+          | Ext_annot (id1, a1) , Ext_annot (id2, a2)  ->
+            match String.compare id1 id2 with
+            | 0 -> Extlib.list_compare compare a1 a2
+            | n -> n
+        in
         let res = Datatype.String.compare e1.ext_name e2.ext_name in
         if res <> 0 then res
         else
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index 48697d89dc5e74e9dd3ad936c88e7d7fec533d60..cc512a4d869da24ad9799974c91b3fd315a50cb0 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -1693,6 +1693,7 @@ and acsl_extension_kind =
   | Ext_terms of term list
   | Ext_preds of predicate list
   (** a list of predicates, the most common case of for extensions *)
+  | Ext_annot of string * acsl_extension list
 
 (** Where are we expected to find corresponding extension keyword.
     @plugin development guide
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index 9f6037a6b458b499e19b3051d4bdfc883bfb8b8a..9ce30a3dac134d87e8e65424eae08e7e4d8f2276 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -921,6 +921,8 @@ and pp_acsl_extension_kind fmt = function
   | Ext_id(int) -> Format.fprintf fmt "Ext_id(%a)"  pp_int int
   | Ext_terms(term_list) -> Format.fprintf fmt "Ext_terms(%a)"  (pp_list pp_term) term_list
   | Ext_preds(predicate_list) -> Format.fprintf fmt "Ext_preds(%a)"  (pp_list pp_predicate) predicate_list
+  | Ext_annot(string,annotation_list) ->
+    Format.fprintf fmt "Ext_annots(%a,%a)" pp_string string (pp_list pp_acsl_extension) annotation_list
 
 and pp_behavior fmt behavior =
   Format.fprintf fmt
diff --git a/src/kernel_services/ast_printing/logic_print.ml b/src/kernel_services/ast_printing/logic_print.ml
index 1b3c0544fc39e38fce56da4f47fe2a8dae606f60..59f6809727dcdd724cb9b841d531c7f072164fa8 100644
--- a/src/kernel_services/ast_printing/logic_print.ml
+++ b/src/kernel_services/ast_printing/logic_print.ml
@@ -311,6 +311,15 @@ let print_model_annot fmt ty =
     (print_logic_type None) ty.model_type
     ty.model_name
 
+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) ->
+    fprintf fmt "@[<2>%s@ %a@]" name (pp_list ~sep:",@ " print_lexpr) d
+  | Ext_extension(name,id,d) ->
+    fprintf fmt "@[<2>%s@ %s@ {@\n%a@]@\n}" name id
+      (pp_list ~sep:"@\n" aux) d
+
 let rec print_decl fmt d =
   match d.decl_node with
   | LDlogic_def(name,labels,tvar,rt,prms,body) ->
@@ -374,8 +383,7 @@ let rec print_decl fmt d =
       (pp_list ~pre:"@[" ~sep:",@ " ~suf:"@]" print_lexpr) tsets
       (pp_opt ~pre:"@ reads@ " pp_print_string) read
       (pp_opt ~pre:"@ writes@ " pp_print_string) write
-  | LDextended (s,l) ->
-    fprintf fmt "@[<2>%s@ %a@]" s (pp_list ~sep:",@ " print_lexpr) l
+  | LDextended d -> print_extended_decl fmt d
 
 let print_deps fmt deps =
   match deps with
diff --git a/src/kernel_services/ast_queries/acsl_extension.ml b/src/kernel_services/ast_queries/acsl_extension.ml
index ff6f3c5060c832a34dcd6fb930718b95a4b0a352..5132e3e1540275b6b489bf52fec1e023e9a3d864 100644
--- a/src/kernel_services/ast_queries/acsl_extension.ml
+++ b/src/kernel_services/ast_queries/acsl_extension.ml
@@ -28,16 +28,36 @@ type extension_preprocessor =
   lexpr list -> lexpr list
 type extension_typer =
   typing_context -> location -> lexpr list -> acsl_extension_kind
+type extension_preprocessor_block =
+  string * extended_decl list -> string * extended_decl list
+type extension_typer_block =
+  typing_context -> location -> string * extended_decl list -> acsl_extension_kind
 type extension_visitor =
   Cil.cilVisitor -> acsl_extension_kind -> acsl_extension_kind Cil.visitAction
 type extension_printer =
   Printer_api.extensible_printer_type -> Format.formatter ->
   acsl_extension_kind -> unit
-type extension = {
-  category: ext_category ;
+type extension_single = {
+  preprocessor: extension_preprocessor ;
+  typer: extension_typer ;
   status: bool ;
+}
+type extension_block = {
+  preprocessor: extension_preprocessor_block ;
+  typer: extension_typer_block ;
+  status: bool ;
+}
+type extension_common = {
+  category: ext_category ;
+  visitor: extension_visitor ;
+  printer: extension_printer ;
+  short_printer: extension_printer ;
+}
+type extension = {
   preprocessor: extension_preprocessor ;
   typer: extension_typer ;
+  status: bool ;
+  category: ext_category ;
   visitor: extension_visitor ;
   printer: extension_printer ;
   short_printer: extension_printer ;
@@ -47,9 +67,10 @@ 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
+  | Ext_annot (_,an) -> Pretty_utils.pp_list ~pre:"@[<v 0>" ~suf:"@]@\n" ~sep:"@\n"
+                          printer#extended fmt an
 
-let default_short_printer name _printer fmt _ext_kind =
-  Format.fprintf fmt "%s" name
+let default_short_printer name _printer fmt _ext_kind = Format.fprintf fmt "%s" name
 
 let make
     name category
@@ -58,15 +79,39 @@ let make
     ?(visitor=fun _ _ -> Cil.DoChildren)
     ?(printer=default_printer)
     ?(short_printer=default_short_printer name)
-    status =
-  { category; status; preprocessor; typer; visitor; printer; short_printer }
+    status : extension_single*extension_common =
+  { preprocessor; typer; status},{ category; visitor; printer; short_printer }
+
+let make_block
+    name category
+    ?(preprocessor=Extlib.id)
+    typer
+    ?(visitor=fun _ _ -> Cil.DoChildren)
+    ?(printer=default_printer)
+    ?(short_printer=default_short_printer name)
+    status : extension_block*extension_common =
+  { preprocessor; typer; status},{ category; visitor; printer; short_printer }
 
 module Extensions = struct
+  (*hash table for  category, visitor, printer and short_printer of extensions*)
   let ext_tbl = Hashtbl.create 5
 
-  let find name =
-    try Hashtbl.find ext_tbl name
-    with Not_found ->
+  (*hash table for status, preprocessor and typer of single extensions*)
+  let ext_single_tbl = Hashtbl.create 5
+
+  (*hash table for status, preprocessor and typer of block extensions*)
+  let ext_block_tbl = Hashtbl.create 5
+
+  let find_single name :extension_single =
+    try Hashtbl.find ext_single_tbl name with Not_found ->
+      Kernel.fatal ~current:true "unsupported clause of name '%s'" name
+
+  let find_common name :extension_common =
+    try Hashtbl.find ext_tbl name with Not_found ->
+      Kernel.fatal ~current:true "unsupported clause of name '%s'" name
+
+  let find_block name :extension_block =
+    try Hashtbl.find ext_block_tbl name with Not_found ->
       Kernel.fatal ~current:true "unsupported clause of name '%s'" name
 
   (* [Logic_lexer] can ask for something that is not a category, which is not
@@ -75,21 +120,60 @@ module Extensions = struct
 
   let is_extension = Hashtbl.mem ext_tbl
 
+  let is_extension_block = Hashtbl.mem ext_block_tbl
+
   let register
       cat name ?preprocessor typer ?visitor ?printer ?short_printer status =
-    let info =
+    let info1,info2 =
       make name 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 info
+    else
+      begin
+        Hashtbl.add ext_single_tbl name info1;
+        Hashtbl.add ext_tbl name info2
+      end
 
-  let preprocess name = (find name).preprocessor
+  let register_block
+      cat name ?preprocessor typer ?visitor ?printer ?short_printer status =
+    let info1,info2 =
+      make_block name 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
+      begin
+        Hashtbl.add ext_block_tbl name info1;
+        Hashtbl.add ext_tbl name info2
+      end
+
+  let preprocess name = (find_single name).preprocessor
+
+  let preprocess_block name = (find_block name).preprocessor
 
   let typing name typing_context loc es =
-    let ext_info = find name in
+    let ext_info = find_single name in
+    let status = ext_info.status in
+    let typer =  ext_info.typer 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 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 typing_block name typing_context loc es =
+    let ext_info = find_block name in
     let status = ext_info.status in
     let typer =  ext_info.typer in
     let normal_error = ref false in
@@ -104,14 +188,18 @@ module Extensions = struct
       Kernel.fatal "Typechecking ACSL extension %s raised exception %s"
         name (Printexc.to_string exn)
 
-  let visit name = (find name).visitor
+  let visit name = (find_common 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 pp = (find_common name).printer printer in
+    match kind with
+    | Ext_annot (id,_) ->
+      Format.fprintf fmt "@[<v 2>@[%s %s {@]@\n%a}@]" name id pp kind
+    | _ ->
+      Format.fprintf fmt "@[<hov 2>%s %a;@]" name pp kind
 
   let short_print name printer fmt kind =
-    let pp = (find name).short_printer in
+    let pp = (find_common name).short_printer in
     Format.fprintf fmt "%a" (pp printer) kind
 end
 
@@ -121,6 +209,8 @@ let register_behavior =
   Extensions.register Ext_contract
 let register_global =
   Extensions.register Ext_global
+let register_global_block =
+  Extensions.register_block Ext_global
 let register_code_annot =
   Extensions.register (Ext_code_annot Ext_here)
 let register_code_annot_next_stmt =
@@ -136,10 +226,13 @@ let () =
   Logic_env.set_extension_handler
     ~category:Extensions.category
     ~is_extension: Extensions.is_extension
-    ~preprocess: Extensions.preprocess ;
+    ~preprocess: Extensions.preprocess
+    ~is_extension_block: Extensions.is_extension_block
+    ~preprocess_block: Extensions.preprocess_block;
   Logic_typing.set_extension_handler
     ~is_extension: Extensions.is_extension
-    ~typer: Extensions.typing ;
+    ~typer: Extensions.typing
+    ~typer_block: Extensions.typing_block ;
   Cil.set_extension_handler
     ~visit: Extensions.visit ;
   Cil_printer.set_extension_handler
@@ -148,21 +241,45 @@ let () =
 
 (* For Deprecation: *)
 
-let deprecated_replace name ext = Hashtbl.add Extensions.ext_tbl name ext
+let deprecated_replace name ext =
+  let info1:extension_single = {
+    preprocessor = ext.preprocessor ;
+    typer = ext.typer ;
+    status = ext.status ;
+  }
+  in
+  let info2:extension_common  = {
+    category = ext.category ;
+    visitor = ext.visitor ;
+    printer = ext.printer ;
+    short_printer = ext.printer ;
+  }
+  in
+  Hashtbl.add Extensions.ext_single_tbl name info1;
+  Hashtbl.add Extensions.ext_tbl name info2
 
 let strong_cat = Hashtbl.create 5
 
 let default_typer _typing_context _loc _l = assert false
 
+let merge ((info1:extension_single),(info2:extension_common)) :extension =
+  {preprocessor = info1.preprocessor ;
+   typer = info1.typer ;
+   status = info1.status ;
+   category = info2.category ;
+   visitor = info2.visitor ;
+   printer = info2.printer ;
+   short_printer = info2.printer}
 
 let deprecated_find ?(strong=true) name cat op_name =
-  match Hashtbl.find_opt Extensions.ext_tbl name with
+  match Hashtbl.find_opt Extensions.ext_single_tbl name with
   | None ->
     if strong then Hashtbl.add strong_cat name cat ;
-    (make name cat default_typer false)
-  | Some ext ->
+    merge (make name cat default_typer false)
+  | Some ext1 ->
+    let ext2 = Extensions.find_common name in
     if strong && Hashtbl.mem strong_cat name then begin
-      if ext.category = cat then ext
+      if ext2.category = cat then merge (ext1,ext2)
       else
         Kernel.fatal
           "Registring %s for %s: this extension already exists for another \
@@ -170,8 +287,9 @@ let deprecated_find ?(strong=true) name cat op_name =
           op_name name
     end else if strong then begin
       Hashtbl.add strong_cat name cat ;
-      { ext with category = cat }
-    end else ext
+      let ext2 = { ext2 with category = cat } in
+      merge (ext1,ext2)
+    end else merge (ext1,ext2)
 
 let deprecated_register_typing name cat status typer =
   deprecated_replace name
diff --git a/src/kernel_services/ast_queries/acsl_extension.mli b/src/kernel_services/ast_queries/acsl_extension.mli
index c2778433fb9c698c286e9948931363602a2a0b71..c615564b73e848de661706e29db19b63f931fbed 100644
--- a/src/kernel_services/ast_queries/acsl_extension.mli
+++ b/src/kernel_services/ast_queries/acsl_extension.mli
@@ -38,6 +38,10 @@ type extension_typer =
 (** Visitor functions for ACSL extensions *)
 type extension_visitor =
   Cil.cilVisitor -> acsl_extension_kind -> acsl_extension_kind Cil.visitAction
+type extension_preprocessor_block =
+  string * extended_decl list -> string * extended_decl list
+type extension_typer_block =
+  typing_context -> location -> string * extended_decl list -> acsl_extension_kind
 (** Pretty printers for ACSL extensions *)
 type extension_printer =
   Printer_api.extensible_printer_type -> Format.formatter ->
@@ -106,6 +110,16 @@ val register_global:
   ?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
   unit
 
+(** Registers extension for global block annotation. See [register_behavior].
+
+    @plugin development guide
+*)
+val register_global_block:
+  string -> ?preprocessor:extension_preprocessor_block -> extension_typer_block ->
+  ?visitor:extension_visitor ->
+  ?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
+  unit
+
 (** Registers extension for code annotation to be evaluated at _current_
     program point. See [register_behavior].
 
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 04582c3557e7c494163aa7e400bbd6ad1c7753b9..6f90ae11d735c7169a1ca90de6324221969f744b 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -1994,6 +1994,9 @@ and childrenCilExtended vis p =
   | Ext_preds preds ->
     let preds' = mapNoCopy (visitCilPredicate vis) preds in
     if preds == preds' then p else Ext_preds preds'
+  | Ext_annot (id,annots) ->
+    let annots' = mapNoCopy (visitCilExtended vis) annots in
+    if annots == annots' then p else Ext_annot (id,annots')
 
 and visitCilPredicates vis ps = mapNoCopy (visitCilIdPredicate vis) ps
 
diff --git a/src/kernel_services/ast_queries/logic_env.ml b/src/kernel_services/ast_queries/logic_env.ml
index dde299d846e9cc6cf30d75365c928ca4e4b006cd..18381986562fe7c5de69f1f331691a93e229792b 100644
--- a/src/kernel_services/ast_queries/logic_env.ml
+++ b/src/kernel_services/ast_queries/logic_env.ml
@@ -29,23 +29,32 @@ module Extensions = struct
   let ref_is_extension = ref (fun _ -> assert false)
   let ref_category = ref (fun _ -> assert false)
   let ref_preprocess = ref (fun _ -> assert false)
+  let ref_is_extension_block = ref (fun _ -> assert false)
+  let ref_preprocess_block = ref (fun _ -> assert false)
 
-  let set_extension_handler ~category ~is_extension ~preprocess =
+  let set_extension_handler
+      ~category ~is_extension ~preprocess ~is_extension_block ~preprocess_block =
     assert (not !initialized) ;
     ref_is_extension := is_extension ;
     ref_category := category ;
     ref_preprocess := preprocess ;
+    ref_is_extension_block := is_extension_block;
+    ref_preprocess_block := preprocess_block;
     initialized := true ;
     ()
 
   let is_extension s = !ref_is_extension s
+  let is_extension_block s = !ref_is_extension_block s
   let category s = !ref_category s
   let preprocess s = !ref_preprocess s
+  let preprocess_block s = !ref_preprocess_block s
 end
 let set_extension_handler = Extensions.set_extension_handler
 let is_extension = Extensions.is_extension
+let is_extension_block = Extensions.is_extension_block
 let extension_category = Extensions.category
 let preprocess_extension = Extensions.preprocess
+let preprocess_extension_block = Extensions.preprocess_block
 
 module CurrentLoc = Cil_const.CurrentLoc
 
diff --git a/src/kernel_services/ast_queries/logic_env.mli b/src/kernel_services/ast_queries/logic_env.mli
index 407ac539994274396bfb7ae3a489e1615fa4037e..954eb3645d1e73961b39b7cb1e0c11a9ab2cb0ff 100644
--- a/src/kernel_services/ast_queries/logic_env.mli
+++ b/src/kernel_services/ast_queries/logic_env.mli
@@ -29,12 +29,16 @@ open Cil_types
 (** {2 registered ACSL extensions } *)
 
 val is_extension: string -> bool
+val is_extension_block: string -> bool
 
 val extension_category: string -> ext_category
 
 val preprocess_extension:
   string -> Logic_ptree.lexpr list -> Logic_ptree.lexpr list
 
+val preprocess_extension_block:
+  string -> string * Logic_ptree.extended_decl list -> string * Logic_ptree.extended_decl list
+
 (** {2 Global Tables} *)
 module Logic_info: State_builder.Hashtbl
   with type key = string and type data = Cil_types.logic_info list
@@ -208,6 +212,10 @@ val set_extension_handler:
   category:(string -> ext_category) ->
   is_extension:(string -> bool) ->
   preprocess:(string -> Logic_ptree.lexpr list -> Logic_ptree.lexpr list) ->
+  is_extension_block:(string -> bool) ->
+  preprocess_block:
+    (string -> string * Logic_ptree.extended_decl list ->
+     string * Logic_ptree.extended_decl list) ->
   unit
 (** Used to setup references 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_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 477044c55237b2a176287a24d50381468bf41ab8..fcf4ab3aed662c046f0a69f2489eeb554f5ce7a3 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -528,11 +528,13 @@ module Extensions = struct
   let initialized = ref false
   let ref_is_extension = ref (fun _ -> assert false)
   let ref_typer = ref (fun _ _ _ _ -> assert false)
+  let ref_typer_block = ref (fun _ _ _ _ -> assert false)
 
-  let set_handler ~is_extension ~typer =
+  let set_handler ~is_extension ~typer ~typer_block =
     assert (not !initialized) ;
     ref_is_extension := is_extension ;
     ref_typer := typer ;
+    ref_typer_block := typer_block;
     initialized := true
 
   let is_extension name = !ref_is_extension name
@@ -540,6 +542,9 @@ module Extensions = struct
   let typer name ~typing_context:typing_context ~loc =
     !ref_typer name typing_context loc
 
+  let typer_block name ~typing_context:typing_context ~loc =
+    !ref_typer_block name typing_context loc
+
   (* For deprecated functions *)
   let ref_deprecated_handler = ref (fun _ _ _ _  -> assert false)
 
@@ -551,6 +556,8 @@ module Extensions = struct
     !ref_deprecated_handler name category status typer
 end
 let set_extension_handler = Extensions.set_handler
+let get_typer = Extensions.typer
+let get_typer_block = Extensions.typer_block
 
 (* Deprecated ACSL extensions functions *)
 let set_deprecated_extension_handler =
@@ -4281,11 +4288,18 @@ struct
       let rvi_opt = get_volatile_fct checks_reads_fct rd_opt in
       let wvi_opt = get_volatile_fct checks_writes_fct wr_opt in
       Dvolatile (tsets, rvi_opt, wvi_opt, [], loc)
-    | LDextended (kind, content) ->
+    | LDextended (Ext_lexpr(kind, 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
       Dextended (textended, [], loc)
+    | LDextended (Ext_extension (kind, name, content)) ->
+      let typing_context = base_ctxt (Lenv.empty ()) in
+      let status,tcontent =
+        Extensions.typer_block kind ~typing_context ~loc (name,content)
+      in
+      let textended = Logic_const.new_acsl_extension kind loc status tcontent in
+      Dextended (textended, [], loc)
 
   let annot a =
     start_transaction ();
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index 3c4c2975d97d17cb65670013dba178c55868ccf5..e1c613d9e297cac4e1fdc8a18ab8a31489934bf3 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -389,12 +389,29 @@ val set_extension_handler:
   is_extension:(string -> bool) ->
   typer:(string -> typing_context -> location -> Logic_ptree.lexpr list ->
          (bool * acsl_extension_kind)) ->
+  typer_block:(string -> typing_context ->
+               Filepath.position * Filepath.position ->
+               string * Logic_ptree.extended_decl list ->
+               bool * Cil_types.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 21.0-Scandium
 *)
 
+val get_typer :
+  string ->
+  typing_context:typing_context ->
+  loc:Filepath.position * Filepath.position ->
+  Logic_ptree.lexpr list -> bool * Cil_types.acsl_extension_kind
+
+val get_typer_block:
+  string ->
+  typing_context:typing_context ->
+  loc:Logic_ptree.location ->
+  string * Logic_ptree.extended_decl list ->
+  bool * Cil_types.acsl_extension_kind
+
 (**/**)
 val set_deprecated_extension_handler:
   handler:(string -> ext_category -> bool ->
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 7fd192b397eb99793a3374823b60c8b13786f505..acdcb97f4f8e164586cf04ede5818b183dbf9f07 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -1186,7 +1186,7 @@ let is_same_pragma p1 p2 =
   | Impact_pragma p1, Impact_pragma p2 -> is_same_impact_pragma p1 p2
   | (Loop_pragma _ | Slice_pragma _ | Impact_pragma _), _ -> false
 
-let is_same_extension x1 x2 =
+let rec is_same_extension x1 x2 =
   Datatype.String.equal x1.ext_name x2.ext_name &&
   (x1.ext_has_status = x2.ext_has_status) &&
   match x1.ext_kind, x2.ext_kind with
@@ -1195,7 +1195,9 @@ let is_same_extension x1 x2 =
     is_same_list is_same_term t1 t2
   | Ext_preds p1, Ext_preds p2 ->
     is_same_list is_same_predicate p1 p2
-  | (Ext_id _ | Ext_preds _ | Ext_terms _), _ -> false
+  | Ext_annot (id1, a1), Ext_annot (id2, a2) ->
+    is_same_string id1 id2 && is_same_list is_same_extension a1 a2
+  | (Ext_id _ | Ext_preds _ | Ext_terms _ | Ext_annot _ ), _ -> false
 
 let is_same_code_annotation (ca1:code_annotation) (ca2:code_annotation) =
   match ca1.annot_content, ca2.annot_content with
diff --git a/src/kernel_services/parsetree/logic_ptree.mli b/src/kernel_services/parsetree/logic_ptree.mli
index bff3332bb8dff7075b6aedd448b7caecbfb70469..ccc7a1d24afbf114b911e6d3a33ab74748ec6e48 100644
--- a/src/kernel_services/parsetree/logic_ptree.mli
+++ b/src/kernel_services/parsetree/logic_ptree.mli
@@ -248,7 +248,8 @@ and decl_node =
   | LDmodel_annot of model_annot    (** model field. *)
   | LDvolatile of lexpr list * (string option * string option)
       (** volatile clause read/write. *)
-  | LDextended of extension (** extended global annotation. *)
+  | LDextended of global_extension (** extended global annotation. *)
+
 
 (** dependencies of an assigned location. *)
 and deps =
@@ -273,6 +274,15 @@ and allocation =
 (** variant of a loop or a recursive function. *)
 and variant = lexpr * string option
 
+and global_extension =
+  | Ext_lexpr of string * lexpr list
+  | Ext_extension of string * string * extended_decl list
+
+and extended_decl = {
+  extended_node : global_extension;
+  extended_loc : location
+}
+
 (** Behavior in a specification. This type shares the name of its constructors
     with {!Cil_types.behavior}. *)
 type behavior = {
diff --git a/src/plugins/value/utils/widen_hints_ext.ml b/src/plugins/value/utils/widen_hints_ext.ml
index bcf81060871baa6be4ebedb8cc8b013dfb035a51..449c0c6752086703c4c64693744deefdf8414abd 100644
--- a/src/plugins/value/utils/widen_hints_ext.ml
+++ b/src/plugins/value/utils/widen_hints_ext.ml
@@ -148,6 +148,7 @@ let printer _pp fmt ext =
   match ext with
   | Ext_id _ -> assert false
   | Ext_preds _ -> assert false
+  | Ext_annot _ -> assert false
   | Ext_terms terms ->
     match widen_hint_terms_of_terms terms with
     | Some (hint_lval, hint_terms) ->
diff --git a/tests/spec/Extend.ml b/tests/spec/Extend.ml
index 71fcdbdc871433955ef45aa232fd62b5f0c3b93b..af1f9f6510af20f330150938ce0703849e464a3c 100644
--- a/tests/spec/Extend.ml
+++ b/tests/spec/Extend.ml
@@ -40,7 +40,7 @@ let print_bar prt fmt ext =
     let l = Bar_table.find idx in
     Pretty_utils.pp_list
       ~pre:"@[<hov 2>" ~sep:",@ " ~suf:"@]" prt#predicate fmt l
-  | Ext_preds _ | Ext_terms _ ->
+  | Ext_preds _ | Ext_terms _ | Ext_annot _->
     Kernel.fatal "bar extension should have ids as arguments"
 
 let visit_bar vis ext =
@@ -56,7 +56,7 @@ let visit_bar vis ext =
       Bar_table.replace idx l';
       Cil.SkipChildren
     end
-  | Ext_terms _ | Ext_preds _ ->
+  | Ext_terms _ | Ext_preds _ | Ext_annot _ ->
       Kernel.fatal "bar extension should have ids as arguments"
 
 let type_baz typing_context _loc l =
diff --git a/tests/spec/Extend_recursive_preprocess.i b/tests/spec/Extend_recursive_preprocess.i
new file mode 100644
index 0000000000000000000000000000000000000000..319f9310fa3a995bdca92dff5499c6d5e940bd69
--- /dev/null
+++ b/tests/spec/Extend_recursive_preprocess.i
@@ -0,0 +1,34 @@
+/* run.config
+MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+OPT: -no-autoload-plugins -kernel-warn-key=annot-error=active -print
+*/
+
+/*@ gl_foo foo1 {
+    gl_fooo must_replace(x);
+    gl_fooo must_not_replace(x);
+    gl_fooo must_replace(x);
+}*/
+
+
+/*@ gl_foo foo1 {
+    gl_foo foo2 {
+      gl_fooo must_replace(x);
+      gl_fooo must_not_replace(x);
+    }
+}*/
+
+/*@ gl_foo foo1 {
+    gl_fooo must_replace(x);
+    gl_foo foo2 {
+      gl_fooo must_replace(x);
+      gl_foo foo3 {
+         gl_fooo must_replace(x);
+	 gl_fooo must_not_replace(x);
+      }
+      gl_fooo must_replace(x);
+    }
+    gl_fooo must_not_replace(x);
+
+}*/
+
+//frama-c -no-autoload-plugins -kernel-warn-key=annot-error=active -print -load-script Extend_recursive_preprocess.ml Extend_recursive_preprocess.i
diff --git a/tests/spec/Extend_recursive_preprocess.ml b/tests/spec/Extend_recursive_preprocess.ml
new file mode 100644
index 0000000000000000000000000000000000000000..f56767b5cc5aed48608d55bcb89e5c721472d175
--- /dev/null
+++ b/tests/spec/Extend_recursive_preprocess.ml
@@ -0,0 +1,83 @@
+open Logic_ptree
+open Logic_const
+open Cil_types
+
+let ext_typing_fooo _typing_context _loc l =
+  let type_lexpr = function
+    | { lexpr_node = PLapp("gl_foo_ok", [], [ _ ]) } -> ptrue
+    | { lexpr_node = PLapp("gl_foo_ko", [], [ _ ]) } -> pfalse
+    | _ -> assert false
+  in
+  Cil_types.Ext_preds (List.map type_lexpr l)
+
+let ext_typing_block typing_context loc_here node =
+  match node.extended_node with
+  | Ext_lexpr (name,data)  ->
+    let status,kind = Logic_typing.get_typer name typing_context node.extended_loc data in
+    Logic_const.new_acsl_extension name loc_here status kind
+  | Ext_extension (name, id, data) ->
+    let status,kind = Logic_typing.get_typer_block name typing_context node.extended_loc (id,data) in
+    Logic_const.new_acsl_extension name loc_here status kind
+
+let  ext_typing_foo typing_context loc (s,d) =
+  let block = List.map (ext_typing_block typing_context loc) d in
+  Cil_types.Ext_annot (s,block)
+
+let preprocess_fooo_ptree_element = function
+  | { lexpr_node = PLapp("must_replace", [], [ v ]) } as x ->
+    { x with lexpr_node = PLapp("gl_foo" ^ "_ok", [], [ v ]) }
+  | { lexpr_node = PLapp("must_not_replace", [], [ v ]) } as x ->
+    { x with lexpr_node = PLapp("gl_foo" ^ "_ko", [], [ v ]) }
+  | _ -> assert false
+
+let preprocess_fooo_ptree = List.map preprocess_fooo_ptree_element
+
+let preprocess_foo_ptree (id,data) = (id ^ "_ok",data)
+
+let ext_fooo_visitor vis ext =
+  let aux p = unamed (Pand(p,p)) in
+  match ext with
+  | Ext_preds pred ->
+    if Visitor_behavior.is_copy vis#behavior then
+      Cil.ChangeTo (Ext_preds (List.map aux pred))
+    else
+      Cil.DoChildren
+  | _ -> assert false
+
+let ext_foo_visitor vis ext =
+  match ext with
+  | Ext_annot _ ->
+    if Visitor_behavior.is_copy vis#behavior then
+      Cil.DoChildrenPost (fun ext ->
+          match ext with
+          | Ext_annot(s, l) -> Ext_annot(s ^ "_ok", l)
+          | _ -> ext)
+    else
+      Cil.DoChildren
+  | _ -> assert false
+
+let ext_fooo_printer prt fmt ext =
+  match ext with
+  | Ext_preds ps ->
+    Pretty_utils.pp_list ~pre:"@[data:" ~sep:",@ " prt#predicate fmt ps
+  | _ -> assert false
+
+let () =  Acsl_extension.register_global
+    "gl_fooo" ~preprocessor:preprocess_fooo_ptree ext_typing_fooo
+    ~printer:ext_fooo_printer ~visitor:ext_fooo_visitor false ;
+  Acsl_extension.register_global_block
+    "gl_foo" ~preprocessor:preprocess_foo_ptree ext_typing_foo
+                              ~visitor:ext_foo_visitor false
+
+let run () =
+  let old = Project.current () in
+  let vis prj = new Visitor.frama_c_copy prj in
+  let final_project =
+    File.create_project_from_visitor ~reorder:true "Test" vis
+  in
+  Project.set_current final_project;
+  File.pretty_ast ();
+  Filecheck.check_ast "Test";
+  Project.set_current old
+
+let () = Db.Main.extend run
diff --git a/tests/spec/oracle/Extend_recursive_preprocess.res.oracle b/tests/spec/oracle/Extend_recursive_preprocess.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..73af51bd109cdddc1b864db092bf7826a23bbee6
--- /dev/null
+++ b/tests/spec/oracle/Extend_recursive_preprocess.res.oracle
@@ -0,0 +1,62 @@
+[kernel] Parsing tests/spec/Extend_recursive_preprocess.i (no preprocessing)
+/* Generated by Frama-C */
+/*@
+gl_foo foo1_ok_ok {
+  gl_fooo data:\true ∧ \true;
+  gl_fooo data:\false ∧ \false;
+  gl_fooo data:\true ∧ \true;
+  }
+*/
+/*@
+gl_foo foo1_ok_ok {
+  gl_foo foo2_ok_ok {
+    gl_fooo data:\true ∧ \true;
+    gl_fooo data:\false ∧ \false;
+    }
+  }
+*/
+/*@
+gl_foo foo1_ok_ok {
+  gl_fooo data:\true ∧ \true;
+  gl_foo foo2_ok_ok {
+    gl_fooo data:\true ∧ \true;
+    gl_foo foo3_ok_ok {
+      gl_fooo data:\true ∧ \true;
+      gl_fooo data:\false ∧ \false;
+      }
+    gl_fooo data:\true ∧ \true;
+    }
+  gl_fooo data:\false ∧ \false;
+  }
+*/
+
+/* Generated by Frama-C */
+/*@
+gl_foo foo1_ok {
+  gl_fooo data:\true;
+  gl_fooo data:\false;
+  gl_fooo data:\true;
+  }
+*/
+/*@ gl_foo foo1_ok {
+      gl_foo foo2_ok {
+        gl_fooo data:\true;
+        gl_fooo data:\false;
+        }
+      }
+*/
+/*@
+gl_foo foo1_ok {
+  gl_fooo data:\true;
+  gl_foo foo2_ok {
+    gl_fooo data:\true;
+    gl_foo foo3_ok {
+      gl_fooo data:\true;
+      gl_fooo data:\false;
+      }
+    gl_fooo data:\true;
+    }
+  gl_fooo data:\false;
+  }
+*/
+