aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Lexer.mll
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-03-23 14:22:33 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2016-03-23 14:22:33 +0100
commit4e62a2c4b2c809ea020423e7e328ba96e379d64d (patch)
tree67a9325ae6e04c3ed353e9cd1f9dc19c1fd87405 /cparser/Lexer.mll
parentccd59f7fc19ffe2347724b532d6ce13c8580c2ab (diff)
downloadcompcert-kvx-4e62a2c4b2c809ea020423e7e328ba96e379d64d.tar.gz
compcert-kvx-4e62a2c4b2c809ea020423e7e328ba96e379d64d.zip
Added the _Noreturn keyword.
CompCert now recognizes the C11 _Noreturn function specifier and emits a simple warning for functions declared _Noreturn containing a return statement. Also the stdnoreturn header and additionally the stdalign header are added. Bug 18541
Diffstat (limited to 'cparser/Lexer.mll')
-rw-r--r--cparser/Lexer.mll2
1 files changed, 2 insertions, 0 deletions
diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll
index 871f2bf9..d3747e22 100644
--- a/cparser/Lexer.mll
+++ b/cparser/Lexer.mll
@@ -65,6 +65,7 @@ let () =
("goto", fun loc -> GOTO loc);
("if", fun loc -> IF loc);
("inline", fun loc -> INLINE loc);
+ ("_Noreturn", fun loc -> NORETURN loc);
("int", fun loc -> INT loc);
("long", fun loc -> LONG loc);
("register", fun loc -> REGISTER loc);
@@ -551,6 +552,7 @@ and singleline_comment = parse
| MOD_ASSIGN loc -> loop MOD_ASSIGN't loc
| MUL_ASSIGN loc -> loop MUL_ASSIGN't loc
| NEQ loc -> loop NEQ't loc
+ | NORETURN loc -> loop NORETURN't loc
| OR_ASSIGN loc -> loop OR_ASSIGN't loc
| PACKED loc -> loop PACKED't loc
| PERCENT loc -> loop PERCENT't loc