summaryrefslogtreecommitdiff
path: root/cparser/Elab.ml
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-07-08 09:15:23 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-07-08 09:15:23 +0000
commitc838d3368f840ca35a638f8e8f6379fbf9606783 (patch)
treed91127ddfd4adf4fe08f4efb977dad52b7ae9dbc /cparser/Elab.ml
parent118c148ec89dc0b53bb377cf637cfdcd800f06e5 (diff)
Preliminary support for gcc-style __attribute__ over types
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1377 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cparser/Elab.ml')
-rw-r--r--cparser/Elab.ml16
1 files changed, 14 insertions, 2 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 7204508..9a4639f 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -255,13 +255,25 @@ let elab_constant loc = function
(* Elaboration of attributes *)
+exception Wrong_attr_arg
+
+let elab_attr_arg loc = function
+ | VARIABLE v -> AIdent v
+ | CONSTANT(CONST_STRING s) -> AString s
+ | CONSTANT(CONST_INT s) ->
+ 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) ->
- (* warning loc "ignoring '%s' attribute" name; *)
- None
+ try
+ Some (Attr(name, 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
| [] -> []