diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-07-08 11:24:09 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-07-08 11:24:09 +0200 |
commit | 3eb2b3b7bb464d9844f7c161fbcff53f597348b9 (patch) | |
tree | 14e8c38541ebb43513f61a426ad3e26209499ef7 | |
parent | cbcf2f8950d0ea7208d9c021422946433f90e745 (diff) | |
download | compcert-3eb2b3b7bb464d9844f7c161fbcff53f597348b9.tar.gz compcert-3eb2b3b7bb464d9844f7c161fbcff53f597348b9.zip |
Add implicit "return 0;" at end of function "main".
As per ISO C99, "hosted environment".
"return 0" is added at the end of any function named "main" that has
"int" as return type. If the name is "main" but the return type is
not "int", emit a warning and do not add anything.
-rw-r--r-- | cparser/Elab.ml | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 5be4c598..5533105a 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1899,6 +1899,18 @@ let elab_fundef env spec name body loc = emit_elab loc (Gdecl(Storage_static, func_id, func_ty, Some func_init)); (* Elaborate function body *) let body' = !elab_funbody_f ty_ret env3 body in + (* Special treatment of the "main" function *) + let body'' = + 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 body' + {sdesc = Sreturn(Some(intconst 0L IInt)); sloc = no_loc} + | _ -> + warning loc "return type of 'main' should be 'int'"; + body' + end else body' in (* Build and emit function definition *) let fn = { fd_storage = sto1; @@ -1909,7 +1921,7 @@ let elab_fundef env spec name body loc = fd_params = params; fd_vararg = vararg; fd_locals = []; - fd_body = body' } in + fd_body = body'' } in emit_elab loc (Gfundef fn); env1 |