diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-06 16:03:45 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-06 16:03:45 +0100 |
| commit | 4afaf8c23274752c8a6067bd785e114578068702 (patch) | |
| tree | 567b78433bded0385391b8805645b8242e9e2e54 /cfrontend/C2C.ml | |
| parent | 3babd253e1d194549294c282e1b0c60097b26b07 (diff) | |
| download | compcert-kvx-4afaf8c23274752c8a6067bd785e114578068702.tar.gz compcert-kvx-4afaf8c23274752c8a6067bd785e114578068702.zip | |
Preliminary support for the "noreturn" attribute
- Mark the "noreturn" attribute as related to function types, so that it is correctly attached to the nearest enclosing function type.
- Add this attribute on functions declared / defined _Noreturn (with the C2011 keyword). The information is not used presently but could be useful later.
Diffstat (limited to 'cfrontend/C2C.ml')
| -rw-r--r-- | cfrontend/C2C.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 183af347..0d24691f 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -274,7 +274,8 @@ let attributes = [ ("aligned", Cutil.Attr_type); (* struct-related *) ("packed", Cutil.Attr_struct); - (* function-related (currently none) *) + (* function-related *) + ("noreturn", Cutil.Attr_function); (* name-related *) ("section", Cutil.Attr_name) ] |