From cbcf2f8950d0ea7208d9c021422946433f90e745 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Wed, 8 Jul 2015 10:49:36 +0200
Subject: Turn "redefinition with an incompatible type" warning into an error.

Also: improve error message by showing old and new types.
---
 cparser/Elab.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'cparser/Elab.ml')

diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index d6b79780..5be4c598 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1805,7 +1805,12 @@ let enter_or_refine_ident local loc env s sto ty =
         | Some new_ty ->
             new_ty
         | None ->
-            warning loc "redefinition of '%s' with incompatible type" s; ty in
+            error loc
+               "redefinition of '%s' with incompatible type.@ \
+                Previous type: %a.@ \
+                New type: %a"
+              s Cprint.typ old_ty Cprint.typ ty;
+            ty in
       let new_sto =
 	(* The only case not allowed is removing static *)
 	match old_sto,sto with
-- 
cgit 


From 3eb2b3b7bb464d9844f7c161fbcff53f597348b9 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Wed, 8 Jul 2015 11:24:09 +0200
Subject: 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.
---
 cparser/Elab.ml | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

(limited to 'cparser/Elab.ml')

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
 
-- 
cgit