diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 186a56d4cdde06ea54acfab703738e1d4f71616e..58294dad1dd6a328bc53c48e15773d9814657cc1 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -6646,6 +6646,29 @@ let mapGlobals (fl: file)
        | _ -> Kernel.fatal ~current:true "mapGlobals: globinit is not a function"
      end)
 
+let global_annotationAttributes = function
+  | Dfun_or_pred _ -> []
+  | Dvolatile (_,_,_,attrs,_) -> attrs
+  | Daxiomatic (_,_,attrs,_) -> attrs
+  | Dtype _ -> []
+  | Dlemma (_,_,_,_,_,attrs,_) -> attrs
+  | Dinvariant _ -> []
+  | Dtype_annot _ -> []
+  | Dmodel_annot _ -> []
+  | Dextended (_,attrs,_) -> attrs
+  | Dcustom_annot (_,_,attrs,_) -> attrs
+
+let globalAttributes = function
+  | GType ({ttype},_) -> typeAttrs ttype
+  | GCompTag({cattr = attrs},_) | GCompTagDecl({cattr = attrs},_)
+  | GEnumTag({eattr = attrs},_) | GEnumTagDecl({eattr = attrs},_)
+  | GVarDecl({vattr = attrs},_) | GVar({vattr = attrs},_,_) -> attrs
+  | GFun({svar = {vattr = attrs}},_)
+  | GFunDecl(_,{vattr = attrs},_) -> attrs
+  | GPragma (attr, _) -> [attr]
+  | GAnnot (gannot,_) -> global_annotationAttributes gannot
+  | GAsm _ | GText _ -> []
+
 (***************************************************************************)
 
 (* Convert an expression into an attribute, if possible. Otherwise raise
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index bd9004a95867dd7da8ecc2ade9eb7c2ae8829970..789da17baa487c0bbf21ed4b643b7a7e499d70fb 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1368,6 +1368,17 @@ val bitfield_attribute_name: string
     NotAnAttrParam with the offending subexpression *)
 val expToAttrParam: exp -> attrparam
 
+
+(** Return the attributes of the global annotation, if any.
+    @since Frama-C+dev
+*)
+val global_annotationAttributes: global_annotation -> attributes
+
+(** Return the attributes of the global, if any.
+    @since Frama-C+dev
+*)
+val globalAttributes: global -> attributes
+
 exception NotAnAttrParam of exp
 
 (* ************************************************************************* *)