Problems with multiple declarations of publically-visible identifiers

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1831 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

3 files changed, 55 insertions, 20 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 1abf3326..1a2a4533 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -839,32 +839,55 @@ let rec translEnv env = function
             env in
       translEnv env' gl
 
-(** Eliminate forward declarations of globals that are defined later. *)
+(** Eliminate multiple declarations of globals. *)
 
 module IdentSet = Set.Make(struct type t = C.ident let compare = compare end)
 
 let cleanupGlobals p =
   
+  (* First pass: determine what is defined *)
+  let strong = ref IdentSet.empty (* def functions or variables with inits *)
+  and weak = ref IdentSet.empty (* variables without inits *)
+  and extern = ref IdentSet.empty in (* extern decls *)
+  let classify_def g =
+        updateLoc g.gloc;
+    match g.gdesc with
+    | C.Gfundef fd ->
+        if IdentSet.mem fd.fd_name !strong then
+          error ("multiple definitions of " ^ fd.fd_name.name);
+        strong := IdentSet.add fd.fd_name !strong
+    | C.Gdecl(Storage_extern, id, ty, init) ->
+        extern := IdentSet.add id !extern
+    | C.Gdecl(sto, id, ty, Some i) ->
+        if IdentSet.mem id !strong then
+          error ("multiple definitions of " ^ id.name);
+        strong := IdentSet.add id !strong
+    | C.Gdecl(sto, id, ty, None) ->
+        weak := IdentSet.add id !weak
+    | _ -> () in
+  List.iter classify_def p;
+
+  (* Second pass: keep "best" definition for each identifier *)  
   let rec clean defs accu = function
     | [] -> accu
     | g :: gl ->
         updateLoc g.gloc;
         match g.gdesc with
-        | C.Gdecl(sto, id, ty, None) ->
-            if IdentSet.mem id defs
+        | C.Gdecl(sto, id, ty, init) ->
+            let better_def_exists =
+              if sto = Storage_extern then
+                IdentSet.mem id !strong || IdentSet.mem id !weak
+              else if init = None then
+                IdentSet.mem id !strong
+              else
+                false in
+            if IdentSet.mem id defs || better_def_exists
             then clean defs accu gl
             else clean (IdentSet.add id defs) (g :: accu) gl
-        | C.Gdecl(_, id, ty, _) ->
-            if IdentSet.mem id defs then
-              error ("multiple definitions of " ^ id.name);
-            clean (IdentSet.add id defs) (g :: accu) gl
         | C.Gfundef fd ->
-            if IdentSet.mem fd.fd_name defs then
-              error ("multiple definitions of " ^ fd.fd_name.name);
             clean (IdentSet.add fd.fd_name defs) (g :: accu) gl
         | _ ->
             clean defs (g :: accu) gl
-
   in clean IdentSet.empty [] (List.rev p)
 
 (** Convert a [C.program] into a [Csyntax.program] *)
diff --git a/cparser/Parse.ml b/cparser/Parse.ml
index 2c467a76..0fc85bf3 100644
--- a/cparser/Parse.ml
+++ b/cparser/Parse.ml
@@ -44,7 +44,7 @@ let preprocessed_file transfs name sourcefile =
   let ic = open_in sourcefile in
   let p =
     try
-      Rename.program (transform_program t (Elab.elab_preprocessed_file name ic))
+      transform_program t (Elab.elab_preprocessed_file name ic)
     with Parsing.Parse_error ->
            Errors.error "Error during parsing"; []
        | Errors.Abort ->
diff --git a/cparser/Rename.ml b/cparser/Rename.ml
index 0ce401f1..76c3c12c 100644
--- a/cparser/Rename.ml
+++ b/cparser/Rename.ml
@@ -19,26 +19,38 @@ open C
 open Cutil
 
 module StringSet = Set.Make(String)
+module StringMap = Map.Make(String)
 
 type rename_env = {
   re_id: ident IdentMap.t;
+  re_public: ident StringMap.t;
   re_used: StringSet.t
 }
 
-let empty_env = { re_id = IdentMap.empty; re_used = StringSet.empty }
+let empty_env =
+  { re_id = IdentMap.empty;
+    re_public = StringMap.empty;
+    re_used = StringSet.empty }
 
 (* For public global identifiers, we must keep their names *)
 
-let enter_global env id =
-  { re_id = IdentMap.add id id env.re_id;
-    re_used = StringSet.add id.name env.re_used }
+let enter_public env id =
+  try
+    let id' = StringMap.find id.name env.re_public in
+    { env with re_id = IdentMap.add id id' env.re_id }
+  with Not_found ->
+    { re_id = IdentMap.add id id env.re_id;
+      re_public = StringMap.add id.name id env.re_public;
+      re_used = StringSet.add id.name env.re_used }
 
 (* For static or local identifiers, we make up a new name if needed *)
 (* If the same identifier has already been declared, 
    don't rename a second time *)
 
 let rename env id =
-  if IdentMap.mem id env.re_id then (id, env) else begin
+  try
+    (IdentMap.find id env.re_id, env)
+  with Not_found ->
     let basename =
       if id.name = "" then Printf.sprintf "_%d" id.stamp else id.name in
     let newname =
@@ -53,8 +65,8 @@ let rename env id =
     let newid = {name = newname; stamp = id.stamp } in
     ( newid,
       { re_id = IdentMap.add id newid env.re_id;
+        re_public = env.re_public;
         re_used = StringSet.add newname env.re_used } )
-  end
 
 (* Monadic map to thread an environment *)
 
@@ -223,7 +235,7 @@ let rec globdecls env accu = function
 (* Reserve names of builtins *)
 
 let reserve_builtins () =
-  List.fold_left enter_global empty_env (Builtins.identifiers())
+  List.fold_left enter_public empty_env (Builtins.identifiers())
 
 (* Reserve global declarations with public visibility *)
 
@@ -234,13 +246,13 @@ let rec reserve_public env = function
         match dcl.gdesc with
         | Gdecl(sto, id, _, _) ->
             begin match sto with
-            | Storage_default | Storage_extern -> enter_global env id
+            | Storage_default | Storage_extern -> enter_public env id
             | Storage_static -> env
             | _ -> assert false
             end
         | Gfundef f ->
             begin match f.fd_storage with
-            | Storage_default | Storage_extern -> enter_global env f.fd_name
+            | Storage_default | Storage_extern -> enter_public env f.fd_name
             | Storage_static -> env
             | _ -> assert false
             end