diff options
| -rw-r--r-- | cparser/Cflow.ml | 11 | ||||
| -rw-r--r-- | cparser/Cutil.ml | 4 | ||||
| -rw-r--r-- | cparser/Cutil.mli | 2 |
3 files changed, 14 insertions, 3 deletions
diff --git a/cparser/Cflow.ml b/cparser/Cflow.ml index 790d9079..718ae421 100644 --- a/cparser/Cflow.ml +++ b/cparser/Cflow.ml @@ -22,6 +22,10 @@ open Cutil module StringSet = Set.Make(String) +(* Functions declared noreturn by the standard *) +let std_noreturn_functions = + ["exit";"abort";"_Exit";"quick_exit";"thrd_exit"] + (* Statements are abstracted as "flow transformers": functions from possible inputs to possible outcomes. Possible inputs are: @@ -177,9 +181,10 @@ let rec outcomes env s : flow = | Sskip -> normal | Sdo {edesc = ECall(fn, args)} -> - if find_custom_attributes ["noreturn"; "__noreturn__"] - (attributes_of_type env fn.etyp) = [] - then normal else noflow + let returns = find_custom_attributes ["noreturn"; "__noreturn__"] + (attributes_of_type env fn.etyp) = [] in + let std_noreturn = List.exists (is_call_to_fun fn) std_noreturn_functions in + if returns && not std_noreturn then normal else noflow | Sdo e -> normal | Sseq(s1, s2) -> diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 6cafaf17..124560e5 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -954,6 +954,10 @@ let is_debug_stmt s = is_debug_call e | _ -> false +let is_call_to_fun e s = + match e.edesc with + | EVar id -> id.C.name = s + | _ -> false (* Assignment compatibility check over attributes. Standard attributes ("const", "volatile", "restrict") can safely diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index a1b9cd26..715cc123 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -210,6 +210,8 @@ val type_of_member : Env.t -> field -> typ (* Return the type of accessing the given field [fld]. Normally it's [fld.fld_type] but there is a special case for small unsigned bitfields. *) +val is_call_to_fun : exp -> string -> bool + (* Test whether the caller is the given function *) val is_debug_stmt : stmt -> bool (* Is the given statement a call to debug builtin? *) val is_literal_0 : exp -> bool |