From 4e62a2c4b2c809ea020423e7e328ba96e379d64d Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Wed, 23 Mar 2016 14:22:33 +0100
Subject: 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
---
 cparser/Cutil.ml | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

(limited to 'cparser/Cutil.ml')

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
-- 
cgit