From 12696ae9f6c34aaffc668711d96beda51a783832 Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 14 Apr 2011 09:15:17 +0000 Subject: 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 --- cparser/Elab.ml | 38 ++++++++++++++++++++++---------------- 1 file changed, 22 insertions(+), 16 deletions(-) (limited to 'cparser/Elab.ml') 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 *) -- cgit v1.2.3