diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 13cc3bef4a1da38d260a1dc63bf756141171f9d2..732978be9413fa1d5291fe45c64216b4cfda1691 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -60,7 +60,6 @@ let valid_sid = false
 open Cil_types
 open Cil_datatype
 open Cil_const
-open Ast_attributes
 
 (* Maps the start and end positions of a function declaration or definition
    (including its possible contract) to its name. *)
@@ -96,7 +95,7 @@ let unsupported_attributes = ["vector_size"]
 let erased_attributes = ["malloc"]
 let () =
   List.iter
-    (fun a -> register_attribute a AttrIgnored)
+    (fun a -> Ast_attributes.register_attribute a AttrIgnored)
     erased_attributes
 
 (* JS: return [Some s] if the attribute string is the attribute annotation [s]
@@ -125,7 +124,7 @@ let stripUnderscore s =
         (* Attribute annotation are always considered known *)
         ()
       | None ->
-        if not (is_known_attribute res) then
+        if not (Ast_attributes.is_known_attribute res) then
           Kernel.warning
             ~once:true ~current:true ~wkey:Kernel.wkey_unknown_attribute
             "Unknown attribute: %s" s
@@ -135,43 +134,43 @@ let stripUnderscore s =
 
 let frama_c_keep_block = "FRAMA_C_KEEP_BLOCK"
 let () = Cil_printer.register_shallow_attribute frama_c_keep_block
-let () = register_attribute frama_c_keep_block AttrStmt
+let () = Ast_attributes.register_attribute frama_c_keep_block AttrStmt
 
 let fc_stdlib = "fc_stdlib"
 let fc_stdlib_generated = "fc_stdlib_generated"
 let () = Cil_printer.register_shallow_attribute fc_stdlib
 let () = Cil_printer.register_shallow_attribute fc_stdlib_generated
 (* fc_stdlib attribute already registered in cil.ml *)
-let () = register_attribute fc_stdlib_generated (AttrName false)
+let () = Ast_attributes.register_attribute fc_stdlib_generated (AttrName false)
 
 let fc_local_static = "fc_local_static"
 let () = Cil_printer.register_shallow_attribute fc_local_static
-let () = register_attribute fc_local_static (AttrName false)
+let () = Ast_attributes.register_attribute fc_local_static (AttrName false)
 
 let frama_c_destructor = "fc_destructor"
 let () = Cil_printer.register_shallow_attribute frama_c_destructor
-let () = register_attribute frama_c_destructor (AttrName false)
+let () = Ast_attributes.register_attribute frama_c_destructor (AttrName false)
 
 let () =
   (* packed and aligned are treated separately, we ignore them
      during standard processing.
   *)
-  register_attribute "packed" AttrIgnored;
-  register_attribute "aligned" AttrIgnored;
-  register_attribute "warn_unused_result" (AttrFunType false);
-  register_attribute "FC_OLDSTYLEPROTO" (AttrName false);
-  register_attribute "static" (AttrName false);
-  register_attribute "missingproto" (AttrName false);
-  register_attribute "dummy" AttrIgnored;
-  registerAttribute "signal" AttrIgnored; (* AVR-specific attribute *)
-  registerAttribute "leaf" AttrIgnored;
-  registerAttribute "nonnull" AttrIgnored;
-  registerAttribute "deprecated" AttrIgnored;
-  registerAttribute "access" AttrIgnored;
-  registerAttribute "returns_twice" AttrIgnored;
-  registerAttribute "pure" AttrIgnored;
-  registerAttribute "cleanup" AttrIgnored;
-  registerAttribute "warning" AttrIgnored;
+  Ast_attributes.register_attribute "packed" AttrIgnored;
+  Ast_attributes.register_attribute "aligned" AttrIgnored;
+  Ast_attributes.register_attribute "warn_unused_result" (AttrFunType false);
+  Ast_attributes.register_attribute "FC_OLDSTYLEPROTO" (AttrName false);
+  Ast_attributes.register_attribute "static" (AttrName false);
+  Ast_attributes.register_attribute "missingproto" (AttrName false);
+  Ast_attributes.register_attribute "dummy" AttrIgnored;
+  Ast_attributes.register_attribute "signal" AttrIgnored; (* AVR-specific attribute *)
+  Ast_attributes.register_attribute "leaf" AttrIgnored;
+  Ast_attributes.register_attribute "nonnull" AttrIgnored;
+  Ast_attributes.register_attribute "deprecated" AttrIgnored;
+  Ast_attributes.register_attribute "access" AttrIgnored;
+  Ast_attributes.register_attribute "returns_twice" AttrIgnored;
+  Ast_attributes.register_attribute "pure" AttrIgnored;
+  Ast_attributes.register_attribute "cleanup" AttrIgnored;
+  Ast_attributes.register_attribute "warning" AttrIgnored;
   ()
 
 (** A hook into the code that creates temporary local vars.  By default this
@@ -298,7 +297,7 @@ let rec is_dangerous e = match e.enode with
 and is_dangerous_lval = function
   | Var v,_ when
       (not v.vglob && not v.vformal && not v.vtemp)
-      || has_attribute "volatile" v.vattr
+      || Ast_attributes.has_attribute "volatile" v.vattr
       || Cil.typeHasAttribute "volatile" (Cil.unrollType v.vtype)
     -> true
   (* Local might be uninitialized, which will trigger UB,
@@ -408,6 +407,7 @@ let process_stdlib_pragma name args =
   end else Some (Attr(name, args))
 
 let fc_stdlib_attribute attrs =
+  let open Ast_attributes in
   let s = get_current_stdheader () in
   if s = "" then attrs
   else begin
@@ -566,8 +566,8 @@ let process_pack_pragma name args =
   end
 
 let force_packed_attribute a =
-  if has_attribute "packed" a then a
-  else add_attribute (Attr("packed",[])) a
+  if Ast_attributes.has_attribute "packed" a then a
+  else Ast_attributes.add_attribute (Attr("packed",[])) a
 
 let is_power_of_two i = i > 0 && i land (i-1) = 0
 
@@ -597,7 +597,7 @@ let warn_invalid_align_attribute aps =
    consider the maximum among them. This function computes this value
    and also emits warnings for invalid attributes. *)
 let combine_aligned_attributes attrs =
-  match filter_attributes "aligned" attrs with
+  match Ast_attributes.filter_attributes "aligned" attrs with
   | [] -> None
   | aligned_attrs ->
     List.fold_left (fun acc attr ->
@@ -642,6 +642,7 @@ let check_aligned attrs =
    This function is complemented by
    [process_pragmas_pack_align_field_attributes]. *)
 let process_pragmas_pack_align_comp_attributes loc ci cattrs =
+  let open Ast_attributes in
   let source = snd loc in
   match !current_packing_pragma, align_pragma_for_struct ci.corig_name with
   | None, None -> check_aligned cattrs
@@ -693,6 +694,7 @@ let process_pragmas_pack_align_comp_attributes loc ci cattrs =
      has 2 alignment directives, it is the maximum of those that is taken). *)
 let process_pragmas_pack_align_field_attributes fi fattrs cattr =
   let open Current_loc.Operators in
