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/PrintCsyntax.ml | |
parent | 3babd253e1d194549294c282e1b0c60097b26b07 (diff) | |
download | compcert-4afaf8c23274752c8a6067bd785e114578068702.tar.gz compcert-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/PrintCsyntax.ml')
0 files changed, 0 insertions, 0 deletions