aboutsummaryrefslogtreecommitdiffstats
path: root/debug
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-09-30 11:13:34 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-09-30 11:13:34 +0200
commitc0757aa180c54ff61093e8079ef58b77775ba28e (patch)
treed9ada5db4dd2789ecc61d75c0ba8d2116bdf56ce /debug
parent05acff8bcb4f127a6f0ff6c587ba38d1c8cbe2fc (diff)
downloadcompcert-kvx-c0757aa180c54ff61093e8079ef58b77775ba28e.tar.gz
compcert-kvx-c0757aa180c54ff61093e8079ef58b77775ba28e.zip
Avoid problem with implict declarations.
In order to avoid the problem that the stamp is not correct for implict declarations I insert all possible stamps of a function into my mapping and assign them one debug id.
Diffstat (limited to 'debug')
-rw-r--r--debug/DebugInformation.ml21
-rw-r--r--debug/Dwarfgen.ml1
2 files changed, 18 insertions, 4 deletions
diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml
index 73f9163a..3bf26e53 100644
--- a/debug/DebugInformation.ml
+++ b/debug/DebugInformation.ml
@@ -387,6 +387,9 @@ let definitions: (int,definition_type) Hashtbl.t = Hashtbl.create 7
(* Mapping from stamp to debug id *)
let stamp_to_definition: (int,int) Hashtbl.t = Hashtbl.create 7
+(* Mapping from name to debug id *)
+let name_to_definition: (string,int) Hashtbl.t = Hashtbl.create 7
+
(* Mapping from atom to debug id *)
let atom_to_definition: (atom, int) Hashtbl.t = Hashtbl.create 7
@@ -510,8 +513,13 @@ let insert_global_declaration env dec=
let id,var = find_gvar_stamp id.stamp in
replace_var id ({var with gvar_declaration = false;})
end
- end
- | Gfundef f ->
+ end else if not (Hashtbl.mem name_to_definition id.name) then begin
+ (* Implict declarations need special handling *)
+ let id' = next_id () in
+ Hashtbl.add stamp_to_definition id.stamp id';
+ Hashtbl.add name_to_definition id.name id'
+ end
+ | Gfundef f ->
let ret = (match f.fd_ret with
| TVoid _ -> None
| _ -> Some (insert_type f.fd_ret)) in
@@ -539,7 +547,13 @@ let insert_global_declaration env dec=
fun_high_pc = None;
fun_scope = None;
} in
- insert (Function fd) f.fd_name.stamp
+ begin try
+ let id' = Hashtbl.find name_to_definition f.fd_name.name in
+ Hashtbl.add stamp_to_definition f.fd_name.stamp id';
+ Hashtbl.add definitions id' (Function fd)
+ with Not_found ->
+ insert (Function fd) f.fd_name.stamp
+ end
| Gcompositedecl (sou,id,at) ->
ignore (insert_type (gen_comp_typ sou id at));
let id = find_type (gen_comp_typ sou id []) in
@@ -798,6 +812,7 @@ let init name =
Hashtbl.reset lookup_types;
Hashtbl.reset definitions;
Hashtbl.reset stamp_to_definition;
+ Hashtbl.reset name_to_definition;
Hashtbl.reset atom_to_definition;
Hashtbl.reset local_variables;
Hashtbl.reset stamp_to_local;
diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml
index ac32f9f1..3239ceb6 100644
--- a/debug/Dwarfgen.ml
+++ b/debug/Dwarfgen.ml
@@ -235,7 +235,6 @@ let needs_types id d =
| Void
| EnumType _ -> d,false
| Typedef t ->
- Printf.printf "Typedef %s\n" t.typedef_name;
add_type (get_opt_val t.typ) d
| PointerType p ->
add_type p.pts d