+  let open Ast_attributes in
   let<> UpdatedCurrentLoc = fi.floc in
   match !current_packing_pragma, align_pragma_for_struct fi.forig_name with
   | None, None -> check_aligned fattrs
@@ -2576,8 +2578,8 @@ let cabsAddAttributes al0 (al: attributes) : attributes =
     List.fold_left
       (fun acc (Attr(an, _) | AttrAnnot an as a) ->
          (* See if the attribute is already in there *)
-         match filter_attributes an acc with
-         | [] -> add_attribute a acc (* Nothing with that name *)
+         match Ast_attributes.filter_attributes an acc with
+         | [] -> Ast_attributes.add_attribute a acc (* Nothing with that name *)
          | a' :: _ ->
            if Cil_datatype.Attribute.equal a a' then
              acc (* Already in *)
@@ -2587,7 +2589,7 @@ let cabsAddAttributes al0 (al: attributes) : attributes =
                Cil_printer.pp_attribute a Cil_printer.pp_attribute a' ;
              (* let acc' = drop_attribute an acc in *)
              (* Keep both attributes *)
-             add_attribute a acc
+             Ast_attributes.add_attribute a acc
            end)
       al
       al0
@@ -2668,7 +2670,7 @@ let rec cabsTypeCombineAttributes what a0 t =
       | TNamed ti  -> mk_tnamed ~tattr ti
       | TBuiltin_va_list -> mk_tbuiltin ~tattr ()
       | TArray (bt, l) ->
-        let att_elt, att_typ = split_array_attributes a0 in
+        let att_elt, att_typ = Ast_attributes.split_array_attributes a0 in
         let bt' = cabsArrayPushAttributes what att_elt bt in
         let tattr = combineAttributes what att_typ t.tattr in
         mk_tarray ~tattr bt' l
@@ -2686,7 +2688,7 @@ let cabsTypeAddAttributes =
 
 (* Do types *)
 
-let get_qualifiers t = filter_qualifier_attributes (Cil.typeAttrs t)
+let get_qualifiers t = Ast_attributes.filter_qualifier_attributes (Cil.typeAttrs t)
 
 let castTo ?context ?(fromsource=false)
     (oldt : typ) (newt : typ) (e : exp) : (typ * exp) =
@@ -2744,8 +2746,8 @@ let makeGlobalVarinfo (isadef: bool) (vi: varinfo) : varinfo * bool =
       (* If the new declaration has a section attribute, remove any
        * preexisting section attribute. This mimics behavior of gcc that is
        * required to compile the Linux kernel properly. *)
-      if has_attribute "section" vi.vattr then
-        oldvi.vattr <- drop_attribute "section" oldvi.vattr;
+      if Ast_attributes.has_attribute "section" vi.vattr then
+        oldvi.vattr <- Ast_attributes.drop_attribute "section" oldvi.vattr;
       (* Before combining attributes, we need to check compatibility between
          qualifiers *)
       begin
@@ -2762,7 +2764,7 @@ let makeGlobalVarinfo (isadef: bool) (vi: varinfo) : varinfo * bool =
           oldvi.vattr <- cabsAddAttributes oldvi.vattr vi.vattr;
           let what =
             if isadef then
-              CombineFundef (has_attribute "FC_OLDSTYLEPROTO" vi.vattr)
+              CombineFundef (Ast_attributes.has_attribute "FC_OLDSTYLEPROTO" vi.vattr)
             else CombineOther
           in
           let mytype = combineTypes what oldvi.vtype vi.vtype in
@@ -2774,7 +2776,7 @@ let makeGlobalVarinfo (isadef: bool) (vi: varinfo) : varinfo * bool =
                raise Cannot_combine if necessary. However, due to old-style
                prototypes in GCC machdeps, we must support eccentric cases,
                for which we perform no such additional verification. *)
