aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2015-07-08 11:24:09 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2015-07-08 11:24:09 +0200
commit3eb2b3b7bb464d9844f7c161fbcff53f597348b9 (patch)
tree14e8c38541ebb43513f61a426ad3e26209499ef7 /cparser
parentcbcf2f8950d0ea7208d9c021422946433f90e745 (diff)
downloadcompcert-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.
Diffstat (limited to 'cparser')
-rw-r--r--cparser/Elab.ml14
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