aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Cutil.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bschommer@users.noreply.github.com>2016-04-04 13:27:39 +0200
committerBernhard Schommer <bschommer@users.noreply.github.com>2016-04-04 13:27:39 +0200
commit1a02cbf4746bcbd059c35613d4a71cd127fbfa13 (patch)
treefebd5b7769e9577ce03917b1c51679a2eac88ce4 /cparser/Cutil.ml
parent8b0d5a0d291c66f05869c15f92539bd1d7082d3a (diff)
parent4e62a2c4b2c809ea020423e7e328ba96e379d64d (diff)
downloadcompcert-1a02cbf4746bcbd059c35613d4a71cd127fbfa13.tar.gz
compcert-1a02cbf4746bcbd059c35613d4a71cd127fbfa13.zip
Merge pull request #95 from AbsInt/noreturn
Added the _Noreturn keyword.
Diffstat (limited to 'cparser/Cutil.ml')
-rw-r--r--cparser/Cutil.ml21
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