-            if not (has_attribute "FC_OLDSTYLEPROTO" vi.vattr) then
+            if not (Ast_attributes.has_attribute "FC_OLDSTYLEPROTO" vi.vattr) then
               ignore (compatibleTypes oldvi.vtype vi.vtype)
           end;
           Cil.update_var_type oldvi mytype;
@@ -2844,7 +2846,7 @@ let makeGlobalVarinfo (isadef: bool) (vi: varinfo) : varinfo * bool =
         let vi = alphaConvertVarAndAddToEnv true vi in
         (* update the field [vdefined] *)
         if isadef then vi.vdefined <- true;
-        vi.vattr <- drop_attribute "FC_OLDSTYLEPROTO" vi.vattr;
+        vi.vattr <- Ast_attributes.drop_attribute "FC_OLDSTYLEPROTO" vi.vattr;
         vi.vattr <- fc_stdlib_attribute vi.vattr;
         vi, false
       end
@@ -2861,9 +2863,9 @@ let setupBuiltin ?(force_keep=false) name ?spec (resTyp, args_or_argtypes, isva)
       Some (List.map (fun vi -> (vi.vname, vi.vtype, vi.vattr)) args), args
     | ArgTypes argTypes ->
       let funargs =
-        List.mapi
-          (fun i at ->
-             ("__x" ^ string_of_int i, at, [anonymous_attribute])) argTypes
+        List.mapi (fun i at ->
+            ("__x" ^ string_of_int i, at, [Ast_attributes.anonymous_attribute])
+          ) argTypes
       in
       Some funargs, List.map makeFormalsVarDecl funargs
   in
