diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2017-02-15 11:30:14 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-02-15 11:30:14 +0100 |
| commit | 53479577c06db853f48cf9927b5039507436be45 (patch) | |
| tree | 53583f62226462200c1c00c1e12806c42c9d1a6d /cparser/Elab.ml | |
| parent | 4ac453011fb3ee241c6f3023f79c942d99f72eb5 (diff) | |
| parent | 6805bcf7b3ddd78bcbe0e25618ccaf0429ff78ec (diff) | |
| download | compcert-53479577c06db853f48cf9927b5039507436be45.tar.gz compcert-53479577c06db853f48cf9927b5039507436be45.zip | |
Merge pull request #162 from AbsInt/return-analysis-2
Improved warnings related to function returns
Diffstat (limited to 'cparser/Elab.ml')
| -rw-r--r-- | cparser/Elab.ml | 24 |
1 files changed, 18 insertions, 6 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index ea85ad04..eb9ff560 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 = |