Revised handling of GCC attributes. Preliminary, untested support for __aligned__ attribute

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1634 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

3 files changed, 34 insertions, 17 deletions

diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index bb540c7..7aac659 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -63,6 +63,14 @@ let rec incl_attributes (al1: attributes) (al2: attributes) =
       else if a1 > a2 then incl_attributes al1 al2'
       else incl_attributes al1' al2'
 
+let rec find_custom_attributes (names: string list)  (al: attributes) =
+  match al with
+  | [] -> []
+  | Attr(name, args) :: tl when List.mem name names ->
+      args :: find_custom_attributes names tl
+  | _ :: tl ->
+      find_custom_attributes names tl
+
 (* Adding top-level attributes to a type.  Doesn't need to unroll defns. *)
 (* Array types cannot carry attributes, so add them to the element type. *)
 
@@ -96,7 +104,7 @@ let rec attributes_of_type env t =
   | TInt(ik, a) -> a
   | TFloat(fk, a) -> a
   | TPtr(ty, a) -> a
-  | TArray(ty, sz, a) -> a              (* correct? *)
+  | TArray(ty, sz, a) -> add_attributes a (attributes_of_type env ty)
   | TFun(ty, params, vararg, a) -> a
   | TNamed(s, a) -> attributes_of_type env (unroll env t)
   | TStruct(s, a) -> a
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index 7a185f5..d4c9441 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -33,6 +33,9 @@ val remove_attributes : attributes -> attributes -> attributes
   (* Difference [attr1 \ attr2] between two sets of attributes *)
 val incl_attributes : attributes -> attributes -> bool
   (* Check that first set of attributes is a subset of second set. *)
+val find_custom_attributes : string list -> attributes -> attr_arg list list
+  (* Extract arguments of custom [Attr] attributes whose names appear
+     in the given list of names. *)
 val attributes_of_type : Env.t -> typ -> attributes
   (* Return the attributes of the given type, expanding typedefs if needed. *)
 val add_attributes_type : attributes -> typ -> typ
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 92452b9..6c14836 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -264,23 +264,29 @@ let elab_attr_arg loc = function
       let (v, _) = elab_int_constant loc s in AInt v
   | _ -> raise Wrong_attr_arg
 
-let elab_attribute loc = function
-  | ("const", []) -> Some AConst
-  | ("restrict", []) -> Some ARestrict
-  | ("volatile", []) -> Some AVolatile
-  | (name, args) -> 
-      try
-        Some (Attr(name, List.map (elab_attr_arg loc) args))
+let elab_gcc_attr loc = function
+  | VARIABLE v ->
+      [Attr(v, [])]
+  | CALL(VARIABLE v, args) ->
+      begin try
+        [Attr(v, List.map (elab_attr_arg loc) args)]
       with Wrong_attr_arg ->
-        warning loc "cannot parse '%s' attribute, ignored" name;
-        None
-
-let rec elab_attributes loc = function
-  | [] -> []
-  | a1 :: al ->
-      match elab_attribute loc a1 with
-      | None -> elab_attributes loc al
-      | Some a -> add_attributes [a] (elab_attributes loc al)
+        warning loc "cannot parse '%s' attribute, ignored" v; []
+      end
+  | _ ->
+      warning loc "ill-formed attribute, ignored"; []
+
+let elab_attribute loc = function
+  | ("const", []) -> [AConst]
+  | ("restrict", []) -> [ARestrict]
+  | ("volatile", []) -> [AVolatile]
+  | (("attribute" | "__attribute__"), l) ->
+        List.flatten (List.map (elab_gcc_attr loc) l)
+  | (name, _) ->
+        warning loc "`%s' annotation ignored" name; []
+
+let elab_attributes loc al =
+  List.fold_left add_attributes [] (List.map (elab_attribute loc) al)
 
 (* Auxiliary for typespec elaboration *)