@@ -2878,7 +2880,7 @@ let setupBuiltin ?(force_keep=false) name ?spec (resTyp, args_or_argtypes, isva)
   cabsPushGlobal (GFunDecl (funspec, v, Cil_builtins.builtinLoc));
   Cil.unsafeSetFormalsDecl v args;
   if force_keep then
-    v.vattr <- add_attribute (Attr ("FC_BUILTIN",[])) v.vattr;
+    v.vattr <- Ast_attributes.add_attribute (Attr ("FC_BUILTIN",[])) v.vattr;
   v
 
 (*  builtin is never ghost *)
@@ -3929,7 +3931,7 @@ let append_chunk_to_annot ~ghost annot_chunk current_chunk =
       let locals = b.blocals in
       b.blocals <- [];
       b.battrs <-
-        add_attributes [Attr(frama_c_keep_block,[])] b.battrs;
+      Ast_attributes.add_attributes [Attr(frama_c_keep_block,[])] b.battrs;
       let block = mkStmt ~ghost ~valid_sid (Block b) in
       let chunk = s2c block in
       let chunk = { chunk with cases = current_chunk.cases } in
@@ -4225,7 +4227,9 @@ let rec doSpecList loc ghost (suggestedAnonName: string)
        so they will be returned by doSpecAttr and used in the variable
        declaration.
        Testcase: small1/attr9.c *)
-    let an, af, at = cabsPartitionAttributes ghost ~default:AttrType !attrs in
+    let an, af, at =
+      cabsPartitionAttributes ghost ~default:Ast_attributes.AttrType !attrs
+    in
     attrs := an;      (* Save the name attributes for later *)
     if af <> [] then
       Kernel.error ~once:true ~current:true
@@ -4440,7 +4444,7 @@ let rec doSpecList loc ghost (suggestedAnonName: string)
         let ekind =
           match Kernel.Enums.get () with
           | "" | "help" | "gcc-enums" ->
-            if has_attribute "packed" enum.eattr ||
+            if Ast_attributes.has_attribute "packed" enum.eattr ||
                bytesSizeOfInt real_kind >= bytesSizeOfInt IInt
             then real_kind
             else if unsigned then IUInt else IInt
