From 5a7fc8637ae82d9aaf71c0053078a950ddee3b89 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 7 Feb 2017 09:57:45 +0100 Subject: More precise warnings about function returns This commit introduces a control-flow static analysis over C abstract syntax (file cparser/Cflow.ml) and uses it to - warn for non-void functions that can return by falling through the body - warn more precisely for _Noreturn functions that can return - introduce the "return 0" in "main" functions less often (cosmetic). For the control-flow analysis, the following conservative approximations are made: - any "goto" label is reachable - all cases of a "switch" statement are reachable as soon as the "switch" is reachable (i.e. the switch expression takes all values needed to reach every case) - the boolean expressions in "if", "while", "do"-"while" and "for" can take true and false values, unless they are compile-time constants. --- cparser/Elab.ml | 24 ++++++++++++++++++------ 1 file changed, 18 insertions(+), 6 deletions(-) (limited to 'cparser/Elab.ml') diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 69830122..76f0c998 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -2329,18 +2329,30 @@ let elab_fundef env spec name defs body loc = (Gdecl(Storage_static, func_id, func_ty, Some func_init)); (* Elaborate function body *) let body1 = !elab_funbody_f ty_ret vararg env3 body in - (* Special treatment of the "main" function *) + (* Analyse it for returns *) + let (can_return, can_fallthrough) = Cflow.function_returns env3 body1 in + (* Special treatment of the "main" function. *) let body2 = if s = "main" then begin match unroll env ty_ret with | TInt(IInt, []) -> - (* Add implicit "return 0;" at end of function body *) - sseq no_loc body1 - {sdesc = Sreturn(Some(intconst 0L IInt)); sloc = no_loc} + (* Add implicit "return 0;" at end of function body, unless + this control point is unreachable, e.g. function already + returns in all cases. *) + if can_fallthrough then + sseq no_loc body1 + {sdesc = Sreturn(Some(intconst 0L IInt)); sloc = no_loc} + else body1 | _ -> warning loc Main_return_type "return type of 'main' should be 'int'"; body1 - end else body1 in + end else begin + (* For non-"main" functions, warn if the body can fall through + and the return type is not "void". *) + if can_fallthrough && not (is_void_type env ty_ret) then + warning loc Return_type "control reaches end of non-void function"; + body1 + end in (* Add the extra declarations if any *) let body3 = if extra_decls = [] then body2 else begin @@ -2352,7 +2364,7 @@ let elab_fundef env spec name defs body loc = if noret then warning loc Celeven_extension "_Noreturn functions are a C11 extension"; if (noret || find_custom_attributes ["noreturn"; "__noreturn__"] attr <> []) - && contains_return body1 then + && can_return then warning loc Invalid_noreturn "function '%s' declared 'noreturn' should not return" s; (* Build and emit function definition *) let fn = -- cgit