Warning for C11 _Noreturn feature.

The warning for C11 features is now also triggered for _Noreturn.

1 files changed, 10 insertions, 4 deletions

diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 6188b482..127f5fe2 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -748,8 +748,11 @@ and elab_init_name_group keep_ty loc env (spec, namelist) =
     let a = elab_attributes env attr in
     if inl && not (is_function_type env ty) then
       error loc "'inline' can only appear on functions";
-    if noret && not (is_function_type env ty) then
-      error loc "'_Noreturn' can only appear on functions";
+    if noret then begin
+      warning loc Celeven_extension "_Noreturn functions are a C11 extension";
+      if not (is_function_type env ty) then
+        error loc "'_Noreturn' can only appear on functions";
+    end;
     ((id, add_attributes_type a ty, init), env1) in
   (mmap elab_one_name env' namelist, sto, tydef)
 
@@ -2249,8 +2252,11 @@ let elab_fundef env spec name defs body loc =
       { sdesc = Sblock (List.map mkdecl extra_decls @ [body2]);
         sloc = no_loc }
     end in
-  if noret && contains_return body1 then
-    warning loc Invalid_noreturn "function '%s' declared 'noreturn' should not return" s;
+  if noret then begin
+    warning loc Celeven_extension "_Noreturn functions are a C11 extension";
+    if contains_return body1 then
+      warning loc Invalid_noreturn "function '%s' declared 'noreturn' should not return" s;
+  end;
   (* Build and emit function definition *)
   let fn =
     { fd_storage = sto1;