aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Cutil.ml
diff options
context:
space:
mode:
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