Move more functionality in the new interface.

Added functions to add more information to the debuging interface,
like the struct layout with offsets, bitifiled layout and removed
the no longer needed mapping from stamp to atom.

15 files changed, 120 insertions, 75 deletions

diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index 29409b32..ea3d985a 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -27,11 +27,10 @@ module Printer(Target:TARGET) =
     let addr_mapping: (string, (int * int)) Hashtbl.t = Hashtbl.create 7
 
     let get_fun_addr name =
-      let name = extern_atom name in
-      let start_addr = new_label ()
-      and end_addr = new_label () in
-      Hashtbl.add addr_mapping name (start_addr,end_addr);
-      start_addr,end_addr
+      let s = new_label ()
+      and e = new_label () in
+      Debug.add_fun_addr name (s,e);
+      s,e
 
     let print_debug_label oc l =
       if !Clflags.option_g && Configuration.advanced_debug then
@@ -120,8 +119,7 @@ module Printer(Target:TARGET) =
         let get_stmt_list_addr = Target.get_stmt_list_addr
         let name_of_section = Target.name_of_section
         let get_fun_addr s = try Some (Hashtbl.find addr_mapping s) with Not_found -> None
-        let get_location a =  try (Target.get_location (stamp_atom a)) with Not_found -> None
-        let get_segment_location a = try (Target.get_segment_location (stamp_atom a)) with Not_found -> None
+        let get_location a =  None
         let get_frame_base a = None
         let symbol = Target.symbol
       end
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 1a6abb6e..e31da76b 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -524,6 +524,11 @@ let convertField env f =
   (intern_string f.fld_name, convertTyp env f.fld_typ)
 
 let convertCompositedef env su id attr members =
