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.

2 files changed, 17 insertions, 12 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)
 ]
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 5d2a5cfe..9cffd934 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -767,12 +767,14 @@ 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 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
+    let a' =
+      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";
+        add_attributes [Attr("noreturn",[])] a
+      end else a in
+    ((id, add_attributes_type a' ty, init), env1) in
   (mmap elab_one_name env' namelist, sto, tydef)
 
 (* Elaboration of a field group *)
@@ -2323,17 +2325,19 @@ let elab_fundef env spec name defs body loc =
       { sdesc = Sblock (List.map mkdecl extra_decls @ [body2]);
         sloc = no_loc }
     end in
-  if noret then begin
+  (* Handling of _Noreturn and of attribute("noreturn") *)
+  if noret then
     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;
+  if (noret || find_custom_attributes ["noreturn"; "__noreturn__"] attr <> [])
+  && contains_return body1 then
+    warning loc Invalid_noreturn "function '%s' declared 'noreturn' should not return" s;
   (* Build and emit function definition *)
   let fn =
     { fd_storage = sto1;
       fd_inline = inline;
       fd_name = fun_id;
-      fd_attrib = attr;
+      fd_attrib = if noret then add_attributes [Attr("noreturn",[])] attr
+                           else attr;
       fd_ret = ty_ret;
       fd_params = params;
       fd_vararg = vararg;