summaryrefslogtreecommitdiff
path: root/cparser
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-02-29 09:49:21 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-02-29 09:49:21 +0000
commitf4954776822ac0b32d5ed659301f2377950f9ca1 (patch)
tree84ad301e3470fbe81ae6c82241fa189e59942c70 /cparser
parentc42d68fdeeef7d08b64a900f52d6b295ad31f4f0 (diff)
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
Diffstat (limited to 'cparser')
-rw-r--r--cparser/Parse.ml2
-rw-r--r--cparser/Rename.ml30
2 files changed, 22 insertions, 10 deletions
diff --git a/cparser/Parse.ml b/cparser/Parse.ml
index 2c467a7..0fc85bf 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 0ce401f..76c3c12 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