diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-16 16:45:05 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-16 16:45:05 +0100 |
| commit | 20c7b4d292ca1e69b66d10e8b0054982fe464714 (patch) | |
| tree | 073ff5557711a4b1141445281e56a67764c11c63 | |
| parent | 9b63d90b40974eed35bd199fcfc6ccbabb1ed5b7 (diff) | |
| download | compcert-kvx-20c7b4d292ca1e69b66d10e8b0054982fe464714.tar.gz compcert-kvx-20c7b4d292ca1e69b66d10e8b0054982fe464714.zip | |
Added handling for noreturn std functions.
The C11 standard declares exit,abort,_Exit,quick_exit and
thrd_exit as _Noreturn however this is not included in older C
libs and leads to false negatives in reporting _Noreturn and
return type warnings. This can be avoided by enhancing the
noreturn check of the Cflow analysis to also test if one of the
above functions is called.
Bug 21009
| -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 |