@@ -4509,13 +4513,13 @@ and makeVarInfoCabs
   let isglobal = kind = `GlobalDecl || kind = `LocalStaticDecl in
   let isformal = kind = `FormalDecl in
   let vtype, nattr =
-    doType ghost (kind:>type_context) (AttrName false)
+    doType ghost (kind:>type_context) (Ast_attributes.AttrName false)
       ~allowVarSizeArrays:isformal
       (* For locals we handle var-sized arrays before makeVarInfoCabs;
          Hence, at this point only formals can have a VLA type *)
       bt (Cabs.PARENTYPE(attrs, ndt, a))
   in
-  if has_attribute "thread" nattr then begin
+  if Ast_attributes.has_attribute "thread" nattr then begin
     let wkey = Kernel.wkey_inconsistent_specifier in
     let source = fst ldecl in
     if isFunctionType vtype then
@@ -4524,12 +4528,12 @@ and makeVarInfoCabs
       Kernel.warning ~wkey ~source "a local object cannot be thread-local";
   end;
   if not isgenerated && ghost then begin
-    if has_attribute "ghost" (Cil.typeAttrs vtype) then
+    if Ast_attributes.has_attribute "ghost" (Cil.typeAttrs vtype) then
       Kernel.warning
         ~wkey:Kernel.wkey_ghost_already_ghost ~once:true ~current:true
         "'%s' is already ghost" n;
     if isArrayType vtype then
-      if has_attribute "ghost" (Cil.typeAttrs (typeOf_array_elem vtype)) then
+      if Ast_attributes.has_attribute "ghost" (Cil.typeAttrs (typeOf_array_elem vtype)) then
         Kernel.warning
           ~wkey:Kernel.wkey_ghost_already_ghost ~once:true ~current:true
           "'%s' elements are already ghost" n;
@@ -4675,7 +4679,7 @@ and doAttributes (ghost:bool) (al: Cabs.attribute list) : attribute list =
    the extra doAttr conversions here, but that's hard to do in doSpecList.*)
 and cabsPartitionAttributes
     ghost
-    ~(default:attribute_class)
+    ~(default:Ast_attributes.attribute_class)
     (attrs:  Cabs.attribute list) :
   Cabs.attribute list * Cabs.attribute list * Cabs.attribute list =
   let rec loop (n,f,t) = function
@@ -4687,7 +4691,7 @@ and cabsPartitionAttributes
           (* doAttr already strip underscores of the attribute if necessary so
              we do not need to strip then before calling get_attribute_class
              here. *)
-          an, get_attribute_class ~default an
+          an, Ast_attributes.get_attribute_class ~default an
       in
       match kind with
       | AttrName _ -> loop (a::n, f, t) rest
@@ -4703,7 +4707,7 @@ and cabsPartitionAttributes
   loop ([], [], []) attrs
 
 and doType (ghost:bool) (context: type_context)
-    (nameortype: attribute_class) (* This is AttrName if we are doing
+    (nameortype: Ast_attributes.attribute_class) (* This is AttrName if we are doing
                                   * the type for a name, or AttrType
                                   * if we are doing this type in a
                                   * typedef *)
@@ -4724,9 +4728,9 @@ and doType (ghost:bool) (context: type_context)
     | Cabs.JUSTBASE -> bt, acc
     | Cabs.PARENTYPE (a1, d, a2) ->
       let a1' = doAttributes ghost a1 in
-      let a1n, a1f, a1t = partition_attributes ~default:AttrType a1' in
+      let a1n, a1f, a1t = Ast_attributes.partition_attributes ~default:AttrType a1' in
       let a2' = doAttributes ghost a2 in
-      let a2n, a2f, a2t = partition_attributes ~default:nameortype a2' in
+      let a2n, a2f, a2t = Ast_attributes.partition_attributes ~default:nameortype a2' in
       let bt' = cabsTypeAddAttributes a1t bt in
       let bt'', a1fadded =
         match unrollTypeNode bt with
@@ -4771,7 +4775,7 @@ and doType (ghost:bool) (context: type_context)
 
     | Cabs.PTR (al, d) ->
       let al' = doAttributes ghost al in
-      let an, af, at = partition_attributes ~default:AttrType al' in
+      let an, af, at = Ast_attributes.partition_attributes ~default:AttrType al' in
       (* Now recurse *)
       let t = mk_tptr ~tattr:at bt in
       let restyp, nattr = doDeclType t acc d in
@@ -4908,7 +4912,7 @@ and doType (ghost:bool) (context: type_context)
           Some len'
       in
       let al' = doAttributes ghost al in
-      if context <> `FormalDecl && has_attribute "static" al' then
+      if context <> `FormalDecl && Ast_attributes.has_attribute "static" al' then
         Kernel.error ~once:true ~current:true
           "static specifier inside array argument is allowed only in \
            function argument";
@@ -4995,12 +4999,12 @@ and doType (ghost:bool) (context: type_context)
        * our life a lot, and is what the standard requires. *)
       let turnArrayIntoPointer (bt: typ)
           (lo: exp option) (a: attributes) : typ =
-        let main_attrs = drop_attribute "static" a in
+        let main_attrs = Ast_attributes.drop_attribute "static" a in
         let a' : attributes =
           match lo with
           | None -> []
           | Some l -> begin
-              let static = if has_attribute "static" a then
+              let static = if Ast_attributes.has_attribute "static" a then
                   [Attr ("static",[])]
                 else []
               in
@@ -5017,7 +5021,7 @@ and doType (ghost:bool) (context: type_context)
                 end
             end
         in
-        let tattr = add_attributes a' main_attrs in
+        let tattr = Ast_attributes.add_attributes a' main_attrs in
         mk_tptr ~tattr bt
       in
       let rec fixupArgumentTypes (argidx: int) (args: varinfo list) : unit =
@@ -5051,7 +5055,7 @@ and doType (ghost:bool) (context: type_context)
           let arg_type_from_vi vi =
             let attrs =
               if vi.vghost then
-                cabsAddAttributes [Attr (frama_c_ghost_formal, [])] vi.vattr
+                cabsAddAttributes [Attr (Ast_attributes.frama_c_ghost_formal, [])] vi.vattr
               else
                 vi.vattr
             in (vi.vname, vi.vtype, attrs)
@@ -5228,7 +5232,7 @@ and makeCompType loc ghost (isstruct: bool)
               end;
               let ftype =
                 typeAddAttributes
-                  [Attr (bitfield_attribute_name, [AInt (Integer.of_int s)])]
+                  [Attr (Ast_attributes.bitfield_attribute_name, [AInt (Integer.of_int s)])]
                   ftype
               in
               w, ftype
@@ -5365,7 +5369,7 @@ and makeCompType loc ghost (isstruct: bool)
     end;
 
   (*  ignore (E.log "makeComp: %s: %a\n" comp.cname d_attrlist a); *)
-  let a = add_attributes comp.cattr a in
+  let a = Ast_attributes.add_attributes comp.cattr a in
   comp.cattr <- process_pragmas_pack_align_comp_attributes loc comp a;
   let res = mk_tcomp comp in
   (* Create a typedef for this one *)
@@ -8909,7 +8913,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
     in
     checkArray inite vi;
     vi.vname <- newname;
-    let attrs = add_attribute (Attr (fc_local_static,[])) vi.vattr in
+    let attrs = Ast_attributes.add_attribute (Attr (fc_local_static,[])) vi.vattr in
     vi.vattr <- fc_stdlib_attribute attrs;
 
     (* However, we have a problem if a real global appears later with the
@@ -8979,7 +8983,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
       let destructor = AStr free.vname in
       let attr = Attr (frama_c_destructor, [destructor]) in
       vi.vdefined <- true;
-      vi.vattr <- add_attribute attr vi.vattr;
+      vi.vattr <- Ast_attributes.add_attribute attr vi.vattr;
     end;
     let se1 =
       if isvarsize then begin (* Variable-sized array *)
@@ -9174,7 +9178,7 @@ and doAliasFun ghost vtype (thisname:string) (othername:string)
     try lookupGlobalVar ghost thisname
     with Not_found -> Kernel.fatal ~current:true "error in doDecl"
   in
-  v.vattr <- drop_attribute "alias" v.vattr
+  v.vattr <- Ast_attributes.drop_attribute "alias" v.vattr
 
 
 (* Do one declaration *)
@@ -9200,7 +9204,7 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
         let vtype, nattr =
           doType local_env.is_ghost `GlobalDecl
             (AttrName false) bt (Cabs.PARENTYPE(attrs, ndt, a)) in
