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

1 files changed, 21 insertions, 0 deletions

diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 1bbb8e98..4b4e1b81 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -1118,3 +1118,24 @@ let rec subst_stmt phi s =
                List.map subst_asm_operand inputs,
                clob)
   }
+
+let contains_return s =
+  let rec aux s =
+    match s.sdesc with
+    | Sskip
+    | Sbreak
+    | Scontinue
+    | Sdo _
+    | Sdecl _
+    | Sasm _
+    | Sgoto _ -> false
+    | Sif(_, s1, s2)
+    | Sseq(s1, s2) -> aux s1 || aux s2
+    | Sswitch (_, s)
+    | Slabeled (_, s)
+    | Swhile (_, s)
+    | Sdowhile(s, _ ) -> aux s
+    | Sfor(s1, _ , s2, s3) ->  aux s1 || aux s2 || aux s3
+    | Sreturn _ -> true
+    | Sblock sl -> List.fold_left (fun acc s -> acc || aux s) false sl in
+  aux s