diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-06 16:53:12 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-06 16:53:12 +0100 |
commit | 8ace28abf0c70ebdc423baea9ae0e8c68e0b60ed (patch) | |
tree | 43e89a45ed321081cbcaaac06165a7e62b84a34b /cfrontend/C2C.ml | |
parent | 9d4bb7ec914566b3920cca3c6823515448fb65c1 (diff) | |
parent | 4afaf8c23274752c8a6067bd785e114578068702 (diff) | |
download | compcert-8ace28abf0c70ebdc423baea9ae0e8c68e0b60ed.tar.gz compcert-8ace28abf0c70ebdc423baea9ae0e8c68e0b60ed.zip |
Merge branch 'elaboration-of-attributes'
Diffstat (limited to 'cfrontend/C2C.ml')
-rw-r--r-- | cfrontend/C2C.ml | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 91941d74..f2fbf255 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -260,6 +260,20 @@ let builtins = Builtins.({ typedefs = builtins_generic.typedefs @ CBuiltins.builtins.typedefs; functions = builtins_generic.Builtins.functions @ CBuiltins.builtins.functions }) +(** ** The known attributes *) + +let attributes = [ + (* type-related *) + ("aligned", Cutil.Attr_type); + (* struct-related *) + ("packed", Cutil.Attr_struct); + (* function-related *) + ("noreturn", Cutil.Attr_function); + (* name-related *) + ("section", Cutil.Attr_name) +] + + (** ** Functions used to handle string literals *) let stringNum = ref 0 (* number of next global for string literals *) @@ -1091,7 +1105,7 @@ let convertFundef loc env fd = Hashtbl.add decl_atom id' { a_storage = fd.fd_storage; a_alignment = None; - a_sections = Sections.for_function env id' fd.fd_ret; + a_sections = Sections.for_function env id' fd.fd_attrib; a_access = Sections.Access_default; a_inline = fd.fd_inline && not fd.fd_vararg; (* PR#15 *) a_loc = loc }; |