-        (match filter_attributes "alias" nattr with
+        (match Ast_attributes.filter_attributes "alias" nattr with
          | [] -> (* ordinary prototype. *)
            ignore (createGlobal l local_env.is_ghost logic_spec spec_res name)
          (*  E.log "%s is not aliased\n" name *)
@@ -9339,7 +9343,7 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
         doType local_env.is_ghost `GlobalDecl
           (AttrName false) bt (Cabs.PARENTYPE(attrs, dt, a))
       in
-      if has_attribute "thread" funattr then begin
+      if Ast_attributes.has_attribute "thread" funattr then begin
         let wkey = Kernel.wkey_inconsistent_specifier in
         let source = fst funloc in
         Kernel.warning ~wkey ~source "only objects can be thread-local"
@@ -9403,7 +9407,7 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
           if f.vname = "" then begin
             f.vname <- "__x" ^ (string_of_int !cnt);
             incr cnt;
-            f.vattr <- add_attribute anonymous_attribute f.vattr;
+            f.vattr <- Ast_attributes.(add_attribute anonymous_attribute f.vattr);
           end;
           alphaConvertVarAndAddToEnv true f
         in
@@ -10019,7 +10023,7 @@ and doStatement local_env (s : Cabs.statement) : chunk =
   | Cabs.BLOCK (b, _, _) ->
     let c = doBodyScope local_env b in
     let b = c2block ~ghost c in
-    b.battrs <- add_attributes [Attr(frama_c_keep_block,[])] b.battrs;
+    b.battrs <- Ast_attributes.add_attributes [Attr(frama_c_keep_block,[])] b.battrs;
     let res = s2c (mkStmt ~ghost ~valid_sid (Block b)) in
     { res with cases = c.cases }
 
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index b44f996889b5283d011708430b4fe611fb38ddeb..49b2eec37d8957ffb72654b921c2d361b61a5628 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -7256,22 +7256,6 @@ let filter_qualifier_attributes = filter_qualifier_attributes
 
 let splitArrayAttributes = split_array_attributes
 
-type attributeClass =
-    AttrName of bool
-  (** Attribute of a name. If argument is true and we are on MSVC then
-      the attribute is printed using __declspec as part of the storage
-      specifier  *)
-  | AttrFunType of bool
-  (** Attribute of a function type. If argument is true and we are on
-      MSVC then the attribute is printed just before the function name *)
-  | AttrType
-  (** Attribute of a type *)
-  | AttrStmt
-  (** Attribute of a statement or a block *)
-  | AttrIgnored
-  (** Attribute that does not correspond to either of the above classes and is
-      ignored by functions {!get_attribute_class} and {!partition_attributes}. *)
-
 let registerAttribute = register_attribute
 
 let removeAttribute = remove_attribute
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index a2162638d7b6dccbbad885710c8f57d463c49299..8bea6ce9e5aebfa78b1a87c0840feb375617af89 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -2414,26 +2414,6 @@ val filter_qualifier_attributes: attributes -> attributes
 val splitArrayAttributes: attributes -> attributes * attributes
 [@@deprecated "Use Ast_attributes.split_array_attributes instead."]
 
-(** Various classes of attributes
-    @before 30.0-Zinc [AttrStmt] and [AttrIgnored] didn't exist
-*)
-type attributeClass =
-    AttrName of bool
-  (** Attribute of a name. If argument is true and we are on MSVC then
-      the attribute is printed using __declspec as part of the storage
-      specifier  *)
-  | AttrFunType of bool
-  (** Attribute of a function type. If argument is true and we are on
-      MSVC then the attribute is printed just before the function name *)
-  | AttrType
-  (** Attribute of a type *)
-  | AttrStmt
-  (** Attribute of a statement or a block *)
-  | AttrIgnored
-  (** Attribute that does not correspond to either of the above classes and is
-      ignored by functions [attributeClass] and [partitionAttributes]. *)
-[@@deprecated "Use Ast_attributes.attribute_class instead."]
-
 val registerAttribute: string -> Ast_attributes.attribute_class -> unit
 (** Add a new attribute with a specified class *)
 [@@deprecated "Use Ast_attributes.register_attribute instead."]
@@ -2442,7 +2422,8 @@ val removeAttribute: string -> unit
 (** Remove an attribute previously registered. *)
 [@@deprecated "Use Ast_attributes.remove_attribute instead."]
 
-val attributeClass: default:Ast_attributes.attribute_class -> string -> Ast_attributes.attribute_class
+val attributeClass: default:Ast_attributes.attribute_class -> string ->
+  Ast_attributes.attribute_class
 (** Return the class of an attributes. The class `default' is returned for
     unknown and ignored attributes.
     @before 30.0-Zinc no [default] argument