From 2b31f7c714f0005abbaf3cbabda6c9a8428c32ef Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Fri, 19 Jul 2019 18:17:18 +0200
Subject: [PATCH] [Cil] new functions to retrieve attributes for globals and
global annotations
---
src/kernel_services/ast_queries/cil.ml | 23 +++++++++++++++++++++++
src/kernel_services/ast_queries/cil.mli | 11 +++++++++++
2 files changed, 34 insertions(+)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 186a56d4cdd..58294dad1dd 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 bd9004a9586..789da17baa4 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
(* ************************************************************************* *)
--
GitLab