+  let t = match su with C.Struct -> 
+    let layout = Cutil.struct_layout env members in
+    List.iter (fun (a,b) -> Debug.set_member_offset id a b) layout;
+    TStruct (id,attr) | C.Union -> TUnion (id,attr) in
+  Debug.set_composite_size id su (Cutil.sizeof env t);
   Composite(intern_string id.name,
             begin match su with C.Struct -> Struct | C.Union -> Union end,
             List.map (convertField env) members,
@@ -1039,7 +1044,6 @@ let convertFundef loc env fd =
     List.map
       (fun (id, ty) ->
         let id' = intern_string id.name in
-        add_stamp id.stamp id';
         (id', convertTyp env ty))
       fd.fd_params in
   let vars =
@@ -1050,7 +1054,6 @@ let convertFundef loc env fd =
         if init <> None then
           unsupported "initialized local variable";
         let id' = intern_string id.name in
-        add_stamp id.stamp id';
         (id', convertTyp env ty))
       fd.fd_locals in
   let body' = convertStmt loc env fd.fd_body in
@@ -1079,7 +1082,7 @@ let convertFundecl env (sto, id, ty, optinit) =
     | Tfunction(args, res, cconv) -> (args, res, cconv)
     | _ -> assert false in
   let id' = intern_string id.name in
-  add_stamp id.stamp id';
+  Debug.atom_function id id';
   let sg = signature_of_type args res cconv in
   let ef =
     if id.name = "malloc" then EF_malloc else
@@ -1121,7 +1124,7 @@ let convertInitializer env ty i =
 
 let convertGlobvar loc env (sto, id, ty, optinit) =
   let id' = intern_string id.name in
-  add_stamp id.stamp id';
+  Debug.atom_global_variable id id';
   let ty' = convertTyp env ty in 
   let sz = Ctypes.sizeof !comp_env ty' in
   let al = Ctypes.alignof !comp_env ty' in
diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml
index 6569bb4c..8d43e689 100644
--- a/cparser/Bitfields.ml
+++ b/cparser/Bitfields.ml
@@ -134,6 +134,7 @@ let rec transf_members env id count = function
                   if !config.bitfields_msb_first
                   then sizeof_ikind carrier_ikind * 8 - pos - sz
                   else pos in
+                Debug.set_bitfield_offset id name pos' carrier (sizeof_ikind carrier_ikind);
                 Hashtbl.add bitfield_table
                   (id, name)
                   {bf_carrier = carrier; bf_carrier_typ = carrier_typ;
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index a3c05c34..90bbfe5a 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -427,7 +427,6 @@ let sizeof_union env members =
    We lay out fields consecutively, inserting padding to preserve
    their alignment.
    Not done here but in composite_info_decl: rounding size to alignment. *)
-
 let sizeof_struct env members =
   let rec sizeof_rec ofs = function
   | [] ->
@@ -449,6 +448,26 @@ let sizeof_struct env members =
       end
   in sizeof_rec 0 members
 
+(* Simplified version to compute offsets on structs without bitfields *)
+let struct_layout env members =
+  let rec struct_layout_rec mem ofs = function
+    | [] ->
+        mem
+    | [ { fld_typ = TArray(_, None, _) } as m ] ->
+      (* C99: ty[] allowed as last field *)
+      begin match alignof env m.fld_typ with
+      | Some a -> ( m.fld_name,align ofs a)::mem
+      | None -> []
+      end
+    | m :: rem ->
+        match alignof env m.fld_typ, sizeof env m.fld_typ with
+        | Some a, Some s -> 
+            let offset = align ofs a in
+            struct_layout_rec ((m.fld_name,offset)::mem) (offset + s) rem
+        | _, _ -> []
+  in struct_layout_rec [] 0 members
+
+
 (* Determine whether a type is incomplete *)
 
 let incomplete_type env t =
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index b1f77944..b9879339 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -105,6 +105,8 @@ val composite_info_decl:
   Env.t -> struct_or_union -> attributes -> Env.composite_info
 val composite_info_def:
   Env.t -> struct_or_union -> attributes -> field list -> Env.composite_info
+val struct_layout:
+  Env.t -> field list -> (string * int) list
 
 (* Type classification functions *)
 
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index de24871f..ca5865dd 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -56,9 +56,11 @@ let elab_loc l = (l.filename, l.lineno)
 
 let top_declarations = ref ([] : globdecl list)
 
-let emit_elab loc td =
+let emit_elab env loc td =
   let loc = elab_loc loc in
-  top_declarations := { gdesc = td; gloc = loc } :: !top_declarations
+  let dec ={ gdesc = td; gloc = loc } in
+  Debug.insert_global_declaration env dec;
+  top_declarations := dec :: !top_declarations
 
 let reset() = top_declarations := []
 
@@ -730,7 +732,7 @@ and elab_struct_or_union only kind loc tag optmembers attrs env =
       (* finishing the definition of an incomplete struct or union *)
       let (ci', env') = elab_struct_or_union_info kind loc env members attrs in
       (* Emit a global definition for it *)
-      emit_elab loc (Gcompositedef(kind, tag', attrs, ci'.ci_members));
+      emit_elab env' loc (Gcompositedef(kind, tag', attrs, ci'.ci_members));
       (* Replace infos but keep same ident *)
       (tag', Env.add_composite env' tag' ci')
   | Some(tag', {ci_sizeof = Some _}), Some _
@@ -745,7 +747,7 @@ and elab_struct_or_union only kind loc tag optmembers attrs env =
       (* enter it with a new name *)
       let (tag', env') = Env.enter_composite env tag ci in
       (* emit it *)
-      emit_elab loc (Gcompositedecl(kind, tag', attrs));
+      emit_elab env' loc (Gcompositedecl(kind, tag', attrs));
       (tag', env')
   | _, Some members ->
       (* definition of a complete struct or union *)
@@ -753,12 +755,12 @@ and elab_struct_or_union only kind loc tag optmembers attrs env =
       (* enter it, incomplete, with a new name *)
       let (tag', env') = Env.enter_composite env tag ci1 in
       (* emit a declaration so that inner structs and unions can refer to it *)
-      emit_elab loc (Gcompositedecl(kind, tag', attrs));
+      emit_elab env' loc (Gcompositedecl(kind, tag', attrs));
       (* elaborate the members *)
       let (ci2, env'') =
         elab_struct_or_union_info kind loc env' members attrs in
       (* emit a definition *)
-      emit_elab loc (Gcompositedef(kind, tag', attrs, ci2.ci_members));
+      emit_elab env'' loc (Gcompositedef(kind, tag', attrs, ci2.ci_members));
       (* Replace infos but keep same ident *)
       (tag', Env.add_composite env'' tag' ci2)
 
@@ -809,7 +811,7 @@ and elab_enum only loc tag optmembers attrs env =
       let (dcls, env') = elab_members env 0L members in
       let info = { ei_members = dcls; ei_attr = attrs } in
       let (tag', env'') = Env.enter_enum env' tag info in
-      emit_elab loc (Genumdef(tag', attrs, dcls));
+      emit_elab env' loc (Genumdef(tag', attrs, dcls));
       (tag', env'')
 
 (* Elaboration of a naked type, e.g. in a cast *)
@@ -1312,7 +1314,7 @@ let elab_expr loc env a =
             let ty = TFun(TInt(IInt, []), None, false, []) in
             (* Emit an extern declaration for it *)
             let id = Env.fresh_ident n in
-            emit_elab loc (Gdecl(Storage_extern, id, ty, None));
+            emit_elab env loc (Gdecl(Storage_extern, id, ty, None));
             { edesc = EVar id; etyp = ty }
         | _ -> elab a1 in
       let bl = List.map elab al in
@@ -1789,7 +1791,7 @@ let enter_typedefs loc env sto dl =
     if redef Env.lookup_ident env s then
       error loc "redefinition of identifier '%s' as different kind of symbol" s;
     let (id, env') = Env.enter_typedef env s ty in
-    emit_elab loc (Gtypedef(id, ty));
+    emit_elab env loc (Gtypedef(id, ty));
     env') env dl
 
 let enter_or_refine_ident local loc env s sto ty =
@@ -1865,7 +1867,7 @@ let enter_decdefs local loc env sto dl =
       ((sto', id, ty', init') :: decls, env2)
     else begin
       (* Global definition *)
-      emit_elab loc (Gdecl(sto', id, ty', init'));
+      emit_elab env2 loc (Gdecl(sto', id, ty', init'));
       (decls, env2)
     end in
   let (decls, env') = List.fold_left enter_decdef ([], env) dl in
@@ -1899,7 +1901,7 @@ let elab_fundef env spec name body loc =
   let (func_ty, func_init) = __func__type_and_init s in
   let (func_id, _, env3,func_ty) =
     enter_or_refine_ident true loc env2 "__func__" Storage_static func_ty in
-  emit_elab loc (Gdecl(Storage_static, func_id, func_ty, Some func_init));
+  emit_elab env3 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 *)
@@ -1925,7 +1927,7 @@ let elab_fundef env spec name body loc =
       fd_vararg = vararg;
       fd_locals = [];
       fd_body = body'' } in
-  emit_elab loc (Gfundef fn);
+  emit_elab env1 loc (Gfundef fn);
   env1
 
 let elab_kr_fundef env spec name params defs body loc =
@@ -1997,7 +1999,7 @@ let rec elab_definition (local: bool) (env: Env.t) (def: Cabs.definition)
 
   (* pragma *)
   | PRAGMA(s, loc) ->
-      emit_elab loc (Gpragma s);
+      emit_elab env loc (Gpragma s);
       ([], env)
 
 and elab_definitions local env = function
diff --git a/cparser/Parse.ml b/cparser/Parse.ml
index c9564c08..2be3a612 100644
--- a/cparser/Parse.ml
+++ b/cparser/Parse.ml
@@ -24,12 +24,7 @@ let transform_program t p name =
   (run_pass Unblock.program 'b'
   (run_pass Bitfields.program 'f'
   p)))) in
-  let debug = 
-    if !Clflags.option_g && Configuration.advanced_debug then
-      Some (CtoDwarf.program_to_dwarf p p1 name)
-    else
-      None in
-  (Rename.program p1 (Filename.chop_suffix name ".c")),debug
+  (Rename.program p1 (Filename.chop_suffix name ".c"))
 
 let parse_transformations s =
   let t = ref CharSet.empty in
@@ -46,7 +41,7 @@ let parse_transformations s =
 let preprocessed_file transfs name sourcefile =
   Cerrors.reset();
   let ic = open_in sourcefile in
-  let p,d =
+  let p =
     try
       let t = parse_transformations transfs in
       let lb = Lexer.init name ic in
@@ -65,6 +60,6 @@ let preprocessed_file transfs name sourcefile =
       Timing.time2 "Emulations" transform_program t p1 name
     with
     | Cerrors.Abort ->
-        [],None in
+        [] in
   close_in ic;
-  if Cerrors.check_errors() then None,None else Some p,d
+  if Cerrors.check_errors() then None else Some p
diff --git a/cparser/Parse.mli b/cparser/Parse.mli
index ac8feb70..58c3cfb9 100644
--- a/cparser/Parse.mli
+++ b/cparser/Parse.mli
@@ -15,7 +15,7 @@
 
 (* Entry point for the library: parse, elaborate, and transform *)
 
-val preprocessed_file: string -> string -> string -> C.program option * DwarfTypes.dw_entry option
+val preprocessed_file: string -> string -> string -> C.program option
 
 (* first arg: desired transformations
    second arg: source file name before preprocessing
diff --git a/debug/Debug.ml b/debug/Debug.ml
index eb195b33..ab20f630 100644
--- a/debug/Debug.ml
+++ b/debug/Debug.ml
@@ -21,9 +21,11 @@ type implem =
      mutable init: string -> unit;
      mutable atom_function: ident -> atom -> unit;
      mutable atom_global_variable: ident -> atom -> unit;
-     mutable set_composite_size: ident -> struct_or_union -> int -> unit;
-     mutable set_member_offset: ident -> string -> int -> int -> unit;
-     mutable insert_declaration: globdecl -> Env.t -> unit;
+     mutable set_composite_size: ident -> struct_or_union -> int option -> unit;
+     mutable set_member_offset: ident -> string -> int -> unit;
+     mutable set_bitfield_offset: ident -> string -> int -> string -> int -> unit;
+     mutable insert_global_declaration: Env.t -> globdecl -> unit;
+     mutable add_fun_addr: atom -> (int * int) -> unit
    }
 
 let implem =
@@ -32,8 +34,10 @@ let implem =
    atom_function = (fun _ _ -> ());
    atom_global_variable = (fun _ _ -> ());
    set_composite_size = (fun _ _ _ -> ());
-   set_member_offset = (fun _ _ _ _ -> ());
-   insert_declaration = (fun _ _ -> ());
+   set_member_offset = (fun _ _  _ -> ());
+   set_bitfield_offset = (fun _ _ _ _ _ -> ());
+   insert_global_declaration = (fun _ _ -> ());
+   add_fun_addr = (fun _ _ -> ());
  }
 
 let init () =
@@ -43,19 +47,25 @@ let init () =
     implem.atom_global_variable <- DebugInformation.atom_global_variable;
     implem.set_composite_size <- DebugInformation.set_composite_size;
     implem.set_member_offset <- DebugInformation.set_member_offset;
-    implem.insert_declaration <- DebugInformation.insert_declaration;
+    implem.set_bitfield_offset <- DebugInformation.set_bitfield_offset;
+    implem.insert_global_declaration <- DebugInformation.insert_global_declaration;
+    implem.add_fun_addr <- DebugInformation.add_fun_addr;
   end else begin
-   implem.init <- (fun _ -> ());
-   implem.atom_function <- (fun _ _ -> ());
-   implem.atom_global_variable <- (fun _ _ -> ());
-   implem.set_composite_size <- (fun _ _ _ -> ());
-   implem.set_member_offset <- (fun _ _ _ _ -> ());
-   implem.insert_declaration <- (fun _ _ -> ())
+    implem.init <- (fun _ -> ());
+    implem.atom_function <- (fun _ _ -> ());
+    implem.atom_global_variable <- (fun _ _ -> ());
+    implem.set_composite_size <- (fun _ _ _ -> ());
+    implem.set_member_offset <- (fun _ _ _ -> ());
+    implem.set_bitfield_offset <- (fun _ _ _ _ _ -> ());
+    implem.insert_global_declaration <- (fun _ _ -> ());
+    implem.add_fun_addr <- (fun _ _ -> ())
   end
 
 let init_compile_unit name = implem.init name
 let atom_function id atom = implem.atom_function id atom
 let atom_global_variable id atom = implem.atom_global_variable id atom
 let set_composite_size id sou size = implem.set_composite_size id sou size
-let set_member_offset id field off size = implem.set_member_offset id field off size
-let insert_declaration dec env = implem.insert_declaration dec env
+let set_member_offset id field off = implem.set_member_offset id field off
+let set_bitfield_offset id field off underlying size = implem.set_bitfield_offset id field off underlying size
+let insert_global_declaration env dec = implem.insert_global_declaration env dec
+let add_fun_addr atom addr = implem.add_fun_addr atom addr
diff --git a/debug/Debug.mli b/debug/Debug.mli
index ea72aeb4..ae32af5b 100644
--- a/debug/Debug.mli
+++ b/debug/Debug.mli
@@ -18,6 +18,8 @@ val init: unit -> unit
 val init_compile_unit: string -> unit
 val atom_function: ident -> atom -> unit
 val atom_global_variable: ident -> atom -> unit
-val set_composite_size: ident -> struct_or_union -> int -> unit
-val set_member_offset: ident -> string -> int -> int -> unit
-val insert_declaration: globdecl -> Env.t -> unit
+val set_composite_size: ident -> struct_or_union -> int option -> unit
+val set_member_offset: ident -> string -> int -> unit
+val set_bitfield_offset: ident -> string -> int -> string -> int -> unit
+val insert_global_declaration:  Env.t -> globdecl -> unit
+val add_fun_addr: atom -> (int * int) -> unit
diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml
index 30d026c7..53f73115 100644
--- a/debug/DebugInformation.ml
+++ b/debug/DebugInformation.ml
@@ -343,7 +343,9 @@ type function_information = {
     fun_return_type: int option; (* Again the special case of void functions *)
     fun_vararg:      bool;
     fun_parameter:   parameter_information list;
-    fun_locals:       int list;
+    fun_locals:      int list;
+    fun_low_pc:      int option;
+    fun_high_pc:     int option;
   }
 
 type definition_type =
@@ -373,6 +375,13 @@ let find_fun_stamp id =
   | Function f -> id,f
   |  _ -> assert false
 
+let find_fun_atom id =
+  let id = (Hashtbl.find atom_to_definition id) in
+  let f = Hashtbl.find definitions id in
+  match f with
+  | Function f -> id,f
+  |  _ -> assert false
+
 
 let replace_var id var =
   let var = GlobalVariable var in
@@ -388,7 +397,7 @@ let gen_comp_typ sou id at =
   else
     TUnion (id,at)
 
-let insert_declaration dec env =
+let insert_global_declaration env dec=
   let insert d_dec stamp =
     let id = next_id () in
     Hashtbl.add definitions id d_dec;
@@ -441,6 +450,8 @@ let insert_declaration dec env =
         fun_vararg = f.fd_vararg;
         fun_parameter = params;
         fun_locals = [];
+        fun_low_pc = None;
+        fun_high_pc = None;
       } in
       insert (Function fd) f.fd_name.stamp
   | Gcompositedecl (sou,id,at) -> 
@@ -481,18 +492,28 @@ let insert_declaration dec env =
         {en with enum_file_loc = Some dec.gloc; enum_enumerators = enumerator;})
   | Gpragma _ -> ()
 
-let set_member_offset str field offset byte_size =
+let set_member_offset str field offset =
   let id = find_type (TStruct (str,[])) in
   replace_composite id (fun comp ->
     let name f = f.cfd_name = field || match f.cfd_bitfield with Some n -> n = field | _ -> false in 
     let members = List.map (fun a -> if name a then
-          {a with cfd_byte_offset = Some offset; cfd_byte_size = Some byte_size;}
+          {a with cfd_byte_offset = Some offset;}
       else a) comp.ct_members in
     {comp with ct_members = members;})
 
 let set_composite_size comp sou size =
   let id = find_type (gen_comp_typ sou comp []) in
-  replace_composite id (fun comp -> {comp with ct_sizeof = Some size;}) 
+  replace_composite id (fun comp -> {comp with ct_sizeof = size;}) 
+
+let set_bitfield_offset str field offset underlying size =
+  let id = find_type (TStruct (str,[])) in
+  replace_composite id (fun comp ->
+    let name f = f.cfd_name = field in
+    let members = List.map (fun a -> if name a then
+      {a with cfd_bit_offset = Some offset; cfd_bitfield = Some underlying; cfd_byte_size = Some size}
+    else
+      a) comp.ct_members in
+    {comp with ct_members = members;})
 
 let atom_global_variable id atom = 
   let id,var = find_var_stamp id.stamp in
@@ -504,6 +525,10 @@ let atom_function id atom =
   replace_fun id ({f with fun_atom = Some atom;});
   Hashtbl.add atom_to_definition atom id
 
+let add_fun_addr atom (high,low) =
+  let id,f = find_fun_atom atom in
+  replace_fun id ({f with fun_high_pc = Some high; fun_low_pc = Some low;})
+
 let init name =
   id := 0;
   file_name := name;
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml
index c85a9efc..09cf72eb 100644
--- a/debug/DwarfPrinter.ml
+++ b/debug/DwarfPrinter.ml
@@ -130,7 +130,6 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
           add_attr_some e.formal_parameter_artificial (add_abbr_entry (0x34,artificial_type_abbr));
           add_location  (get_location e.formal_parameter_id) buf;
           add_attr_some e.formal_parameter_name add_name;
-          add_location  (get_segment_location e.formal_parameter_id) buf;
           add_type buf;
           add_attr_some e.formal_parameter_variable_parameter (add_abbr_entry (0x4b,variable_parameter_type_abbr))
       | DW_TAG_label _ ->
@@ -205,7 +204,6 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
           add_attr_some e.variable_external (add_abbr_entry (0x3f,external_type_abbr));
           add_location  (get_location e.variable_id) buf;
           add_name buf;
-          add_location  (get_segment_location e.variable_id) buf;
           add_type buf
       | DW_TAG_volatile_type _ ->
           prologue 0x35;
@@ -367,7 +365,6 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
       print_opt_value oc fp.formal_parameter_artificial print_flag;
       print_opt_value oc (get_location fp.formal_parameter_id) print_loc;
       print_opt_value oc fp.formal_parameter_name print_string;
-      print_opt_value oc  (get_segment_location fp.formal_parameter_id) print_loc;
       print_ref oc fp.formal_parameter_type;
       print_opt_value oc fp.formal_parameter_variable_parameter print_flag
 
@@ -441,7 +438,6 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
       print_opt_value oc var.variable_external print_flag;
       print_opt_value oc (get_location var.variable_id) print_loc;
       print_string oc var.variable_name;
-      print_opt_value oc (get_segment_location var.variable_id) print_loc;
       print_ref oc var.variable_type
 
     let print_volatile_type oc vt =
diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli
index 174f2403..b852d1f4 100644
--- a/debug/DwarfTypes.mli
+++ b/debug/DwarfTypes.mli
@@ -270,7 +270,6 @@ module type DWARF_TARGET=
     val name_of_section: section_name -> string
     val get_fun_addr: string -> (int * int) option
     val get_location: int -> location_value option
-    val get_segment_location: int -> location_value option
     val get_frame_base: int -> location_value option
     val symbol: out_channel -> atom -> unit
   end
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 04acf902..47d6e81c 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -108,6 +108,7 @@ let preprocess ifile ofile =
 (* From preprocessed C to Csyntax *)
 
 let parse_c_file sourcename ifile =
+  Debug.init_compile_unit sourcename;
   Sections.initialize();
   (* Simplification options *)
   let simplifs =
@@ -117,10 +118,10 @@ let parse_c_file sourcename ifile =
   ^ (if !option_fpacked_structs then "p" else "")
   in
   (* Parsing and production of a simplified C AST *)
-  let ast,debug =
+  let ast =
     match Parse.preprocessed_file simplifs sourcename ifile with
-    | None,_ -> exit 2
-    | Some p,d -> p,d in
+    | None -> exit 2
+    | Some p -> p in
   (* Save C AST if requested *)
   if !option_dparse then begin
     let ofile = output_filename sourcename ".c" ".parsed.c" in
@@ -141,7 +142,7 @@ let parse_c_file sourcename ifile =
     PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax;
     close_out oc
   end;
-  csyntax,debug
+  csyntax,None
 
 (* Dump Asm code in binary format for the validator *)
 
diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml
index 5eb52e88..c50b3230 100644
--- a/lib/Camlcoq.ml
+++ b/lib/Camlcoq.ml
@@ -284,7 +284,6 @@ let coqint_of_camlint64 : int64 -> Integers.Int64.int = Z.of_uint64
 type atom = positive
 
 let atom_of_string = (Hashtbl.create 17 : (string, atom) Hashtbl.t)
-let atom_of_stamp = (Hashtbl.create 17: (int, atom) Hashtbl.t)
 let string_of_atom = (Hashtbl.create 17 : (atom, string) Hashtbl.t)
 let next_atom = ref Coq_xH
 
@@ -296,14 +295,7 @@ let intern_string s =
     next_atom := Pos.succ !next_atom;
     Hashtbl.add atom_of_string s a;
     Hashtbl.add string_of_atom a s;
-    a
-
-let add_stamp s a =
-  Hashtbl.add atom_of_stamp s a
-
-let stamp_atom s =
-  Hashtbl.find atom_of_stamp s
-  
+    a 
 let extern_atom a =
   try
     Hashtbl.find string_of_atom a