Merge pull request #56 from AbsInt/debug_locations

Debug locations

33 files changed, 2257 insertions, 909 deletions

diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index f7f0d313..86f9f973 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -152,7 +152,8 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
       | Section_user(s, wr, ex) ->
           sprintf ".section	\"%s\",\"a%s%s\",%%progbits"
             s (if wr then "w" else "") (if ex then "x" else "")
-      | Section_debug_info
+      | Section_debug_info _
+      | Section_debug_loc
       | Section_debug_abbrev -> "" (* Dummy value *)
             
     let section oc sec =
@@ -905,9 +906,9 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
     let get_end_addr () = -1 (* Dummy constant *)
 
     let get_stmt_list_addr () = -1 (* Dummy constant *)
-
-    module DwarfAbbrevs = DwarfUtil.DefaultAbbrevs (* Dummy Abbrev types *)
         
+    let get_debug_start_addr () = -1 (* Dummy constant *)
+       
     let label = elf_label
        
     let new_label = new_label
diff --git a/backend/Constprop.v b/backend/Constprop.v
index cd844d30..8f4cb76d 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -144,9 +144,9 @@ Fixpoint debug_strength_reduction (ae: AE.t) (al: list (builtin_arg reg)) :=
   | a :: al =>
       let a' := builtin_arg_reduction ae a in
       let al' := a :: debug_strength_reduction ae al in
-      match a' with
-      | BA_int _ | BA_long _ | BA_float _ | BA_single _ => a' :: al'
-      | _ => al'
+      match a, a' with
+      | BA _, (BA_int _ | BA_long _ | BA_float _ | BA_single _) => a' :: al'
+      | _, _ => al'
       end
   end.
 
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index d9005f5e..eafefed5 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -243,7 +243,11 @@ Proof.
   induction 2; simpl.
 - exists (@nil val); constructor.
 - destruct IHlist_forall2 as (vl' & A).
-  destruct (builtin_arg_reduction ae a1); repeat (eauto; econstructor). 
+  assert (eval_builtin_args ge (fun r => rs#r) sp m
+             (a1 :: debug_strength_reduction ae al) (b1 :: vl'))
+  by (constructor; eauto).
+  destruct a1; try (econstructor; eassumption).
+  destruct (builtin_arg_reduction ae (BA x)); repeat (eauto; econstructor). 
 Qed.
 
 Lemma builtin_strength_reduction_correct:
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index f3c80f3e..a152e3c2 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -24,14 +24,11 @@ open TargetPrinter
 module Printer(Target:TARGET) =
   struct
 
-    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 = Target.new_label ()
+      and e = Target.new_label () in
+      Debug.add_fun_addr name (e,s);
+      s,e
 
     let print_debug_label oc l =
       if !Clflags.option_g && Configuration.advanced_debug then
@@ -39,7 +36,6 @@ module Printer(Target:TARGET) =
       else
         ()
 
-
     let print_location oc loc =
       if loc <> Cutil.no_loc then Target.print_file_line oc (fst loc) (snd loc)
           
@@ -67,7 +63,9 @@ module Printer(Target:TARGET) =
       print_debug_label oc e;
       Target.print_fun_info oc name;
       Target.emit_constants oc lit;
-      Target.print_jumptable oc jmptbl
+      Target.print_jumptable oc jmptbl;
+      if !Clflags.option_g then
+        Hashtbl.iter (fun p i -> Debug.add_label name p i) current_function_labels
     
     let print_init_data oc name id =
       if Str.string_match PrintCsyntax.re_string_literal (extern_atom name) 0
@@ -102,8 +100,7 @@ module Printer(Target:TARGET) =
             let sz =
               match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in
             Target.print_comm_symb oc sz name align
-              
-              
+                            
     let print_globdef oc (name,gdef) =
       match gdef with
       | Gfun (Internal code) -> print_function oc name code
@@ -113,18 +110,13 @@ module Printer(Target:TARGET) =
     module DwarfTarget: DwarfTypes.DWARF_TARGET =
       struct
         let label = Target.label
-        let name_of_section = Target.name_of_section
+        let section = Target.section
         let print_file_loc = Target.print_file_loc
-        let get_start_addr = Target.get_start_addr   
-        let get_end_addr = Target.get_end_addr
-        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 symbol = Target.symbol
       end
 
-    module DebugPrinter = DwarfPrinter (DwarfTarget) (Target.DwarfAbbrevs)
-      
-     
+    module DebugPrinter = DwarfPrinter (DwarfTarget)     
   end
 
 let print_program oc p db =
@@ -138,7 +130,14 @@ let print_program oc p db =
   close_filenames ();
   if !Clflags.option_g && Configuration.advanced_debug then
     begin
-      match db with
+      let atom_to_s s =
+        let s = C2C.atom_sections s in
+        match s with
+        | [] -> Target.name_of_section Section_text
+        | (Section_user (n,_,_))::_ -> n
+        | a::_ ->
+            Target.name_of_section a in
+      match Debug.generate_debug_info atom_to_s (Target.name_of_section Section_text) with
       | None -> ()
       | Some db ->
           Printer.DebugPrinter.print_debug oc db
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 67e53aea..1c3b47b5 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -48,10 +48,10 @@ module type TARGET =
       val get_start_addr: unit -> int
       val get_end_addr: unit -> int
       val get_stmt_list_addr: unit -> int
+      val get_debug_start_addr: unit -> int
       val new_label: unit -> int
       val label: out_channel -> int -> unit
       val print_file_loc: out_channel -> file_loc -> unit
-      module DwarfAbbrevs:  DWARF_ABBREVS
     end
 
 (* On-the-fly label renaming *)
@@ -140,12 +140,6 @@ let coqint oc n =
   fprintf oc "%ld" (camlint_of_coqint n)
 
 (* Printing annotations in asm syntax *)
-(** All files used in the debug entries *)
-module StringSet = Set.Make(String)
-let all_files : StringSet.t ref = ref StringSet.empty
-let add_file file =
-  all_files := StringSet.add file !all_files
-
 
 let filename_info : (string, int * Printlines.filebuf option) Hashtbl.t
                   = Hashtbl.create 7
@@ -283,6 +277,9 @@ let print_debug_info comment print_line print_preg sp_name oc kind txt args =
   | 5 ->  (* local variable preallocated in stack *)
       fprintf oc "%s debug: %s resides at%a\n"
                  comment txt print_debug_args args
+  | 6 ->  (* scope annotations *)
+      fprintf oc "%s debug: current scopes%a\n"
+                 comment print_debug_args args;
   | _ ->
       ()
 					    
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 5cd5997d..bd281374 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -524,6 +524,13 @@ 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,
@@ -741,6 +748,22 @@ let rec convertExpr env e =
   | C.ECompound(ty1, ie) ->
       unsupported "compound literals"; ezero
 
+  | C.ECall({edesc = C.EVar {name = "__builtin_debug"}}, args) ->
+      let (kind, args1) =
+        match args with
+        | {edesc = C.EConst(CInt(n,_,_))} :: args1 -> (n, args1)
+        | _ -> error "ill_formed __builtin_debug"; (0L, args) in
+      let (text, args2) =
+        match args1 with
+        | {edesc = C.EConst(CStr(txt))} :: args2 -> (txt, args2)
+        | {edesc = C.EVar id} :: args2 -> (id.name, args2)
+        | _ -> error "ill_formed __builtin_debug"; ("", args1) in
+      let targs2 = convertTypArgs env [] args2 in
+      Ebuiltin(
+        EF_debug(P.of_int64 kind, intern_string text,
+                 typlist_of_typelist targs2),
+        targs2, convertExprList env args2, convertTyp env e.etyp)
+ 
   | C.ECall({edesc = C.EVar {name = "__builtin_annot"}}, args) ->
       begin match args with
       | {edesc = C.EConst(CStr txt)} :: args1 ->
@@ -922,16 +945,6 @@ let rec contains_case s =
 
 (** Annotations for line numbers *)
 
-let add_lineno prev_loc this_loc s =
-  if !Clflags.option_g && prev_loc <> this_loc && this_loc <> Cutil.no_loc
-  then begin
-    let txt = sprintf "#line:%s:%d" (fst this_loc) (snd this_loc) in
-     Ssequence(Sdo(Ebuiltin(EF_debug(P.one, intern_string txt, []),
-                            Tnil, Enil, Tvoid)),
-               s)
-  end else
-    s
-
 (** Statements *)
 
 let swrap = function
@@ -939,36 +952,31 @@ let swrap = function
   | Errors.Error msg ->
       error ("retyping error: " ^  string_of_errmsg msg); Sskip
 
-let rec convertStmt ploc env s =
+let rec convertStmt env s =
   updateLoc s.sloc;
   match s.sdesc with
   | C.Sskip ->
       Sskip
   | C.Sdo e ->
-      add_lineno ploc s.sloc (swrap (Ctyping.sdo (convertExpr env e)))
+      swrap (Ctyping.sdo (convertExpr env e))
   | C.Sseq(s1, s2) ->
-      let s1' = convertStmt ploc env s1 in
-      let s2' = convertStmt s1.sloc env s2 in
+      let s1' = convertStmt env s1 in
+      let s2' = convertStmt env s2 in
       Ssequence(s1', s2')
   | C.Sif(e, s1, s2) ->
       let te = convertExpr env e in
-      add_lineno ploc s.sloc 
-        (swrap (Ctyping.sifthenelse te 
-                      (convertStmt s.sloc env s1) (convertStmt s.sloc env s2)))
+      swrap (Ctyping.sifthenelse te (convertStmt env s1) (convertStmt env s2))
   | C.Swhile(e, s1) ->
       let te = convertExpr env e in
-      add_lineno ploc s.sloc
-        (swrap (Ctyping.swhile te (convertStmt s.sloc env s1)))
+      swrap (Ctyping.swhile te (convertStmt env s1))
   | C.Sdowhile(s1, e) ->
       let te = convertExpr env e in
-      add_lineno ploc s.sloc
-        (swrap (Ctyping.sdowhile te (convertStmt s.sloc env s1)))
+      swrap (Ctyping.sdowhile te (convertStmt env s1))
   | C.Sfor(s1, e, s2, s3) ->
       let te = convertExpr env e in
-      add_lineno ploc s.sloc
-        (swrap (Ctyping.sfor
-                      (convertStmt s.sloc env s1) te
-                      (convertStmt s.sloc env s2) (convertStmt s.sloc env s3)))
+      swrap (Ctyping.sfor
+                  (convertStmt env s1) te
+                  (convertStmt env s2) (convertStmt env s3))
   | C.Sbreak ->
       Sbreak
   | C.Scontinue ->
@@ -981,22 +989,20 @@ let rec convertStmt ploc env s =
           contains_case init
         end;
       let te = convertExpr env e in
-      add_lineno ploc s.sloc
-        (swrap (Ctyping.sswitch te
-                    (convertSwitch s.sloc env (is_longlong env e.etyp) cases)))
+      swrap (Ctyping.sswitch te
+               (convertSwitch env (is_longlong env e.etyp) cases))
   | C.Slabeled(C.Slabel lbl, s1) ->
-      add_lineno ploc s.sloc
-        (Slabel(intern_string lbl, convertStmt s.sloc env s1))
+      Slabel(intern_string lbl, convertStmt env s1)
   | C.Slabeled(C.Scase _, _) ->
       unsupported "'case' outside of 'switch'"; Sskip
   | C.Slabeled(C.Sdefault, _) ->
       unsupported "'default' outside of 'switch'"; Sskip
   | C.Sgoto lbl ->
-      add_lineno ploc s.sloc (Sgoto(intern_string lbl))
+      Sgoto(intern_string lbl)
   | C.Sreturn None ->
-      add_lineno ploc s.sloc (Sreturn None)
+      Sreturn None
   | C.Sreturn(Some e) ->
-      add_lineno ploc s.sloc (Sreturn(Some(convertExpr env e)))
+      Sreturn(Some(convertExpr env e))
   | C.Sblock _ ->
       unsupported "nested blocks"; Sskip
   | C.Sdecl _ ->
@@ -1004,10 +1010,9 @@ let rec convertStmt ploc env s =
   | C.Sasm(attrs, txt, outputs, inputs, clobber) ->
       if not !Clflags.option_finline_asm then
         unsupported "inline 'asm' statement (consider adding option -finline-asm)";
-      add_lineno ploc s.sloc
-        (Sdo (convertAsm s.sloc env txt outputs inputs clobber))
+      Sdo (convertAsm s.sloc env txt outputs inputs clobber)
 
-and convertSwitch ploc env is_64 = function
+and convertSwitch env is_64 = function
   | [] ->
       LSnil
   | (lbl, s) :: rem ->
@@ -1024,7 +1029,7 @@ and convertSwitch ploc env is_64 = function
                               then Z.of_uint64 v
                               else Z.of_uint32 (Int64.to_int32 v))
       in
-      LScons(lbl', convertStmt ploc env s, convertSwitch s.sloc env is_64 rem)
+      LScons(lbl', convertStmt env s, convertSwitch env is_64 rem)
 
 (** Function definitions *)
 
@@ -1038,7 +1043,9 @@ let convertFundef loc env fd =
   let params =
     List.map
       (fun (id, ty) ->
-        (intern_string id.name, convertTyp env ty))
+        let id' = intern_string id.name in
+        Debug.atom_parameter fd.fd_name id id';
+        (id', convertTyp env ty))
       fd.fd_params in
   let vars =
     List.map
@@ -1047,10 +1054,13 @@ let convertFundef loc env fd =
           unsupported "'static' or 'extern' local variable";
         if init <> None then
           unsupported "initialized local variable";
-        (intern_string id.name, convertTyp env ty))
+        let id' = intern_string id.name in
+        Debug.atom_local_variable id id';
+        (id', convertTyp env ty))
       fd.fd_locals in
-  let body' = convertStmt loc env fd.fd_body in
+  let body' = convertStmt env fd.fd_body in
   let id' = intern_string fd.fd_name.name in
+  Debug.atom_function fd.fd_name id';
   Hashtbl.add decl_atom id'
     { a_storage = fd.fd_storage;
       a_alignment = None;
@@ -1116,6 +1126,7 @@ let convertInitializer env ty i =
 
 let convertGlobvar loc env (sto, id, ty, optinit) =
   let id' = intern_string id.name in
+  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/common/Sections.ml b/common/Sections.ml
index c0c95848..be0f415e 100644
--- a/common/Sections.ml
+++ b/common/Sections.ml
@@ -27,8 +27,9 @@ type section_name =
   | Section_literal
   | Section_jumptable
   | Section_user of string * bool (*writable*) * bool (*executable*)
-  | Section_debug_info
+  | Section_debug_info of string
   | Section_debug_abbrev
+  | Section_debug_loc
 
 type access_mode =
   | Access_default
diff --git a/common/Sections.mli b/common/Sections.mli
index e878b9e5..cf6f13b8 100644
--- a/common/Sections.mli
+++ b/common/Sections.mli
@@ -26,8 +26,9 @@ type section_name =
   | Section_literal
   | Section_jumptable
   | Section_user of string * bool (*writable*) * bool (*executable*)
-  | Section_debug_info
+  | Section_debug_info of string
   | Section_debug_abbrev
+  | Section_debug_loc
 
 type access_mode =
   | Access_default
diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml
index fbf57082..d064f4b1 100644
--- a/cparser/Bitfields.ml
+++ b/cparser/Bitfields.ml
@@ -134,6 +134,7 @@ let rec transf_struct_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/Cprint.ml b/cparser/Cprint.ml
index 4ceaa016..1af5af1e 100644
--- a/cparser/Cprint.ml
+++ b/cparser/Cprint.ml
@@ -20,6 +20,8 @@ open C
 
 let print_idents_in_full = ref false
 
+let print_debug_idents = ref false
+
 let print_line_numbers = ref false
 
 let location pp (file, lineno) =
@@ -27,7 +29,9 @@ let location pp (file, lineno) =
     fprintf pp "# %d \"%s\"@ " lineno file
 
 let ident pp i =
-  if !print_idents_in_full
+  if !print_debug_idents
+  then fprintf pp "$%d" i.stamp
+  else if !print_idents_in_full
   then fprintf pp "%s$%d" i.name i.stamp
   else fprintf pp "%s" i.name
 
diff --git a/cparser/Cprint.mli b/cparser/Cprint.mli
index d63e341c..349b5f9a 100644
--- a/cparser/Cprint.mli
+++ b/cparser/Cprint.mli
@@ -15,6 +15,7 @@
 
 val print_idents_in_full : bool ref
 val print_line_numbers : bool ref
+val print_debug_idents : bool ref
 
 val location : Format.formatter -> C.location -> unit
 val attributes : Format.formatter -> C.attributes -> unit
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 820f90f5..33c4822d 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 ?(enter:bool=true) env loc td =
   let loc = elab_loc loc in
-  top_declarations := { gdesc = td; gloc = loc } :: !top_declarations
+  let dec ={ gdesc = td; gloc = loc } in
+  if enter then  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 ~enter:false 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
@@ -2224,7 +2226,9 @@ and elab_block_body env ctx sl =
   | DEFINITION def :: sl1 ->
       let (dcl, env') = elab_definition true env def in
       let loc = elab_loc (get_definitionloc def) in
-      List.map (fun d -> {sdesc = Sdecl d; sloc = loc}) dcl
+      List.map (fun ((sto,id,ty,_) as d) ->
+        Debug.insert_local_declaration sto id ty loc;
+        {sdesc = Sdecl d; sloc = loc}) dcl
       @ elab_block_body env' ctx sl1
   | s :: sl1 ->
       let s' = elab_stmt env ctx s in
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/cparser/Unblock.ml b/cparser/Unblock.ml
index 91f50552..c6646b5c 100644
--- a/cparser/Unblock.ml
+++ b/cparser/Unblock.ml
@@ -177,16 +177,89 @@ and expand_init islocal env i =
   in
     expand i
 
+(* Insertion of debug annotation, for -g mode *)
+
+let debug_id = Env.fresh_ident "__builtin_debug"
+let debug_ty =
+  TFun(TVoid [], Some [Env.fresh_ident "kind", TInt(IInt, [])], true, [])
+
+let debug_annot kind args =
+  { sloc = no_loc;
+    sdesc = Sdo { 
+      etyp = TVoid [];
+      edesc = ECall({edesc = EVar debug_id; etyp = debug_ty},
+                    intconst kind IInt :: args)
+    }
+  }
+
+let string_const str =
+  let c = CStr str in { edesc = EConst c; etyp = type_of_constant c }
+
+let integer_const n =
+  intconst (Int64.of_int n) IInt
+
+(* Line number annotation:
+      __builtin_debug(1, "#line:filename:lineno") *)
+(* TODO: consider
+      __builtin_debug(1, "filename", lineno)
+   instead. *)
+
+let debug_lineno (filename, lineno) =
+  debug_annot 1L
+    [string_const (Printf.sprintf "#line:%s:%d" filename lineno)]
+
+(* Scope annotation:
+      __builtin_debug(6, "", scope1, scope2, ..., scopeN)
+*)
+
+let empty_string = string_const ""
+
+let curr_fun_id = ref 0
+
+let debug_var_decl ctx id =
+  Debug.add_lvar_scope !curr_fun_id id (List.hd ctx)
+
+let debug_scope ctx =
+  debug_annot 6L (empty_string :: List.rev_map integer_const ctx)
+
+(* Add line number debug annotation if the line number changes.
+   Add scope debug annotation regardless. *)
+
+
+let add_lineno ctx prev_loc this_loc s =
+  if !Clflags.option_g then
+    sseq no_loc (debug_scope ctx)
+      (if this_loc <> prev_loc && this_loc <> no_loc
+       then sseq no_loc (debug_lineno this_loc) s
+       else s)
+  else s
+
+(* Generate fresh scope identifiers, for blocks that contain at least
+   one declaration *)
+
+let block_contains_decl sl =
+  List.exists
+    (function {sdesc = Sdecl _} -> true | _ -> false)
+    sl
+
+let next_scope_id = ref 0
+
+let new_scope_id () =
+  incr next_scope_id; !next_scope_id
+
 (* Process a block-scoped variable declaration.
    The variable is entered in [local_variables].
    The initializer, if any, is converted into assignments and
    prepended to [k]. *)
 
-let process_decl loc env (sto, id, ty, optinit) k =
+let process_decl loc env ctx (sto, id, ty, optinit) k =
   let ty' = remove_const env ty in
   local_variables := (sto, id, ty', None) :: !local_variables;
+  debug_var_decl ctx id;
+  (* TODO: register the fact that id is declared in scope ctx *)
   match optinit with
-  | None -> k
+  | None ->
+      k
   | Some init ->
       let init' = expand_init true env init in
       let l = local_initializer env { edesc = EVar id; etyp = ty' } init' [] in
@@ -194,57 +267,90 @@ let process_decl loc env (sto, id, ty, optinit) k =
 
 (* Simplification of blocks within a statement *)
 
-let rec unblock_stmt env s =
+let rec unblock_stmt env ctx ploc s =
   match s.sdesc with
   | Sskip -> s
   | Sdo e ->
-      {s with sdesc = Sdo(expand_expr true env e)}
+      add_lineno ctx ploc s.sloc
+        {s with sdesc = Sdo(expand_expr true env e)}
   | Sseq(s1, s2) ->
-      {s with sdesc = Sseq(unblock_stmt env s1, unblock_stmt env s2)}
+      {s with sdesc = Sseq(unblock_stmt env ctx ploc s1,
+                           unblock_stmt env ctx s1.sloc s2)}
   | Sif(e, s1, s2) -> 
-      {s with sdesc = Sif(expand_expr true env e,
-                          unblock_stmt env s1, unblock_stmt env s2)}
+      add_lineno ctx ploc s.sloc
+        {s with sdesc = Sif(expand_expr true env e,
+                            unblock_stmt env ctx s.sloc s1,
+                            unblock_stmt env ctx s.sloc s2)}
   | Swhile(e, s1) -> 
-      {s with sdesc = Swhile(expand_expr true env e, unblock_stmt env s1)}
+      add_lineno ctx ploc s.sloc
+        {s with sdesc = Swhile(expand_expr true env e,
+                               unblock_stmt env ctx s.sloc s1)}
   | Sdowhile(s1, e) ->
-      {s with sdesc = Sdowhile(unblock_stmt env s1, expand_expr true env e)}
+      add_lineno ctx ploc s.sloc
+        {s with sdesc = Sdowhile(unblock_stmt env ctx s.sloc s1,
+                                 expand_expr true env e)}
   | Sfor(s1, e, s2, s3) ->
-      {s with sdesc = Sfor(unblock_stmt env s1,
-                           expand_expr true env e,
-                           unblock_stmt env s2,
-                           unblock_stmt env s3)}
+      add_lineno ctx ploc s.sloc
+        {s with sdesc = Sfor(unblock_stmt env ctx s.sloc s1,
+                             expand_expr true env e,
+                             unblock_stmt env ctx s.sloc s2,
+                             unblock_stmt env ctx s.sloc s3)}
   | Sbreak -> s
   | Scontinue -> s
   | Sswitch(e, s1) ->
-      {s with sdesc = Sswitch(expand_expr true env e, unblock_stmt env s1)}
+      add_lineno ctx ploc s.sloc
+        {s with sdesc = Sswitch(expand_expr true env e,
+                                unblock_stmt env ctx s.sloc s1)}
   | Slabeled(lbl, s1) -> 
-      {s with sdesc = Slabeled(lbl, unblock_stmt env s1)}
-  | Sgoto lbl -> s
-  | Sreturn None -> s
+      add_lineno ctx ploc s.sloc
+        {s with sdesc = Slabeled(lbl, unblock_stmt env ctx s.sloc s1)}
+  | Sgoto lbl ->
+      add_lineno ctx ploc s.sloc s
+  | Sreturn None ->
+      add_lineno ctx ploc s.sloc s
   | Sreturn (Some e) ->
-      {s with sdesc = Sreturn(Some (expand_expr true env e))}
-  | Sblock sl -> unblock_block env sl
-  | Sdecl d -> assert false
+      add_lineno ctx ploc s.sloc 
+        {s with sdesc = Sreturn(Some (expand_expr true env e))}
+  | Sblock sl ->
+      let ctx' =
+        if block_contains_decl sl
+        then
+          let id = new_scope_id () in
+          (match ctx with
+          | [] -> Debug.enter_function_scope !curr_fun_id id
+          | a::_ -> Debug.enter_scope !curr_fun_id a id);
+          id:: ctx
+        else ctx in
+      unblock_block env ctx' ploc sl
+  | Sdecl d ->
+      assert false
   | Sasm(attr, template, outputs, inputs, clob) ->
       let expand_asm_operand (lbl, cstr, e) =
         (lbl, cstr, expand_expr true env e) in
-      {s with sdesc = Sasm(attr, template,
-                           List.map expand_asm_operand outputs,
-                           List.map expand_asm_operand inputs, clob)}
+      add_lineno ctx ploc s.sloc 
+        {s with sdesc = Sasm(attr, template,
+                             List.map expand_asm_operand outputs,
+                             List.map expand_asm_operand inputs, clob)}
 
 
-and unblock_block env = function
+and unblock_block env ctx ploc = function
   | [] -> sskip
   | {sdesc = Sdecl d; sloc = loc} :: sl ->
-      process_decl loc env d (unblock_block env sl)
+      add_lineno ctx ploc loc
+        (process_decl loc env ctx d
+           (unblock_block env ctx loc sl))
   | s :: sl ->
-      sseq s.sloc (unblock_stmt env s) (unblock_block env sl)
+      sseq s.sloc (unblock_stmt env ctx ploc s)
+                  (unblock_block env ctx s.sloc sl)
 
 (* Simplification of blocks and compound literals within a function *)
 
 let unblock_fundef env f =
   local_variables := [];
-  let body = unblock_stmt env f.fd_body in
+  next_scope_id := 0;
+  curr_fun_id:= f.fd_name.stamp;
+  (* TODO: register the parameters as being declared in function scope *)
+  let body = unblock_stmt env [] no_loc f.fd_body in
   let decls = !local_variables in
   local_variables := [];
   { f with fd_locals = f.fd_locals @ decls; fd_body = body }
@@ -299,4 +405,5 @@ let rec unblock_glob env accu = function
 (* Entry point *)
 
 let program p =
+  {gloc = no_loc; gdesc = Gdecl(Storage_extern, debug_id, debug_ty, None)} ::
   unblock_glob (Builtins.environment()) [] p
diff --git a/debug/CtoDwarf.ml b/debug/CtoDwarf.ml
deleted file mode 100644
index c2085eb0..00000000
--- a/debug/CtoDwarf.ml
+++ /dev/null
@@ -1,543 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Bernhard Schommer, AbsInt Angewandte Informatik GmbH       *)
-(*                                                                     *)
-(*  AbsInt Angewandte Informatik GmbH. All rights reserved. This file  *)
-(*  is distributed under the terms of the INRIA Non-Commercial         *)
-(*  License Agreement.                                                 *)
-(*                                                                     *)
-(* *********************************************************************)
-
-open Builtins
-open C
-open Cprint
-open Cutil
-open C2C
-open DwarfTypes
-open DwarfUtil
-open Env
-open Set
-
-(* Functions to translate a C Ast into Dwarf 2 debugging information *)
-
-
-(* Hashtable from type name to entry id *)
-let type_table: (string, int) Hashtbl.t = Hashtbl.create 7
-
-(* Hashtable for typedefname to entry id *)
-let typedef_table: (string, int) Hashtbl.t = Hashtbl.create 7
-
-(* Hashtable from composite table to entry id *)
-let composite_types_table: (int, int) Hashtbl.t = Hashtbl.create 7
-
-(* Hashtable from id of a defined composite types to minimal type info *)
-let composite_declarations: (int, (struct_or_union * string * location)) Hashtbl.t = Hashtbl.create 7
-
-module IntSet = Set.Make(struct type t = int let compare = compare end)
-
-(* Set of all declared composite_types *)
-let composite_defined: IntSet.t ref = ref IntSet.empty
-
-(* Get the type id of a composite_type *)
-let get_composite_type (name: int): int =
-  try 
-    Hashtbl.find composite_types_table name
-  with Not_found ->
-    let id = next_id () in
-    Hashtbl.add composite_types_table name id;
-    id
-
-(* Translate a C.typ to a string needed for hashing *)
-let typ_to_string (ty: typ) =
-  let buf = Buffer.create 7 in
-  let chan = Format.formatter_of_buffer buf in
-  typ chan ty;
-  Format.pp_print_flush chan ();
-  Buffer.contents buf
-
-let rec mmap f env = function
-  | [] -> ([],env)
-  | hd :: tl ->
-      let (hd',env1) = f env hd in
-      let (tl', env2) = mmap f env1 tl in
-      (hd' :: tl', env2)
-
-
-(* Helper functions for the attributes *)
-
-let strip_attributes typ =
-  let strip = List.filter (fun a -> a = AConst || a = AVolatile) in 
-  match typ with
-  | TVoid at -> TVoid (strip at)
-  | TInt (k,at) ->  TInt (k,strip at)
-  | TFloat (k,at) -> TFloat(k,strip at)
-  | TPtr (t,at) -> TPtr(t,strip at)
-  | TArray (t,s,at) -> TArray(t,s,strip at)
-  | TFun (t,arg,v,at) -> TFun(t,arg,v,strip at)
-  | TNamed (n,at) -> TNamed(n,strip at)
-  | TStruct (n,at) -> TStruct(n,strip at)
-  | TUnion (n,at) -> TUnion(n,strip at)
-  | TEnum (n,at) -> TEnum(n,strip at)
-  
-
-let strip_last_attribute typ  = 
-  let rec hd_opt l = match l with
-    [] -> None,[]
-  | AConst::rest -> Some AConst,rest
-  | AVolatile::rest -> Some AVolatile,rest 
-  | _::rest -> hd_opt rest in
-  match typ with
-  | TVoid at -> let l,r = hd_opt at in
-    l,TVoid r
-  | TInt (k,at) -> let l,r = hd_opt at in
-    l,TInt (k,r)
-  | TFloat (k,at) -> let l,r = hd_opt at in
-    l,TFloat (k,r)
-  | TPtr (t,at) -> let l,r = hd_opt at in
-    l,TPtr(t,r)
-  | TArray (t,s,at) -> let l,r = hd_opt at in
-    l,TArray(t,s,r)
-  | TFun (t,arg,v,at) -> let l,r = hd_opt at in
-    l,TFun(t,arg,v,r)
-  | TNamed (n,at) -> let l,r = hd_opt at in
-    l,TNamed(n,r)
-  | TStruct (n,at) -> let l,r = hd_opt at in
-    l,TStruct(n,r)
-  | TUnion (n,at) -> let l,r = hd_opt at in
-    l,TUnion(n,r)
-  | TEnum (n,at) -> let l,r = hd_opt at in
-    l,TEnum(n,r)
-
-(*  Dwarf tag for the void type*)
-let rec void_dwarf_tag =
-  let void = {
-    base_type_byte_size = 0;
-    base_type_encoding = None;
-    base_type_name = "void";
-  } in
-  DW_TAG_base_type void
-
-(* Generate a dwarf tag for the given integer type *)
-and int_to_dwarf_tag k =  
-  let encoding =
-    (match k with
-    | IBool -> DW_ATE_boolean
-    | IChar ->
-        if !Machine.config.Machine.char_signed then 
-          DW_ATE_signed_char 
-        else 
-          DW_ATE_unsigned_char
-    | ILong | ILongLong | IShort | ISChar -> DW_ATE_signed_char
-    | _ -> DW_ATE_unsigned)in
-  let int = {
-    base_type_byte_size = sizeof_ikind k;
-    base_type_encoding = Some encoding;
-    base_type_name = typ_to_string (TInt (k,[]));} in
-  DW_TAG_base_type int
-
-(* Generate a dwarf tag for the given floating point type *)
-and float_to_dwarf_tag k = 
-  let byte_size = sizeof_fkind k in
-  let float = {
-    base_type_byte_size = byte_size;
-    base_type_encoding = Some DW_ATE_float;
-    base_type_name = typ_to_string (TFloat (k,[]));
-  } in
-  DW_TAG_base_type float
-
-(* Generate a dwarf tag for the given function type *)
-and fun_to_dwarf_tag rt args =
-  let ret,et = (match rt with
-  | TVoid _ -> None,[]
-  | _ -> let ret,et = type_to_dwarf rt in
-                Some ret,et) in
-  let prototyped,children,others =
-    (match args with 
-    | None -> 
-        let u = {
-          unspecified_parameter_file_loc = None;
-          unspecified_parameter_artificial = None;
-        } in
-        let u = new_entry (DW_TAG_unspecified_parameter u) in 
-        false,[u],[]
-    | Some [] -> true,[],[]
-    | Some l ->
-        let c,e = mmap (fun acc (_,t) ->
-          let t,e = type_to_dwarf t in
-          let fp =
-            {
-             formal_parameter_file_loc = None;
-             formal_parameter_artificial = None;
-             formal_parameter_location = None;
-             formal_parameter_name = None;
-             formal_parameter_segment = None;
-             formal_parameter_type = t;
-             formal_parameter_variable_parameter = None;
-           } in
-          let entry = new_entry (DW_TAG_formal_parameter fp) in
-          entry,(e@acc)) [] l in
-        true,c,e) in
-  let s = {
-    subroutine_type = ret;
-    subroutine_prototyped = prototyped;
-  } in
-  let s = new_entry (DW_TAG_subroutine_type s) in
-  let s = add_children s children in
-  s.id,((s::others)@et)
-
-(* Generate a dwarf tag for the given array type *)
-and array_to_dwarf_tag child size =
-  let append_opt a b =
-    match a with
-    | None -> b
-    | Some a -> a::b in
-  let size_to_subrange s =
-    match s with 
-    | None -> None
-    | Some i ->
-        let i = Int64.to_int (Int64.sub i Int64.one) in
-        let s =
-          {
-           subrange_type = None;
-           subrange_upper_bound = Some (BoundConst i);
-         } in
-        Some (new_entry (DW_TAG_subrange_type s)) in 
-  let rec aux t = 
-    (match t with
-    | TArray (child,size,_) ->
-        let sub = size_to_subrange size in
-        let t,c,e = aux child in
-        t,append_opt sub c,e
-    | _ -> let t,e = type_to_dwarf t in
-      t,[],e) in
-  let t,children,e = aux child in
-  let sub = size_to_subrange size in
-  let children = List.rev (append_opt sub children) in
-  let arr = {
-    array_type_file_loc = None;
-    array_type = t;
-  } in
-  let arr = new_entry (DW_TAG_array_type arr) in
-  let arr = add_children arr children in
-  arr.id,(arr::e)
-
-(* Translate a typ without attributes to a dwarf_tag *)
-and type_to_dwarf_entry typ typ_string=
-   let id,entries = 
-   (match typ with
-   | TVoid _ -> 
-       let e = new_entry void_dwarf_tag in
-       e.id,[e]
-   | TInt (k,_) ->
-       let e = new_entry (int_to_dwarf_tag k) in
-       e.id,[e]
-   | TFloat (k,_) ->
-       let e = new_entry (float_to_dwarf_tag k) in
-       e.id,[e]
-   | TPtr (t,_) ->
-       let t,e = type_to_dwarf t in
-       let pointer = {pointer_type = t;} in
-       let t = new_entry (DW_TAG_pointer_type pointer) in
-       t.id,t::e
-   | TFun (rt,args,_,_) -> fun_to_dwarf_tag rt args
-   | TStruct (i,_)
-   | TUnion (i,_)
-   | TEnum (i,_) ->
-       let t = get_composite_type i.stamp in
-       t,[]
-   | TNamed (i,at) ->
-       let t = Hashtbl.find typedef_table i.name in
-       t,[]
-   | TArray (child,size,_) -> array_to_dwarf_tag child size)         
-   in
-   Hashtbl.add type_table typ_string id;
-   id,entries
-
-(* Tranlate type with attributes to their corresponding dwarf represenation *)
-and attr_type_to_dwarf typ typ_string =
-  let l,t = strip_last_attribute typ in
-  match l with
-  | Some AConst -> let id,t = type_to_dwarf t in
-    let const_tag = DW_TAG_const_type ({const_type = id;}) in
-    let const_entry = new_entry const_tag in
-    let id = const_entry.id in
-    Hashtbl.add type_table typ_string id;
-    id,const_entry::t
-  | Some AVolatile -> let id,t = type_to_dwarf t in 
-    let volatile_tag = DW_TAG_volatile_type ({volatile_type = id;}) in
-    let volatile_entry = new_entry volatile_tag in
-    let id = volatile_entry.id in
-    Hashtbl.add type_table typ_string id;
-    id,volatile_entry::t
-  | Some (ARestrict|AAlignas _| Attr(_,_)) -> type_to_dwarf t (* This should not happen *)
-  | None -> type_to_dwarf_entry typ typ_string
-        
-(* Translate a given type to its dwarf representation *)
-and type_to_dwarf (typ: typ): int * dw_entry list =
-  match typ with
-   | TStruct (i,_)
-   | TUnion (i,_)
-   | TEnum (i,_) ->
-       let t = get_composite_type i.stamp in
-       t,[]
-   | _ -> 
-       let typ = strip_attributes typ in
-       let typ_string = typ_to_string typ in
-       try
-         Hashtbl.find type_table typ_string,[]
-       with Not_found ->
-         attr_type_to_dwarf typ typ_string
-
-(* Translate a typedef to its corresponding dwarf representation *)
-let typedef_to_dwarf gloc (name,t) =
-  let i,t = type_to_dwarf t in
-  let td = {
-    typedef_file_loc = gloc;
-    typedef_name = name;
-    typedef_type = i;
-  } in 
-  let td = new_entry (DW_TAG_typedef td) in
-  Hashtbl.add typedef_table name td.id;
-  td::t     
-
-(* Translate a global var to its corresponding dwarf representation *)
-let glob_var_to_dwarf (s,n,t,_) gloc =
-   let i,t = type_to_dwarf t in
-   let ext = (match s with
-   | Storage_static -> false
-   | _ -> true) in
-   let decl = {
-     variable_file_loc = (Some gloc);
-     variable_declaration = None;
-     variable_external = Some ext;
-     variable_location = None;
-     variable_name = n.name;
-     variable_segment = None;
-     variable_type = i;
-   } in
-   let decl = new_entry (DW_TAG_variable decl) in
-   t,decl
-
-(* Translate a function definition to its corresponding dwarf representation *)
-let fundef_to_dwarf f gloc =
-  let ret,e = (match f.fd_ret with
-  | TVoid _ -> None,[]
-  | _ -> let i,t = type_to_dwarf f.fd_ret in
-    Some i,t) in
-  let ext = (match f.fd_storage with
-  | Storage_static -> false
-  | _ -> true) in
-  let fdef = {
-    subprogram_file_loc = (Some gloc);
-    subprogram_external = Some ext;
-    subprogram_frame_base = None;
-    subprogram_name = f.fd_name.name;
-    subprogram_prototyped = true;
-    subprogram_type = ret;
-  } in
-  let fp,e =  mmap (fun acc (p,t) ->
-    let t,e = type_to_dwarf t in
-    let fp =
-      {
-       formal_parameter_file_loc = None;
-       formal_parameter_artificial = None;
-       formal_parameter_location = None;
-       formal_parameter_name = (Some p.name);
-       formal_parameter_segment = None;
-       formal_parameter_type = t;
-       formal_parameter_variable_parameter = None;
-     } in
-    let entry = new_entry (DW_TAG_formal_parameter fp) in
-    entry,(e@acc)) e f.fd_params in
-  let fdef = new_entry (DW_TAG_subprogram fdef) in
-  let fdef = add_children fdef fp in
-  e,fdef
-
-(* Translate a enum definition to its corresponding dwarf representation *)
-let enum_to_dwarf (n,at,e) gloc =
-  let enumerator_to_dwarf (i,c,_)=
-    let tag =      
-      {
-       enumerator_file_loc = None;
-       enumerator_value = Int64.to_int c;
-       enumerator_name = i.name;
-     } in
-    new_entry (DW_TAG_enumerator tag) in
-  let bs = sizeof_ikind enum_ikind in
-  let enum = {
-    enumeration_file_loc = Some gloc;
-    enumeration_byte_size = bs;
-    enumeration_declaration = None;
-    enumeration_name = if n.name <> "" then Some n.name else None;
-  } in
-  let id = get_composite_type n.stamp in
-  let child = List.map enumerator_to_dwarf e in
-  let enum = 
-    {
-     tag = DW_TAG_enumeration_type enum;
-     children = child;
-     id = id;
-   } in
-  [enum]
-  
-(* Translate a struct definition to its corresponding dwarf representation *)
-let struct_to_dwarf (n,at,m) env gloc =
-  let info = Env.find_struct env n in
-  let tag =DW_TAG_structure_type {
-    structure_file_loc = Some gloc;
-    structure_byte_size = info.ci_sizeof;
-    structure_declaration = None;
-    structure_name = if n.name <> "" then Some n.name else None;
-  } in
-  let id = get_composite_type n.stamp in
-  let rec pack acc bcc l m =
-    match m with
-    | [] -> acc,bcc,[]
-    | m::ms as ml ->
-        (match m.fld_bitfield with
-        | None -> acc,bcc,ml
-        | Some n ->
-            if n = 0 then
-              acc,bcc,ms (* bit width 0 means end of pack *)
-            else if l + n > 8 * !Machine.config.Machine.sizeof_int then
-              acc,bcc,ml (* doesn't fit in current word *)
-            else
-              let t,e = type_to_dwarf m.fld_typ in
-              let um = {
-                member_file_loc = None;
-                member_byte_size = Some !Machine.config.Machine.sizeof_int;
-                member_bit_offset = Some l;
-                member_bit_size = Some n;
-                member_data_member_location = None;
-                member_declaration = None;
-                member_name = if m.fld_name <> "" then Some m.fld_name else None;
-                member_type = t;
-              } in
-              pack ((new_entry (DW_TAG_member um))::acc) (e@bcc) (l + n) ms)
-  and translate acc bcc m =
-    match m with
-      [] -> acc,bcc
-    | m::ms as ml ->
-        (match m.fld_bitfield with
-        | None -> 
-            let t,e = type_to_dwarf m.fld_typ in
-            let um = {
-              member_file_loc = None;
-              member_byte_size = None;
-              member_bit_offset = None;
-              member_bit_size = None;
-              member_data_member_location = None;
-              member_declaration = None;
-              member_name = if m.fld_name <> "" then Some m.fld_name else None;
-              member_type = t;
-            } in
-            translate ((new_entry (DW_TAG_member um))::acc) (e@bcc) ms
-        | Some _ -> let acc,bcc,rest = pack acc bcc 0 ml in 
-          translate acc bcc rest)
-  in
-  let children,e = translate [] []  m in
-  let children,e = List.rev children,e in
-  let sou = {
-    tag = tag;
-    children = children;
-    id = id;} in
-  e@[sou]
-
-(* Translate a union definition to its corresponding dwarf representation *)
-let union_to_dwarf (n,at,m) env gloc = 
-  let info = Env.find_union env n in
-  let tag = DW_TAG_union_type {
-    union_file_loc = Some gloc;
-    union_byte_size = info.ci_sizeof;
-    union_declaration = None;
-    union_name = if n.name <> "" then Some n.name else None;
-  } in
-  let id = get_composite_type n.stamp in
-  let children,e = mmap 
-      (fun  acc f ->
-        let t,e = type_to_dwarf f.fld_typ in
-        let um = {
-          member_file_loc = None;
-          member_byte_size = None;
-          member_bit_offset = None;
-          member_bit_size = None;
-          member_data_member_location = None;
-          member_declaration = None;
-          member_name = if f.fld_name <> "" then Some f.fld_name else None;
-          member_type = t;
-        } in
-        new_entry (DW_TAG_member um),e@acc)[] m in
-  let sou = {
-    tag = tag;
-    children = children;
-    id = id;} in
-  e@[sou]
-
-(* Translate global declarations to there dwarf representation *)
-let globdecl_to_dwarf env (typs,decls) decl =
-  PrintAsmaux.add_file (fst decl.gloc);
-  match decl.gdesc with
-  | Gtypedef (n,t) -> let ret = typedef_to_dwarf (Some decl.gloc) (n.name,t)  in
-    typs@ret,decls
-  | Gdecl d -> let t,d = glob_var_to_dwarf d decl.gloc in
-    typs@t,d::decls
-  | Gfundef f ->   let t,d = fundef_to_dwarf f decl.gloc in
-    typs@t,d::decls
-  | Genumdef (n,at,e) ->
-      composite_defined:= IntSet.add n.stamp !composite_defined;
-      let ret = enum_to_dwarf (n,at,e) decl.gloc in
-      typs@ret,decls
-  | Gcompositedef (Struct,n,at,m) ->
-      composite_defined:= IntSet.add n.stamp !composite_defined;
-      let ret = struct_to_dwarf (n,at,m) env decl.gloc in
-      typs@ret,decls
-  | Gcompositedef (Union,n,at,m) ->
-      composite_defined:= IntSet.add n.stamp !composite_defined;
-      let ret = union_to_dwarf (n,at,m) env decl.gloc in
-      typs@ret,decls
-  | Gcompositedecl (sou,i,_) -> Hashtbl.add composite_declarations i.stamp (sou,i.name,decl.gloc);
-      typs,decls
-  | Gpragma _ -> typs,decls       
-
-let forward_declaration_to_dwarf sou name loc stamp =
-  let id = get_composite_type stamp in
-  let tag = match sou with
-  | Struct ->
-      DW_TAG_structure_type{
-      structure_file_loc = Some loc;
-      structure_byte_size = None;
-      structure_declaration = Some true;
-      structure_name = if name <> "" then Some name else None;
-    } 
-  | Union ->
-      DW_TAG_union_type {
-      union_file_loc = Some loc;
-      union_byte_size = None;
-      union_declaration = Some true;
-      union_name = if name <> "" then Some name else None;
-    } in
-  {tag = tag; children = []; id = id}
-  
-
-(* Compute the dwarf representations of global declarations. The second program argument is the 
-   program after the bitfield and packed struct transformation *)
-let program_to_dwarf prog prog1 name =
-  Hashtbl.reset type_table;
-  Hashtbl.reset composite_types_table;
-  Hashtbl.reset typedef_table;
-  let prog = cleanupGlobals (prog) in
-  let env = translEnv Env.empty prog1 in
-  reset_id ();
-  let typs = List.map (typedef_to_dwarf None) C2C.builtins.typedefs in
-  let typs = List.concat typs in
-  let typs,defs = List.fold_left (globdecl_to_dwarf env) (typs,[]) prog in
-  let typs = Hashtbl.fold (fun i (sou,name,loc) typs -> if not (IntSet.mem i !composite_defined) then
-    (forward_declaration_to_dwarf sou name loc i)::typs else typs) composite_declarations typs in
-  let defs =  typs @ defs in
-  let cp = {
-    compile_unit_name = name;
-  } in
-  let cp = new_entry (DW_TAG_compile_unit cp) in
-  add_children cp defs
diff --git a/debug/Debug.ml b/debug/Debug.ml
new file mode 100644
index 00000000..1d3b260e
--- /dev/null
+++ b/debug/Debug.ml
@@ -0,0 +1,108 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Bernhard Schommer, AbsInt Angewandte Informatik GmbH       *)
+(*                                                                     *)
+(*  AbsInt Angewandte Informatik GmbH. All rights reserved. This file  *)
+(*  is distributed under the terms of the INRIA Non-Commercial         *)
+(*  License Agreement.                                                 *)
+(*                                                                     *)
+(* *********************************************************************)
+
+open AST
+open BinNums
+open C
+open Camlcoq
+open Dwarfgen
+open DwarfTypes
+
+(* Interface for generating and printing debug information *)
+
+(* Record used for stroring references to the actual implementation functions *)
+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 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;
+     mutable generate_debug_info: (atom -> string) -> string -> debug_entries option;
+     mutable all_files_iter: (string -> unit) -> unit;
+     mutable insert_local_declaration:  storage -> ident -> typ -> location -> unit;
+     mutable atom_local_variable: ident -> atom -> unit;
+     mutable enter_scope: int -> int -> int -> unit;
+     mutable enter_function_scope: int -> int -> unit;
+     mutable add_lvar_scope: int -> ident -> int -> unit;
+     mutable open_scope: atom -> int -> positive -> unit;
+     mutable close_scope: atom -> int -> positive -> unit;
+     mutable start_live_range: atom -> positive -> int * int builtin_arg -> unit;
+     mutable end_live_range: atom -> positive -> unit;
+     mutable stack_variable: atom -> int * int builtin_arg -> unit;
+     mutable function_end: atom -> positive -> unit;
+     mutable add_label: atom -> positive -> int -> unit;
+     mutable atom_parameter: ident -> ident -> atom -> unit;
+     mutable add_compilation_section_start: string ->(int * int * int * string) -> unit;
+     mutable compute_file_enum: (string -> int) -> (string-> int) -> (unit -> unit) -> unit;
+     mutable exists_section: string -> bool;
+   }
+
+let implem =
+  {
+   init = (fun _ -> ());
+   atom_function = (fun _ _ -> ());
+   atom_global_variable = (fun _ _ -> ());
+   set_composite_size = (fun _ _ _ -> ());
+   set_member_offset = (fun _ _  _ -> ());
+   set_bitfield_offset = (fun _ _ _ _ _ -> ());
+   insert_global_declaration = (fun _ _ -> ());
+   add_fun_addr = (fun _ _ -> ());
+   generate_debug_info = (fun _  _ -> None);
+   all_files_iter = (fun _ -> ());
+   insert_local_declaration = (fun  _ _ _ _ -> ());
+   atom_local_variable = (fun _ _ -> ());
+   enter_scope = (fun _ _ _  -> ());
+   enter_function_scope = (fun _ _ -> ());
+   add_lvar_scope = (fun _ _ _ -> ());
+   open_scope = (fun _ _ _ -> ());
+   close_scope = (fun _ _ _ -> ());
+   start_live_range = (fun _ _ _ -> ());
+   end_live_range = (fun _ _ -> ());
+   stack_variable = (fun _ _ -> ());
+   function_end = (fun _ _ -> ());
+   add_label = (fun _ _ _ -> ());
+   atom_parameter = (fun _ _ _ -> ());
+   add_compilation_section_start = (fun _ _ -> ());
+   compute_file_enum = (fun _ _ _ -> ());
+   exists_section = (fun _ -> true);
+}
+
+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 = 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
+let generate_debug_info fun_s var_s = implem.generate_debug_info fun_s var_s
+let all_files_iter f = implem.all_files_iter f
+let insert_local_declaration sto id ty loc = implem.insert_local_declaration sto id ty loc
+let atom_local_variable id atom = implem.atom_local_variable id atom
+let enter_scope p_id id = implem.enter_scope p_id id
+let enter_function_scope fun_id sc_id = implem.enter_function_scope fun_id sc_id
+let add_lvar_scope fun_id var_id s_id = implem.add_lvar_scope fun_id var_id s_id
+let open_scope atom id lbl = implem.open_scope atom id lbl
+let close_scope atom id lbl = implem.close_scope atom id lbl
+let start_live_range atom lbl loc = implem.start_live_range atom lbl loc
+let end_live_range atom lbl = implem.end_live_range atom lbl
+let stack_variable atom loc = implem.stack_variable atom loc
+let function_end atom loc = implem.function_end atom loc
+let add_label atom p lbl = implem.add_label atom p lbl
+let atom_parameter fid pid atom = implem.atom_parameter fid pid atom
+let add_compilation_section_start sec addr = implem.add_compilation_section_start sec addr
+let exists_section sec = implem.exists_section sec
+let compute_file_enum end_l entry_l line_e = implem.compute_file_enum end_l entry_l line_e
diff --git a/debug/Debug.mli b/debug/Debug.mli
new file mode 100644
index 00000000..166a6759
--- /dev/null
+++ b/debug/Debug.mli
@@ -0,0 +1,78 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Bernhard Schommer, AbsInt Angewandte Informatik GmbH       *)
+(*                                                                     *)
+(*  AbsInt Angewandte Informatik GmbH. All rights reserved. This file  *)
+(*  is distributed under the terms of the INRIA Non-Commercial         *)
+(*  License Agreement.                                                 *)
+(*                                                                     *)
+(* *********************************************************************)
+
+open AST
+open C
+open Camlcoq
+open DwarfTypes
+open BinNums
+
+
+(* Record used for stroring references to the actual implementation functions *)
+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 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;
+     mutable generate_debug_info: (atom -> string) -> string -> debug_entries option;
+     mutable all_files_iter: (string -> unit) -> unit;
+     mutable insert_local_declaration:  storage -> ident -> typ -> location -> unit;
+     mutable atom_local_variable: ident -> atom -> unit;
+     mutable enter_scope: int -> int -> int -> unit;
+     mutable enter_function_scope: int -> int -> unit;
+     mutable add_lvar_scope: int -> ident -> int -> unit;
+     mutable open_scope: atom -> int -> positive -> unit;
+     mutable close_scope: atom -> int -> positive -> unit;
+     mutable start_live_range: atom -> positive -> int * int builtin_arg -> unit;
+     mutable end_live_range: atom -> positive -> unit;
+     mutable stack_variable: atom -> int * int builtin_arg -> unit;
+     mutable function_end: atom -> positive -> unit;
+     mutable add_label: atom -> positive -> int -> unit;
+     mutable atom_parameter: ident -> ident -> atom -> unit;
+     mutable add_compilation_section_start: string -> (int * int * int * string) -> unit;
+     mutable compute_file_enum: (string -> int) -> (string-> int) -> (unit -> unit) -> unit;
+     mutable exists_section: string -> bool;
+   }
+
+val implem: implem
+
+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 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
+val all_files_iter: (string -> unit) -> unit
+val insert_local_declaration: storage -> ident -> typ -> location -> unit
+val atom_local_variable: ident -> atom -> unit
+val enter_scope: int -> int -> int -> unit
+val enter_function_scope: int -> int -> unit
+val add_lvar_scope: int -> ident -> int -> unit
+val open_scope: atom -> int -> positive -> unit
+val close_scope: atom -> int -> positive -> unit
+val start_live_range: atom -> positive -> (int * int builtin_arg) -> unit
+val end_live_range: atom -> positive -> unit
+val stack_variable: atom -> int * int builtin_arg -> unit
+val function_end: atom -> positive -> unit
+val add_label: atom -> positive -> int -> unit
+val generate_debug_info: (atom -> string) -> string -> debug_entries option
+val atom_parameter: ident -> ident -> atom -> unit
+val add_compilation_section_start: string -> (int * int * int * string) -> unit
+val compute_file_enum: (string -> int) -> (string-> int) -> (unit -> unit) -> unit
+val exists_section: string -> bool
diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml
new file mode 100644
index 00000000..382845a4
--- /dev/null
+++ b/debug/DebugInformation.ml
@@ -0,0 +1,821 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Bernhard Schommer, AbsInt Angewandte Informatik GmbH       *)
+(*                                                                     *)
+(*  AbsInt Angewandte Informatik GmbH. All rights reserved. This file  *)
+(*  is distributed under the terms of the INRIA Non-Commercial         *)
+(*  License Agreement.                                                 *)
+(*                                                                     *)
+(* *********************************************************************)
+
+open AST
+open BinNums
+open C
+open Camlcoq
+open Cutil
+
+(* This implements an interface for the collection of debugging 
+   information. *)
+
+(* Simple id generator *)
+let id = ref 0
+
+let next_id () =
+  let nid = !id in
+  incr id; nid
+
+let reset_id () =
+  id := 0
+
+(* Auximilary functions *)
+let list_replace c f l =
+  List.map (fun a -> if c a then f a else a) l
+
+(* The name of the current compilation unit *)
+let file_name: string ref = ref ""
+
+(** All files used in the debug entries *)
+module StringSet = Set.Make(String)
+let all_files : StringSet.t ref = ref StringSet.empty
+let add_file file =
+  all_files := StringSet.add file !all_files
+
+(* Types for the information of type info *)
+type composite_field =
+    {
+     cfd_name:        string;
+     cfd_typ:         int;
+     cfd_bit_size:    int option;
+     cfd_bit_offset:  int option;
+     cfd_byte_offset: int option;
+     cfd_byte_size:   int option;
+     cfd_bitfield:    string option;
+   }
+
+type composite_type =
+    {
+     ct_name:        string;
+     ct_sou:         struct_or_union;
+     ct_file_loc:    location option;
+     ct_members:     composite_field list;
+     ct_sizeof:      int option;
+     ct_declaration: bool;
+   }
+
+type ptr_type = {
+    pts: int
+  }
+
+type const_type = {
+    cst_type: int
+  }
+
+type volatile_type = {
+    vol_type: int
+  }
+
+
+type array_type = {
+    arr_type: int;
+    arr_size: int64 option list;
+  }
+
+type typedef = {
+    typedef_file_loc: location option;
+    typedef_name:     string;
+    typ:              int option;
+  }
+
+type enumerator = {
+    enumerator_name:     string;
+    enumerator_const:    int64;
+  }
+
+type enum_type = {
+    enum_name:        string;
+    enum_byte_size:   int option;
+    enum_file_loc:    location option;
+    enum_enumerators: enumerator list; 
+  }
+
+type int_type = {
+    int_kind: ikind;
+  }
+
+type float_type = {
+    float_kind: fkind;
+  }
+
+type parameter_type = {
+    param_type: int;
+    param_name: string;
+  }
+
+type function_type = {
+    fun_return_type: int option;
+    fun_prototyped:  bool;
+    fun_params:      parameter_type list;
+  }
+
+type debug_types =
+  | IntegerType of int_type
+  | FloatType of float_type
+  | PointerType of ptr_type
+  | ArrayType of array_type
+  | CompositeType of composite_type
+  | EnumType of enum_type
+  | FunctionType of function_type
+  | Typedef of typedef
+  | ConstType of const_type
+  | VolatileType of volatile_type
+  | Void
+
+(* All types encountered *)
+let types: (int,debug_types) Hashtbl.t = Hashtbl.create 7
+
+(* Lookup table for types *)
+let lookup_types: (string, int) Hashtbl.t = Hashtbl.create 7
+
+(* Translate a C.typ to a string needed for hashing *)
+let typ_to_string (ty: typ) =
+  let buf = Buffer.create 7 in
+  let chan = Format.formatter_of_buffer buf in
+  Cprint.print_debug_idents := true;
+  Cprint.typ chan ty;
+  Cprint.print_debug_idents := false;
+  Format.pp_print_flush chan ();
+  Buffer.contents buf
+
+(* Helper functions for the attributes *)
+let strip_attributes typ =
+  let strip =  List.filter (fun a -> a = AConst || a = AVolatile) in 
+  match typ with
+  | TVoid at -> TVoid (strip at)
+  | TInt (k,at) ->  TInt (k,strip at)
+  | TFloat (k,at) -> TFloat(k,strip at)
+  | TPtr (t,at) -> TPtr(t,strip at)
+  | TArray (t,s,at) -> TArray(t,s,strip at)
+  | TFun (t,arg,v,at) -> TFun(t,arg,v,strip at)
+  | TNamed (n,at) -> TNamed(n,strip at)
+  | TStruct (n,at) -> TStruct(n,strip at)
+  | TUnion (n,at) -> TUnion(n,strip at)
+  | TEnum (n,at) -> TEnum(n,strip at)
+
+let strip_last_attribute typ  = 
+  let rec hd_opt l = match l with
+    [] -> None,[]
+  | AConst::rest -> Some AConst,rest
+  | AVolatile::rest -> Some AVolatile,rest 
+  | _::rest -> hd_opt rest in
+  match typ with
+  | TVoid at -> let l,r = hd_opt at in
+    l,TVoid r
+  | TInt (k,at) -> let l,r = hd_opt at in
+    l,TInt (k,r)
+  | TFloat (k,at) -> let l,r = hd_opt at in
+    l,TFloat (k,r)
+  | TPtr (t,at) -> let l,r = hd_opt at in
+    l,TPtr(t,r)
+  | TArray (t,s,at) -> let l,r = hd_opt at in
+    l,TArray(t,s,r)
+  | TFun (t,arg,v,at) -> let l,r = hd_opt at in
+    l,TFun(t,arg,v,r)
+  | TNamed (n,at) -> let l,r = hd_opt at in
+    l,TNamed(n,r)
+  | TStruct (n,at) -> let l,r = hd_opt at in
+    l,TStruct(n,r)
+  | TUnion (n,at) -> let l,r = hd_opt at in
+    l,TUnion(n,r)
+  | TEnum (n,at) -> let l,r = hd_opt at in
+    l,TEnum(n,r)
+
+(* Does the type already exist? *)
+let exist_type (ty: typ) =
+  (* We are only interrested in Const and Volatile *)
+  let ty = strip_attributes ty in
+  Hashtbl.mem lookup_types (typ_to_string ty)
+
+(* Find the type id to an type *)
+let find_type (ty: typ) =
+  (* We are only interrested in Const and Volatile *)
+  let ty = strip_attributes ty in
+  Hashtbl.find lookup_types (typ_to_string ty)
+
+(* Add type and information *)
+let insert_type (ty: typ) =
+  let insert d_ty ty =
+    let id = next_id () 
+    and name = typ_to_string ty in
+    Hashtbl.add types id d_ty;
+    Hashtbl.add lookup_types name id;
+    id in
+  (* We are only interrested in Const and Volatile *)
+  let ty = strip_attributes ty in
+  let rec typ_aux ty = 
+    try find_type ty with
+    | Not_found ->
+        let d_ty =
+          match ty with
+          | TVoid _ -> Void
+          | TInt (k,_) -> 
+              IntegerType ({int_kind = k })
+          | TFloat (k,_) ->
+              FloatType ({float_kind = k})
+          | TPtr (t,_) ->
+              let id = attr_aux t in
+              PointerType ({pts = id})
+          | TArray (t,s,_) ->
+              let rec size acc t = (match t with
+              | TArray (child,s,_) ->
+                  size (s::acc) child
+              | _ -> t,List.rev acc) in
+              let t,s = size [s] t in
+              let id = attr_aux t in
+              let arr = {
+                arr_type = id;
+                arr_size= s;
+              } in
+              ArrayType arr
+          | TFun (t,param,va,_) ->
+              let param,prot = (match param with 
+              | None -> [],false
+              | Some p -> List.map (fun (i,t) -> let t = attr_aux t in 
+                {
+                 param_type = t;
+                 param_name = i.name;               
+               }) p,true) in
+              let ret = (match t with 
+              | TVoid _ -> None
+              | _ -> Some (attr_aux t)) in
+              let ftype = {
+                fun_return_type = ret;
+                fun_prototyped = prot;
+                fun_params = param;
+              } in
+              FunctionType ftype
+          | TNamed (id,_) ->
+              let typ = try
+                let _,t =
+                  List.find (fun a -> fst a = id.name) CBuiltins.builtins.Builtins.typedefs in
+                Some (attr_aux t)
+              with Not_found -> None in
+              let t = {
+                typedef_file_loc = None;
+                typedef_name = id.name;
+                typ = typ;
+              } in
+              Typedef t
+          | TStruct (id,_) ->
+              let str =
+                {
+                 ct_name = id.name;
+                 ct_sou = Struct;
+                 ct_file_loc = None;
+                 ct_members = [];
+                 ct_declaration = false;
+                 ct_sizeof = None;
+               } in
+              CompositeType str
+          | TUnion (id,_) ->
+              let union =
+                {
+                 ct_name = id.name;
+                 ct_sou = Union;
+                 ct_file_loc = None;
+                 ct_members = [];
+                 ct_declaration = false;
+                 ct_sizeof = None;
+               } in
+              CompositeType union
+          | TEnum (id,_) ->
+              let enum = 
+                {
+                 enum_name = id.name;
+                 enum_byte_size = None;
+                 enum_file_loc = None;
+                 enum_enumerators = [];
+               } in
+              EnumType enum in
+        insert d_ty ty
+  and attr_aux ty = 
+    try
+      find_type ty
+    with
+      Not_found ->
+        match strip_last_attribute ty with
+        | Some AConst,t -> 
+            let id = attr_aux t in
+            let const = { cst_type = id} in
+            insert (ConstType const) ty
+        | Some AVolatile,t ->
+            let id = attr_aux t in
+            let volatile = {vol_type = id} in
+            insert (VolatileType volatile) ty
+        | Some (ARestrict|AAlignas _| Attr(_,_)),t ->
+            attr_aux t
+        | None,t -> typ_aux t
+  in
+  attr_aux ty
+
+(* Replace the composite information *)
+let replace_composite id f =
+  let str = Hashtbl.find types id in
+  match str with
+  | CompositeType comp -> let comp' = f comp in
+    if comp <> comp' then Hashtbl.replace types id (CompositeType comp')
+  | _ -> assert false (* This should never happen *)
+
+(* Replace the enum information *)
+let replace_enum id f =
+  let str = Hashtbl.find types id in
+  match str with
+  | EnumType comp -> let comp' = f comp in
+    if comp <> comp' then Hashtbl.replace types id (EnumType comp')
+  | _ -> assert false (* This should never happen *)
+
+(* Replace the typdef information *)
+let replace_typedef id f =
+  let typdef = Hashtbl.find types id in
+  match typdef with
+  | Typedef typ -> let typ' = f typ in
+    if typ <> typ' then Hashtbl.replace types id (Typedef typ')
+  | _ -> assert false (* This should never happen *)
+
+(* Types for global definitions *)
+
+(* Information for a global variable *)
+type global_variable_information = {
+    gvar_name:        string;
+    gvar_atom:        atom option;
+    gvar_file_loc:    location;
+    gvar_declaration: bool;
+    gvar_external:    bool;
+    gvar_type:        int;
+  }
+
+type parameter_information = 
+ {
+  parameter_name:     string;
+  parameter_ident:    int;
+  parameter_atom:     atom option;
+  parameter_type:     int;
+}
+
+type function_information = {
+    fun_name:        string;
+    fun_atom:        atom option;
+    fun_file_loc:    location;
+    fun_external:    bool;
+    fun_return_type: int option; (* Again the special case of void functions *)
+    fun_vararg:      bool;
+    fun_parameter:   parameter_information list;
+    fun_low_pc:      int option;
+    fun_high_pc:     int option;
+    fun_scope:       int option;
+  }
+
+type definition_type =
+  | GlobalVariable of global_variable_information
+  | Function of function_information
+
+
+(* All global definitions encountered *)
+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
+
+let find_gvar_stamp id =
+  let id = (Hashtbl.find stamp_to_definition id) in
+  let var = Hashtbl.find definitions id in
+  match var with
+  | GlobalVariable var -> id,var
+  |  _ -> assert false
+
+let find_fun_stamp id =
+  let id = (Hashtbl.find stamp_to_definition id) in
+  let f = Hashtbl.find definitions id in
+  match f with
+  | 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
+  Hashtbl.replace definitions id var
+
+let replace_fun id f =
+  let f = Function f in
+  Hashtbl.replace definitions id f
+
+
+(* Information for local variables *)
+type local_variable_information = {
+    lvar_name:    string;
+    lvar_atom:    atom option;
+    lvar_file_loc:location;
+    lvar_type:    int;
+    lvar_static:  bool;  (* Static variable are mapped to symbols *)
+  }
+
+type scope_information = 
+  {
+   scope_variables: int list; (* Variable and Scope ids *)
+ }
+
+type local_information =
+  | LocalVariable of local_variable_information
+  | Scope of scope_information
+
+(* All local variables *)
+let local_variables: (int, local_information) Hashtbl.t = Hashtbl.create 7
+
+(* Mapping from stampt to the debug id of the local variable *)
+let stamp_to_local: (int,int) Hashtbl.t = Hashtbl.create 7
+
+(* Mapping form atom to the debug id of the local variable *)
+let atom_to_local: (atom, int) Hashtbl.t = Hashtbl.create 7
+
+(* Map from scope id + function id to debug id *)
+let scope_to_local: (int * int,int) Hashtbl.t = Hashtbl.create 7
+
+(* Map from scope id + function atom to debug id *)
+let atom_to_scope: (atom * int, int) Hashtbl.t = Hashtbl.create 7
+
+let find_lvar_stamp id =
+  let id = (Hashtbl.find stamp_to_local id) in
+  let v = Hashtbl.find local_variables id in
+  match v with
+  | LocalVariable v -> id,v
+  | _ -> assert false
+
+let replace_lvar id var =
+  let var = LocalVariable var in
+  Hashtbl.replace local_variables id var
+
+let find_scope_id fid id =
+  let id = Hashtbl.find scope_to_local (fid,id) in
+  let v = Hashtbl.find local_variables id in
+  match v with
+  | Scope v -> id,v
+  | _ -> assert false
+
+let replace_scope id var =
+  let var = Scope var in
+  Hashtbl.replace local_variables id var
+
+let gen_comp_typ sou id at = 
+  if sou = Struct then
+    TStruct (id,at)
+  else
+    TUnion (id,at)
+
+let insert_global_declaration env dec=
+  add_file (fst dec.gloc);
+  let insert d_dec stamp =
+    let id = next_id () in
+    Hashtbl.add definitions id d_dec;
+    Hashtbl.add stamp_to_definition stamp id
+  in
+  match dec.gdesc with
+  | Gdecl (sto,id,ty,init) ->
+      if  not (is_function_type env ty) then begin
+        if not (Hashtbl.mem stamp_to_definition id.stamp)  then begin
+          let at_decl,ext = (match sto with
+          | Storage_extern -> init = None,true
+          | Storage_static -> false,false
+          | _ -> false,true) in
+          let ty = insert_type ty in
+          let decl = {
+            gvar_name = id.name;
+            gvar_atom = None;
+            gvar_file_loc = dec.gloc;
+            gvar_declaration = at_decl;
+            gvar_external = ext;
+            gvar_type = ty;
+          } in
+          insert (GlobalVariable decl) id.stamp
+        end else if init <> None || sto <> Storage_extern then begin (* It is a definition *)
+          let id,var = find_gvar_stamp id.stamp in
+          replace_var id ({var with gvar_declaration = false;})
+        end
+      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
+      let ext =  (match f.fd_storage with
+      | Storage_static -> false
+      | _ -> true) in
+      let params = List.map (fun (p,ty) ->
+        let ty = insert_type ty in
+        {
+         parameter_name = p.name;
+         parameter_ident = p.stamp;
+         parameter_atom = None;
+         parameter_type = ty;
+       }) f.fd_params in
+      let fd =
+      { 
+        fun_name = f.fd_name.name;
+        fun_atom = None;
+        fun_file_loc = dec.gloc;
+        fun_external = ext;
+        fun_return_type = ret;
+        fun_vararg = f.fd_vararg;
+        fun_parameter = params;
+        fun_low_pc = None;
+        fun_high_pc = None;
+        fun_scope = None;
+      } in
+      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
+      replace_composite id (fun comp -> if comp.ct_file_loc = None then
+        {comp with ct_file_loc = Some (dec.gloc);}
+      else comp)
+  | Gcompositedef (sou,id,at,fi) -> 
+      ignore (insert_type (gen_comp_typ sou id at));
+      let id = find_type (gen_comp_typ sou id []) in
+      let fi = List.filter (fun f -> f.fld_name <> "") fi in (* Fields without names need no info *)
+      let fields = List.map (fun f ->
+        {
+         cfd_name = f.fld_name;
+         cfd_typ = insert_type f.fld_typ;
+         cfd_bit_size = f.fld_bitfield;
+         cfd_bit_offset = None;
+         cfd_byte_offset = None;
+         cfd_byte_size = None;
+         cfd_bitfield = None;
+       }) fi in
+      replace_composite id (fun comp ->
+        let loc = if comp.ct_file_loc = None then Some dec.gloc else comp.ct_file_loc in
+        {comp with ct_file_loc = loc; ct_members = fields; ct_declaration = true;})
+  | Gtypedef (id,t) -> 
+      let id = insert_type (TNamed (id,[])) in
+      let tid = insert_type t in
+      replace_typedef id (fun typ -> {typ with typedef_file_loc = Some dec.gloc; typ = Some tid;});
+  | Genumdef (n,at,e) -> 
+      ignore(insert_type (TEnum (n,at)));
+      let id = find_type (TEnum (n,[])) in
+      let enumerator = List.map (fun (i,c,_) ->
+        {    
+             enumerator_name = i.name;
+             enumerator_const = c;
+       }) e in
+      replace_enum id (fun en ->
+        {en with enum_file_loc = Some dec.gloc; enum_enumerators = enumerator;})
+  | Gpragma _ -> ()
+
+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_replace name (fun a -> {a with cfd_byte_offset = Some offset;}) 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 = 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_replace name (fun a -> 
+      {a with cfd_bit_offset = Some offset; cfd_bitfield = Some underlying; cfd_byte_size = Some size})
+        comp.ct_members in
+    {comp with ct_members = members;})
+
+let atom_global_variable id atom = 
+  try
+    let id,var = find_gvar_stamp id.stamp in
+    replace_var id ({var with gvar_atom = Some atom;});
+    Hashtbl.add atom_to_definition atom id 
+  with Not_found -> ()
+    
+let atom_function id atom =
+  try
+    let id',f = find_fun_stamp id.stamp in
+    replace_fun id' ({f with fun_atom = Some atom;});
+    Hashtbl.add atom_to_definition atom id';
+    Hashtbl.iter (fun (fid,sid) tid -> if fid = id.stamp then 
+      Hashtbl.add atom_to_scope (atom,sid) tid) scope_to_local
+  with Not_found -> ()
+
+let atom_parameter fid id atom =
+  try
+    let fid',f = find_fun_stamp fid.stamp in
+    let name p = p.parameter_ident = id.stamp in
+    let params = list_replace name (fun p -> {p with parameter_atom = Some atom;}) f.fun_parameter in
+    replace_fun fid' ({f with fun_parameter = params;})
+  with Not_found -> ()
+    
+let add_fun_addr atom (high,low) =
+  try
+    let id,f = find_fun_atom atom in
+    replace_fun id ({f with fun_high_pc = Some high; fun_low_pc = Some low;})
+  with Not_found -> ()
+
+let atom_local_variable id atom =
+  try
+    let id,var = find_lvar_stamp id.stamp in
+    replace_lvar id ({var with lvar_atom = Some atom;});
+    Hashtbl.add atom_to_local atom id
+  with Not_found -> ()
+
+let add_lvar_scope f_id var_id s_id =
+  try
+    let s_id',scope = find_scope_id f_id s_id in
+    let var_id,_ = find_lvar_stamp var_id.stamp in 
+    replace_scope s_id' ({scope_variables = var_id::scope.scope_variables;})
+  with Not_found -> ()
+
+let insert_local_declaration sto id ty loc =
+  let ty = insert_type ty in
+  let var = {
+    lvar_name = id.name;
+    lvar_atom = None;
+    lvar_file_loc = loc;
+    lvar_type = ty;
+    lvar_static = sto = Storage_static;
+  } in
+  let id' = next_id () in
+  Hashtbl.add local_variables id' (LocalVariable var);
+  Hashtbl.add stamp_to_local id.stamp id'
+
+let new_scope f_id sc_id =
+  let scope = {scope_variables = [];} in
+  let id = next_id () in
+  Hashtbl.add local_variables id (Scope scope);
+  Hashtbl.add scope_to_local (f_id,sc_id) id;
+  id
+
+let enter_function_scope fun_id sc_id =
+  try
+    let id = new_scope fun_id sc_id in
+    let fun_id,f = find_fun_stamp fun_id in
+    replace_fun fun_id ({f with fun_scope = Some id})
+  with Not_found -> ()
+
+let enter_scope f_id p_id id =
+  try
+    let id' = new_scope f_id id in
+    let p_id',scope = find_scope_id f_id p_id in
+    replace_scope p_id' ({scope_variables = id'::scope.scope_variables;})
+  with Not_found  -> ()
+
+
+type scope_range =
+    {
+     start_addr: positive option;
+     end_addr: positive option;
+   }
+
+type var_range =
+    {
+     range_start: positive option;
+     range_end:   positive option;
+     var_loc:     int * int builtin_arg;
+   }
+
+type var_location =
+  | RangeLoc of var_range list
+  | FunctionLoc of  int * int builtin_arg (* Stack allocated variables *)
+
+let var_locations: (atom,var_location) Hashtbl.t = Hashtbl.create 7
+
+let scope_ranges: (int,scope_range list) Hashtbl.t = Hashtbl.create 7
+
+let label_translation: (atom * positive, int) Hashtbl.t = Hashtbl.create 7
+
+let add_label atom p i =
+  Hashtbl.add label_translation (atom,p) i
+
+(* Auxiliary data structures and functions *)
+module IntSet = Set.Make(struct
+  type t = int
+  let compare (x:int) (y:int) = compare x y
+end)
+
+let open_scopes: IntSet.t ref = ref IntSet.empty
+let open_vars: atom list ref = ref []
+
+let open_scope atom s_id lbl =
+  try
+    let s_id = Hashtbl.find atom_to_scope (atom,s_id) in
+    let old_r = try Hashtbl.find scope_ranges s_id with Not_found -> [] in
+    let n_scop = { start_addr = Some lbl; end_addr = None;} in
+    open_scopes := IntSet.add s_id !open_scopes;
+    Hashtbl.replace scope_ranges s_id (n_scop::old_r)
+  with Not_found -> ()
+
+let close_scope atom s_id lbl =
+  try
+    let s_id = Hashtbl.find atom_to_scope (atom,s_id) in
+    let old_r = try Hashtbl.find scope_ranges s_id with Not_found -> [] in
+    let last_r,rest = 
+      begin
+        match old_r with
+        | a::rest -> a,rest
+        | _ -> assert false (* We must have an opening scope *)
+      end in
+    let new_r = ({last_r with end_addr = Some lbl;})::rest in
+    open_scopes := IntSet.remove s_id !open_scopes;
+    Hashtbl.replace scope_ranges s_id new_r
+  with Not_found -> ()
+
+let start_live_range atom lbl loc =
+  let old_r = begin try Hashtbl.find var_locations atom with Not_found -> (RangeLoc []) end in
+  match old_r with
+  | RangeLoc old_r ->
+      let n_r = { range_start = Some lbl; range_end = None; var_loc = loc } in
+      open_vars := atom::!open_vars;
+      Hashtbl.replace var_locations atom (RangeLoc (n_r::old_r))
+  | _ -> () (* Parameter that is passed as variable *)
+
+let end_live_range atom lbl =
+  try
+    let old_r = Hashtbl.find var_locations atom in
+    match old_r with
+    | RangeLoc (n_r::old_r) ->
+        if n_r.range_end = None then (* We can skip non open locations *)
+          let n_r = {n_r with  range_end = Some lbl} in
+          Hashtbl.replace var_locations atom (RangeLoc (n_r::old_r))
+    | _ -> ()
+  with Not_found -> ()
+
+let stack_variable atom (sp,loc) =
+  Hashtbl.add var_locations atom (FunctionLoc (sp,loc))
+
+let function_end atom loc =
+  IntSet.iter (fun id -> close_scope atom id loc) !open_scopes;
+  open_scopes := IntSet.empty;
+  List.iter (fun atom -> end_live_range atom loc) !open_vars;
+  open_vars:= []
+
+let compilation_section_start: (string,int * int * int * string) Hashtbl.t = Hashtbl.create 7
+let compilation_section_end: (string,int) Hashtbl.t = Hashtbl.create 7
+
+let add_compilation_section_start sec addr =
+  Hashtbl.add compilation_section_start sec addr
+
+let add_compilation_section_end sec addr =
+  Hashtbl.add compilation_section_end sec addr
+
+let exists_section sec =
+  Hashtbl.mem compilation_section_start sec
+
+let filenum: (string * string,int) Hashtbl.t = Hashtbl.create 7
+
+let compute_file_enum end_label entry_label line_end =
+  Hashtbl.iter (fun sec (_,_,_,secname) ->
+    Hashtbl.add compilation_section_end sec (end_label secname);
+    StringSet.iter (fun file ->
+      let lbl = entry_label file in
+      Hashtbl.add filenum (sec,file) lbl) !all_files;
+    line_end ()) compilation_section_start
+
+let init name =
+  id := 0;
+  file_name := name;
+  Hashtbl.reset types;
+  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;
+  Hashtbl.reset atom_to_local;
+  Hashtbl.reset scope_to_local;
+  Hashtbl.reset compilation_section_start;
+  Hashtbl.reset compilation_section_end;
+  Hashtbl.reset filenum;
+  all_files := StringSet.empty
diff --git a/debug/DebugInit.ml b/debug/DebugInit.ml
new file mode 100644
index 00000000..6a50b020
--- /dev/null
+++ b/debug/DebugInit.ml
@@ -0,0 +1,80 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Bernhard Schommer, AbsInt Angewandte Informatik GmbH       *)
+(*                                                                     *)
+(*  AbsInt Angewandte Informatik GmbH. All rights reserved. This file  *)
+(*  is distributed under the terms of the INRIA Non-Commercial         *)
+(*  License Agreement.                                                 *)
+(*                                                                     *)
+(* *********************************************************************)
+
+open AST
+open BinNums
+open C
+open Camlcoq
+open Dwarfgen
+open DwarfTypes
+open Debug
+
+let init_debug () =
+  implem.init <- DebugInformation.init;
+  implem.atom_function <- DebugInformation.atom_function;
+  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.set_bitfield_offset <- DebugInformation.set_bitfield_offset;
+  implem.insert_global_declaration <- DebugInformation.insert_global_declaration;
+  implem.add_fun_addr <- DebugInformation.add_fun_addr;
+  implem.generate_debug_info <- (fun a b -> Some (Dwarfgen.gen_debug_info a b));
+  implem.all_files_iter <- (fun f -> DebugInformation.StringSet.iter f !DebugInformation.all_files);
+  implem.insert_local_declaration <- DebugInformation.insert_local_declaration;
+  implem.atom_local_variable <- DebugInformation.atom_local_variable;
+  implem.enter_scope <- DebugInformation.enter_scope;
+  implem.enter_function_scope <- DebugInformation.enter_function_scope;
+  implem.add_lvar_scope <- DebugInformation.add_lvar_scope;
+  implem.open_scope <- DebugInformation.open_scope;
+  implem.close_scope <- DebugInformation.close_scope;
+  implem.start_live_range <- DebugInformation.start_live_range;
+  implem.end_live_range <- DebugInformation.end_live_range;
+  implem.stack_variable <- DebugInformation.stack_variable;
+  implem.function_end <- DebugInformation.function_end;
+  implem.add_label <- DebugInformation.add_label;
+  implem.atom_parameter <- DebugInformation.atom_parameter;
+  implem.add_compilation_section_start <- DebugInformation.add_compilation_section_start;
+  implem.compute_file_enum <- DebugInformation.compute_file_enum;
+  implem.exists_section <- DebugInformation.exists_section
+
+let init_none () =
+  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 _ _ -> ());
+  implem.generate_debug_info <- (fun _ _ -> None);
+  implem.all_files_iter <- (fun _ -> ());
+  implem.insert_local_declaration <- (fun  _ _ _ _ -> ());
+  implem.atom_local_variable <- (fun _ _ -> ());
+  implem.enter_scope <- (fun _ _  _ -> ());
+  implem.enter_function_scope <- (fun _ _ -> ());
+  implem.add_lvar_scope <- (fun _ _ _ -> ());
+  implem.open_scope <- (fun _ _ _ -> ());
+  implem.close_scope <- (fun _ _ _ -> ());
+  implem.start_live_range <- (fun _ _ _ -> ());
+  implem.end_live_range <- (fun _ _ -> ());
+  implem.stack_variable <- (fun _ _ -> ());
+  implem.function_end <- (fun _ _ -> ());
+  implem.add_label <- (fun _ _ _ -> ());
+  implem.atom_parameter <- (fun _ _ _ -> ());
+  implem.add_compilation_section_start <- (fun _ _ -> ());
+  implem.exists_section <- (fun _ -> true)
+
+let init () =
+  if !Clflags.option_g && Configuration.advanced_debug then
+    init_debug ()
+  else
+    init_none ()
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml
index 15843eb9..a95c71a1 100644
--- a/debug/DwarfPrinter.ml
+++ b/debug/DwarfPrinter.ml
@@ -19,14 +19,13 @@ open PrintAsmaux
 open Sections
 
 (* The printer is parameterized over target specific functions and a set of dwarf type constants *)
-module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
+module DwarfPrinter(Target: DWARF_TARGET):
     sig
-      val print_debug: out_channel -> dw_entry -> unit
+      val print_debug: out_channel -> debug_entries -> unit
     end =
   struct
 
     open Target
-    open DwarfAbbrevs
 
     (* Byte value to string *)
     let string_of_byte value =
@@ -36,6 +35,10 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
     let print_label oc lbl =
       fprintf oc "%a:\n" label lbl
 
+    (* Print a positive label *)
+    let print_plabel oc lbl =
+      print_label oc (transl_label lbl)
+
     (* Helper functions for abbreviation printing *)
     let add_byte buf value =
       Buffer.add_string buf (string_of_byte value)
@@ -64,18 +67,15 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
 
     let add_low_pc = add_abbr_entry (0x11,low_pc_type_abbr)
 
-    let add_fun_pc sp buf =
-      match get_fun_addr sp.subprogram_name with
-      | None ->()
-      | Some (a,b) -> add_high_pc buf; add_low_pc buf
-
     let add_declaration = add_abbr_entry (0x3c,declaration_type_abbr)
 
     let add_location loc buf =
       match loc with
       | None -> ()
-      | Some (LocConst _) -> add_abbr_entry (0x2,location_const_type_abbr) buf
-      | Some (LocBlock _) -> add_abbr_entry (0x2,location_block_type_abbr) buf
+      | Some (LocRef _) -> add_abbr_entry (0x2,location_ref_type_abbr) buf
+      | Some (LocList _ )
+      | Some (LocSymbol _)
+      | Some (LocSimple _) -> add_abbr_entry (0x2,location_block_type_abbr) buf
 
     (* Dwarf entity to string function *)
     let abbrev_string_of_entity entity has_sibling =
@@ -105,8 +105,8 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
       | DW_TAG_compile_unit e ->
           prologue 0x11;
           add_abbr_entry (0x1b,comp_dir_type_abbr) buf;
-          add_high_pc buf;
           add_low_pc buf;
+          add_high_pc buf;
           add_abbr_entry (0x13,language_type_abbr) buf;
           add_name buf;
           add_abbr_entry (0x25,producer_type_abbr) buf;
@@ -129,32 +129,31 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
           prologue 0x5;
           add_attr_some e.formal_parameter_file_loc add_file_loc;
           add_attr_some e.formal_parameter_artificial (add_abbr_entry (0x34,artificial_type_abbr));
-          add_location  e.formal_parameter_location buf;
           add_attr_some e.formal_parameter_name add_name;
-          add_location e.formal_parameter_segment buf;
           add_type buf;
-          add_attr_some e.formal_parameter_variable_parameter (add_abbr_entry (0x4b,variable_parameter_type_abbr))
+          add_attr_some e.formal_parameter_variable_parameter (add_abbr_entry (0x4b,variable_parameter_type_abbr));
+          add_location  e.formal_parameter_location buf
       | DW_TAG_label _ ->
           prologue 0xa;
           add_low_pc buf;
           add_name buf;
-      | DW_TAG_lexical_block _ ->
+      | DW_TAG_lexical_block a ->
           prologue 0xb;
-          add_high_pc buf;
-          add_low_pc buf
+          add_attr_some a.lexical_block_high_pc add_high_pc;
+          add_attr_some a.lexical_block_low_pc add_low_pc
       | DW_TAG_member e ->
           prologue 0xd;
           add_attr_some e.member_file_loc add_file_loc;
-          add_attr_some e.member_byte_size add_member_size;
-          add_attr_some e.member_bit_offset (add_abbr_entry (0xd,bit_offset_type_abbr));
-          add_attr_some e.member_bit_size (add_abbr_entry (0xc,bit_size_type_abbr));
+          add_attr_some e.member_byte_size add_byte_size;
+          add_attr_some e.member_bit_offset (add_abbr_entry (0xc,bit_offset_type_abbr));
+          add_attr_some e.member_bit_size (add_abbr_entry (0xd,bit_size_type_abbr));
+          add_attr_some e.member_declaration add_declaration;
+          add_attr_some e.member_name add_name;
+          add_type buf;
           (match e.member_data_member_location with
           | None -> ()
           | Some (DataLocBlock __) -> add_abbr_entry (0x38,data_location_block_type_abbr) buf
-          | Some (DataLocRef _) -> add_abbr_entry (0x38,data_location_ref_type_abbr) buf);
-          add_attr_some e.member_declaration add_declaration;
-          add_attr_some e.member_name add_name;
-          add_type buf
+          | Some (DataLocRef _) -> add_abbr_entry (0x38,data_location_ref_type_abbr) buf)
       | DW_TAG_pointer_type _ ->
           prologue 0xf;
           add_type buf
@@ -166,9 +165,10 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
           add_attr_some e.structure_name add_name
       | DW_TAG_subprogram e ->
           prologue 0x2e;
-          add_attr_some e.subprogram_file_loc add_file_loc;
+          add_file_loc buf;
           add_attr_some e.subprogram_external (add_abbr_entry (0x3f,external_type_abbr));
-          add_fun_pc e buf;
+          add_attr_some e.subprogram_high_pc add_high_pc;
+          add_attr_some e.subprogram_low_pc add_low_pc;
           add_name buf;
           add_abbr_entry (0x27,prototyped_type_abbr) buf;
           add_attr_some e.subprogram_type add_type;
@@ -200,12 +200,11 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
           add_attr_some e.unspecified_parameter_artificial (add_abbr_entry (0x34,artificial_type_abbr))
       | DW_TAG_variable e ->
           prologue 0x34;
-          add_attr_some e.variable_file_loc add_file_loc;
+          add_file_loc buf;
           add_attr_some e.variable_declaration add_declaration;
           add_attr_some e.variable_external (add_abbr_entry (0x3f,external_type_abbr));
           add_location  e.variable_location buf;
           add_name buf;
-          add_location e.variable_segment buf;
           add_type buf
       | DW_TAG_volatile_type _ ->
           prologue 0x35;
@@ -246,7 +245,7 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
     let print_abbrev oc =
       let abbrevs = Hashtbl.fold (fun s i acc -> (s,i)::acc) abbrev_mapping [] in
       let abbrevs = List.sort (fun (_,a) (_,b) -> Pervasives.compare a b) abbrevs in
-      fprintf oc "	.section	%s\n" (name_of_section Section_debug_abbrev);
+      section oc Section_debug_abbrev;
       let lbl = new_label () in
       abbrev_start_addr := lbl;
       print_label oc lbl;
@@ -276,9 +275,6 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
       | None -> ()
       | Some o -> f oc o
 
-    let print_file_loc oc f =
-      print_opt_value oc f print_file_loc
-
     let print_flag oc b =
       output_string oc (string_of_byte b)
 
@@ -294,16 +290,74 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
     let print_byte oc b =
       fprintf oc "	.byte		0x%X\n" b
 
-    let print_loc oc loc =
-      ()
-
-    let print_data_location oc dl =
-      ()
+    let print_2byte oc b =
+      fprintf oc "	.2byte		0x%X\n" b
 
     let print_ref oc r =
       let ref = entry_to_label r in
       fprintf oc "	.4byte		%a\n" label ref
 
+    let print_file_loc oc = function
+      | Some (file,col) ->
+          fprintf oc "	.4byte		%a\n" label file;
+          print_uleb128 oc col
+      | None -> ()
+
+    let print_loc_expr oc = function
+      | DW_OP_bregx (a,b) ->
+          print_byte oc dw_op_bregx;
+          print_uleb128 oc a;
+          fprintf oc "	.sleb128	%ld\n" b
+      | DW_OP_plus_uconst i ->
+          print_byte oc dw_op_plus_uconst;
+          print_uleb128 oc i
+      | DW_OP_piece i ->
+          print_byte oc dw_op_piece;
+          print_uleb128 oc i
+      | DW_OP_reg i ->
+          if i < 32 then
+            print_byte oc (dw_op_reg0 + i)
+          else begin
+            print_byte oc dw_op_regx;
+            print_uleb128 oc i
+          end
+
+    let print_loc oc loc =
+      match loc with
+      | LocSymbol s ->
+          print_sleb128 oc 5;
+          print_byte oc dw_op_addr;
+          fprintf oc "	.4byte		%a\n" symbol s
+      | LocSimple e ->
+          print_sleb128 oc (size_of_loc_expr e);
+          print_loc_expr oc e
+      | LocList e ->
+          let size = List.fold_left (fun acc a -> acc + size_of_loc_expr a) 0 e in
+          print_sleb128 oc size;
+          List.iter (print_loc_expr oc) e
+      | LocRef f ->  print_ref oc f
+
+    let print_list_loc oc = function
+      | LocSymbol s ->
+          print_2byte oc 5;
+          print_byte oc dw_op_addr;
+          fprintf oc "	.4byte		%a\n" symbol s
+      | LocSimple e ->
+          print_2byte oc (size_of_loc_expr e);
+          print_loc_expr oc e
+      | LocList e ->
+          let size = List.fold_left (fun acc a -> acc + size_of_loc_expr a) 0 e in
+          print_2byte oc size;
+          List.iter (print_loc_expr oc) e
+      | LocRef f ->  print_ref oc f
+
+    let print_data_location oc dl =
+      match dl with
+      | DataLocBlock e ->
+          print_sleb128 oc (size_of_loc_expr e);
+          print_loc_expr oc e
+      | _ -> ()
+
     let print_addr oc a =
       fprintf oc "	.4byte		%a\n" label a
 
@@ -336,12 +390,12 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
     let print_compilation_unit oc tag =
       let prod_name = sprintf "AbsInt Angewandte Informatik GmbH:CompCert Version %s:%s" Version.version Configuration.arch in
       print_string oc (Sys.getcwd ());
-      print_addr oc (get_end_addr ());
-      print_addr oc (get_start_addr ());
+      print_addr oc tag.compile_unit_low_pc;
+      print_addr oc tag.compile_unit_high_pc;
       print_uleb128 oc 1;
       print_string oc tag.compile_unit_name;
       print_string oc prod_name;
-      print_addr oc (get_stmt_list_addr ())
+      print_addr oc tag.compile_unit_stmt_list
 
     let print_const_type oc ct =
       print_ref oc ct.const_type
@@ -360,29 +414,30 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
     let print_formal_parameter oc fp =
       print_file_loc oc fp.formal_parameter_file_loc;
       print_opt_value oc fp.formal_parameter_artificial print_flag;
-      print_opt_value oc fp.formal_parameter_location print_loc;
       print_opt_value oc fp.formal_parameter_name print_string;
-      print_opt_value oc fp.formal_parameter_segment print_loc;
       print_ref oc fp.formal_parameter_type;
-      print_opt_value oc fp.formal_parameter_variable_parameter print_flag
+      print_opt_value oc fp.formal_parameter_variable_parameter print_flag;
+      print_opt_value oc fp.formal_parameter_location print_loc
 
     let print_tag_label oc tl =
       print_ref oc tl.label_low_pc;
       print_string oc tl.label_name
 
+
     let print_lexical_block oc lb =
-      print_ref oc lb.lexical_block_high_pc;
-      print_ref oc lb.lexical_block_low_pc
+      print_opt_value oc lb.lexical_block_high_pc print_addr;
+      print_opt_value oc lb.lexical_block_low_pc print_addr
 
     let print_member oc mb =
       print_file_loc oc mb.member_file_loc;
       print_opt_value oc mb.member_byte_size print_byte;
       print_opt_value oc mb.member_bit_offset print_byte;
       print_opt_value oc mb.member_bit_size print_byte;
-      print_opt_value oc mb.member_data_member_location print_data_location;
       print_opt_value oc mb.member_declaration print_flag;
       print_opt_value oc mb.member_name print_string;
-      print_ref oc mb.member_type
+      print_ref oc mb.member_type;
+      print_opt_value oc mb.member_data_member_location print_data_location
+
 
     let print_pointer oc pt =
       print_ref oc pt.pointer_type
@@ -398,11 +453,10 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
       fprintf oc "	.4byte		%a\n" label s
      
     let print_subprogram oc sp =
-      let addr = get_fun_addr sp.subprogram_name  in
-      print_file_loc oc sp.subprogram_file_loc;
+      print_file_loc oc (Some sp.subprogram_file_loc);
       print_opt_value oc sp.subprogram_external print_flag;
-      print_opt_value oc sp.subprogram_frame_base print_loc;
-      print_opt_value oc addr print_subprogram_addr;
+      print_opt_value oc sp.subprogram_high_pc print_addr;
+      print_opt_value oc sp.subprogram_low_pc print_addr;
       print_string oc sp.subprogram_name;
       print_flag oc sp.subprogram_prototyped;
       print_opt_value oc sp.subprogram_type print_ref
@@ -431,12 +485,11 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
       print_opt_value oc up.unspecified_parameter_artificial print_flag
 
     let print_variable oc var =
-      print_file_loc oc var.variable_file_loc;
+      print_file_loc oc (Some var.variable_file_loc);
       print_opt_value oc var.variable_declaration print_flag;
       print_opt_value oc var.variable_external print_flag;
       print_opt_value oc var.variable_location print_loc;
       print_string oc var.variable_name;
-      print_opt_value oc var.variable_segment print_loc;
       print_ref oc var.variable_type
 
     let print_volatile_type oc vt =
@@ -482,16 +535,15 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
           print_sleb128 oc 0) entry
 
     (* Print the debug abbrev section *)
-    let print_debug_abbrev oc entry =
-      compute_abbrev entry;
+    let print_debug_abbrev oc entries =
+      List.iter (fun (_,_,e,_) -> compute_abbrev e) entries;
       print_abbrev oc
 
     (* Print the debug info section *)
-    let print_debug_info oc entry =
-      let debug_start = new_label () in
-      debug_start_addr:= debug_start;
-      fprintf oc"	.section	%s\n" (name_of_section Section_debug_info);
-      print_label oc debug_start;
+    let print_debug_info oc sec start entry  =
+      debug_start_addr:= start;
+      section oc (Section_debug_info sec);      
+      print_label oc start;
       let debug_length_start = new_label ()  (* Address used for length calculation *)
       and debug_end = new_label () in
       fprintf oc "	.4byte		%a-%a\n" label debug_end label debug_length_start;
@@ -503,10 +555,24 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
       print_sleb128 oc 0;
       print_label oc debug_end (* End of the debug section *)
 
+    let print_location_entry oc c_low l =
+      print_label oc (entry_to_label l.loc_id);
+      List.iter (fun (b,e,loc) ->
+        fprintf oc "	.4byte		%a-%a\n" label b label c_low;
+        fprintf oc "	.4byte		%a-%a\n" label e label c_low;
+        print_list_loc oc loc) l.loc;
+      fprintf oc "	.4byte	0\n";
+      fprintf oc "	.4byte	0\n"
+
+    let print_location_list oc (c_low,l) =
+      List.iter (print_location_entry oc c_low) l
 
     (* Print the debug info and abbrev section *)
-    let print_debug oc entry =
-      print_debug_abbrev oc entry;
-      print_debug_info oc entry
+    let print_debug oc entries =
+      print_debug_abbrev oc entries;
+      List.iter (fun (s,d,e,_) -> print_debug_info oc s d e) entries;
+      section oc Section_debug_loc;
+      List.iter (fun (_,_,_,l) -> print_location_list oc l) entries
+
 
   end
diff --git a/debug/DwarfPrinter.mli b/debug/DwarfPrinter.mli
index 9e0e6693..e1e10601 100644
--- a/debug/DwarfPrinter.mli
+++ b/debug/DwarfPrinter.mli
@@ -12,7 +12,7 @@
 
 open DwarfTypes
 
-module DwarfPrinter: functor (Target: DWARF_TARGET) -> functor (DwarfAbbrevs: DWARF_ABBREVS) ->
+module DwarfPrinter: functor (Target: DWARF_TARGET) ->
   sig
-    val print_debug: out_channel -> dw_entry -> unit
+    val print_debug: out_channel -> debug_entries -> unit
   end
diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli
index eaf07e1e..906b7cba 100644
--- a/debug/DwarfTypes.mli
+++ b/debug/DwarfTypes.mli
@@ -12,6 +12,8 @@
 
 (* Types used for writing dwarf debug information *)
 
+open BinNums
+open Camlcoq
 open Sections
 
 (* Basic types for the value of attributes *)
@@ -36,12 +38,20 @@ type address = int
 
 type block = string
 
-type location_value =
-  | LocConst of constant
-  | LocBlock of block
+type location_expression =
+  | DW_OP_plus_uconst of constant
+  | DW_OP_bregx of int * int32
+  | DW_OP_piece of int
+  | DW_OP_reg of int
 
+type location_value =
+  | LocSymbol of atom
+  | LocRef of address
+  | LocSimple of location_expression
+  | LocList of location_expression list
+        
 type data_location_value =
-  | DataLocBlock of block
+  | DataLocBlock of location_expression
   | DataLocRef of reference
 
 type bound_value =
@@ -50,7 +60,7 @@ type bound_value =
 
 (* Types representing the attribute information per tag value *)
 
-type file_loc = string * constant
+type file_loc = int * constant
 
 type dw_tag_array_type =
     {
@@ -67,7 +77,10 @@ type dw_tag_base_type =
 
 type dw_tag_compile_unit =
     {
-     compile_unit_name:            string;
+     compile_unit_name:      string;
+     compile_unit_low_pc:    int;
+     compile_unit_high_pc:   int;
+     compile_unit_stmt_list: int;
    }
 
 type dw_tag_const_type =
@@ -94,11 +107,10 @@ type dw_tag_formal_parameter =
     {
      formal_parameter_file_loc:           file_loc       option;
      formal_parameter_artificial:         flag           option;
-     formal_parameter_location:           location_value option;
      formal_parameter_name:               string         option;
-     formal_parameter_segment:            location_value option;
      formal_parameter_type:               reference;
      formal_parameter_variable_parameter: flag           option;
+     formal_parameter_location:           location_value option;
    }
 
 type dw_tag_label =
@@ -109,8 +121,8 @@ type dw_tag_label =
 
 type dw_tag_lexical_block =
     {
-     lexical_block_high_pc: address;
-     lexical_block_low_pc:  address;
+     lexical_block_high_pc: address option;
+     lexical_block_low_pc:  address option;
    }
 
 type dw_tag_member =
@@ -140,12 +152,13 @@ type dw_tag_structure_type =
 
 type dw_tag_subprogram =
     {
-     subprogram_file_loc:   file_loc       option;
-     subprogram_external:   flag           option;
-     subprogram_frame_base: location_value option;
+     subprogram_file_loc:   file_loc;
+     subprogram_external:   flag      option;
      subprogram_name:       string;
      subprogram_prototyped: flag;
-     subprogram_type:       reference      option;
+     subprogram_type:       reference option;
+     subprogram_high_pc:    reference option;
+     subprogram_low_pc:     reference option;
    }
 
 type dw_tag_subrange_type =
@@ -183,13 +196,12 @@ type dw_tag_unspecified_parameter =
 
 type dw_tag_variable =
     {
-     variable_file_loc:    file_loc       option;
+     variable_file_loc:    file_loc;
      variable_declaration: flag           option;
      variable_external:    flag           option;
-     variable_location:    location_value option;
      variable_name:        string;
-     variable_segment:     location_value option;
      variable_type:        reference;
+     variable_location:    location_value option;
    }
 
 type dw_tag_volatile_type =
@@ -228,46 +240,21 @@ type dw_entry =
      id:       reference;
    }
 
-(* Module type for a matching from type to dwarf encoding *)
-module type DWARF_ABBREVS =
-  sig
-    val sibling_type_abbr: int
-    val file_loc_type_abbr: int * int
-    val type_abbr: int
-    val name_type_abbr: int
-    val encoding_type_abbr: int
-    val byte_size_type_abbr: int
-    val member_size_abbr: int
-    val high_pc_type_abbr: int
-    val low_pc_type_abbr: int
-    val stmt_list_type_abbr: int
-    val declaration_type_abbr: int
-    val external_type_abbr: int
-    val prototyped_type_abbr: int
-    val bit_offset_type_abbr: int
-    val comp_dir_type_abbr: int
-    val language_type_abbr: int
-    val producer_type_abbr: int
-    val value_type_abbr: int
-    val artificial_type_abbr: int
-    val variable_parameter_type_abbr: int
-    val bit_size_type_abbr: int
-    val location_const_type_abbr: int
-    val location_block_type_abbr: int
-    val data_location_block_type_abbr: int
-    val data_location_ref_type_abbr: int
-    val bound_const_type_abbr: int
-    val bound_ref_type_abbr: int
-  end
+(* The type for the location list. *)
+type location_entry =
+    {
+     loc:     (int * int * location_value) list;
+     loc_id:  reference;
+   }
+type dw_locations = int * location_entry list
+
+type debug_entries = (string * int * dw_entry * dw_locations) list
 
 (* The target specific functions for printing the debug information *)
 module type DWARF_TARGET=
   sig
     val label: out_channel -> int -> unit
     val print_file_loc: out_channel -> file_loc -> unit
-    val get_start_addr: unit -> int
-    val get_end_addr: unit -> int
-    val get_stmt_list_addr: unit -> int    
-    val name_of_section: section_name -> string
-    val get_fun_addr: string -> (int * int) option
+    val section: out_channel -> section_name -> unit
+    val symbol: out_channel -> atom -> unit
   end
diff --git a/debug/DwarfUtil.ml b/debug/DwarfUtil.ml
index f47c2b58..16e446ee 100644
--- a/debug/DwarfUtil.ml
+++ b/debug/DwarfUtil.ml
@@ -14,18 +14,8 @@
 
 open DwarfTypes
 
-let id = ref 0
-
-let next_id () =
-  let nid = !id in
-  incr id; nid
-
-let reset_id () =
-  id := 0
-
 (* Generate a new entry from a given tag *)
-let new_entry tag =
-  let id = next_id () in
+let new_entry id tag =
   {
    tag = tag;
    children = [];
@@ -86,34 +76,67 @@ let dw_form_ref8     = 0x14
 let dw_ref_udata     = 0x15
 let dw_ref_indirect  = 0x16
 
+(* Operation encoding *)
+let dw_op_addr = 0x3
+let dw_op_plus_uconst = 0x23
+let dw_op_reg0 = 0x50
+let dw_op_regx = 0x90
+let dw_op_bregx = 0x92
+let dw_op_piece = 0x93
+
+
 (* Default corresponding encoding for the different abbreviations *)
-module DefaultAbbrevs =
-  struct
-    let sibling_type_abbr = dw_form_ref4
-    let file_loc_type_abbr = dw_form_data4,dw_form_udata
-    let type_abbr = dw_form_ref_addr
-    let name_type_abbr = dw_form_string
-    let encoding_type_abbr = dw_form_data1
-    let byte_size_type_abbr = dw_form_data1
-    let member_size_abbr = dw_form_udata
-    let high_pc_type_abbr = dw_form_addr
-    let low_pc_type_abbr = dw_form_addr
-    let stmt_list_type_abbr = dw_form_data4
-    let declaration_type_abbr = dw_form_flag
-    let external_type_abbr = dw_form_flag
-    let prototyped_type_abbr = dw_form_flag
-    let bit_offset_type_abbr = dw_form_data1
-    let comp_dir_type_abbr = dw_form_string
-    let language_type_abbr = dw_form_udata
-    let producer_type_abbr = dw_form_string
-    let value_type_abbr = dw_form_sdata
-    let artificial_type_abbr = dw_form_flag
-    let variable_parameter_type_abbr = dw_form_flag
-    let bit_size_type_abbr = dw_form_data1
-    let location_const_type_abbr = dw_form_data4
-    let location_block_type_abbr = dw_form_block
-    let data_location_block_type_abbr = dw_form_block
-    let data_location_ref_type_abbr = dw_form_ref4
-    let bound_const_type_abbr = dw_form_udata
-    let bound_ref_type_abbr=dw_form_ref4
-  end
+let sibling_type_abbr = dw_form_ref4
+let file_loc_type_abbr = dw_form_data4,dw_form_udata
+let type_abbr = dw_form_ref_addr
+let name_type_abbr = dw_form_string
+let encoding_type_abbr = dw_form_data1
+let byte_size_type_abbr = dw_form_data1
+let member_size_abbr = dw_form_udata
+let high_pc_type_abbr = dw_form_addr
+let low_pc_type_abbr = dw_form_addr
+let stmt_list_type_abbr = dw_form_data4
+let declaration_type_abbr = dw_form_flag
+let external_type_abbr = dw_form_flag
+let prototyped_type_abbr = dw_form_flag
+let bit_offset_type_abbr = dw_form_data1
+let comp_dir_type_abbr = dw_form_string
+let language_type_abbr = dw_form_udata
+let producer_type_abbr = dw_form_string
+let value_type_abbr = dw_form_sdata
+let artificial_type_abbr = dw_form_flag
+let variable_parameter_type_abbr = dw_form_flag
+let bit_size_type_abbr = dw_form_data1
+let location_ref_type_abbr = dw_form_data4
+let location_block_type_abbr = dw_form_block
+let data_location_block_type_abbr = dw_form_block
+let data_location_ref_type_abbr = dw_form_ref4
+let bound_const_type_abbr = dw_form_udata
+let bound_ref_type_abbr=dw_form_ref4
+
+(* Sizeof functions for the encoding of uleb128 and sleb128 *)
+let sizeof_uleb128 value =
+  let size = ref 1 in
+  let value = ref (value lsr 7) in
+  while !value <> 0 do
+    value := !value lsr 7;
+    incr size;
+  done;
+  !size
+
+let sizeof_sleb128 value =
+  let size = ref 1 in
+  let byte = ref (value land 0x7f) in
+  let value = ref (value lsr 7) in
+  while not ((!value = 0 && (!byte land 0x40) = 0) || (!value = -1 && ((!byte land 0x40) <> 0))) do
+    byte := !value land 0x7f;
+    value := !value lsr 7;
+    incr size;
+  done;
+  !size
+
+let size_of_loc_expr = function
+  | DW_OP_bregx (a,b) -> 1 + (sizeof_uleb128 a)  + (sizeof_sleb128 (Int32.to_int b))
+  | DW_OP_plus_uconst a
+  | DW_OP_piece a -> 1 + (sizeof_uleb128 a)
+  | DW_OP_reg i -> if i < 32 then 1 else  2
diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml
new file mode 100644
index 00000000..3239ceb6
--- /dev/null
+++ b/debug/Dwarfgen.ml
@@ -0,0 +1,444 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Bernhard Schommer, AbsInt Angewandte Informatik GmbH       *)
+(*                                                                     *)
+(*  AbsInt Angewandte Informatik GmbH. All rights reserved. This file  *)
+(*  is distributed under the terms of the INRIA Non-Commercial         *)
+(*  License Agreement.                                                 *)
+(*                                                                     *)
+(* *********************************************************************)
+
+open AST
+open C
+open Camlcoq
+open Cutil
+open DebugInformation
+open DwarfTypes
+open DwarfUtil
+(* Generate the dwarf DIE's from the information collected in DebugInformation *)
+
+(* Helper function to get values that must be set. *)
+let get_opt_val = function
+  | Some a -> a
+  | None -> assert false
+
+(* Auxiliary data structures and functions *)
+module IntSet = Set.Make(struct
+  type t = int
+  let compare (x:int) (y:int) = compare x y
+end)
+
+let rec mmap f env = function
+  | [] -> ([],env)
+  | hd :: tl ->
+      let (hd',env1) = f env hd in
+      let (tl', env2) = mmap f env1 tl in
+      (hd' :: tl', env2)
+
+(* Functions to translate the basetypes. *)
+let int_type_to_entry id i =
+   let encoding =
+    (match i.int_kind with
+    | IBool -> DW_ATE_boolean
+    | IChar ->
+        if !Machine.config.Machine.char_signed then 
+          DW_ATE_signed_char 
+        else 
+          DW_ATE_unsigned_char
+    | IInt | ILong | ILongLong | IShort | ISChar -> DW_ATE_signed
+    | _ -> DW_ATE_unsigned)in
+  let int = {
+    base_type_byte_size = sizeof_ikind i.int_kind;
+    base_type_encoding = Some encoding;
+    base_type_name = typ_to_string (TInt (i.int_kind,[]));} in
+  new_entry id (DW_TAG_base_type int)
+
+let float_type_to_entry id f = 
+  let byte_size = sizeof_fkind f.float_kind in
+  let float = {
+    base_type_byte_size = byte_size;
+    base_type_encoding = Some DW_ATE_float;
+    base_type_name = typ_to_string (TFloat (f.float_kind,[]));
+  } in
+  new_entry id (DW_TAG_base_type float)
+
+let void_to_entry id =
+  let void = {
+    base_type_byte_size = 0;
+    base_type_encoding = None;
+    base_type_name = "void";
+  } in
+  new_entry id (DW_TAG_base_type void)
+
+let translate_file_loc sec (f,l)  =
+  Hashtbl.find filenum (sec,f),l
+
+let translate_file_loc_opt sec = function
+  | None -> None
+  | Some (f,l) ->
+    try 
+      Some (translate_file_loc sec (f,l))
+    with Not_found -> None
+
+let typedef_to_entry sec id t =
+  let i = get_opt_val t.typ in
+  let td = {
+    typedef_file_loc = translate_file_loc_opt sec t.typedef_file_loc;
+    typedef_name = t.typedef_name;
+    typedef_type = i;
+  } in
+  new_entry id (DW_TAG_typedef td) 
+
+let pointer_to_entry id p =
+  let p = {pointer_type = p.pts} in
+  new_entry id (DW_TAG_pointer_type p)
+
+let array_to_entry id arr =
+  let arr_tag = {
+    array_type_file_loc = None;
+    array_type = arr.arr_type;
+  } in
+  let arr_entry = new_entry id (DW_TAG_array_type arr_tag) in
+  let children = List.map (fun a ->
+    let r = match a with
+    | None -> None
+    | Some i ->
+        let bound = Int64.to_int (Int64.sub i Int64.one) in
+        Some (BoundConst bound) in
+    let s = {
+       subrange_type = None;
+       subrange_upper_bound = r;
+    } in
+    new_entry (next_id ()) (DW_TAG_subrange_type s)) arr.arr_size in
+  add_children arr_entry children
+
+let const_to_entry id c =
+  new_entry id (DW_TAG_const_type ({const_type = c.cst_type}))
+
+let volatile_to_entry id v =
+  new_entry id (DW_TAG_volatile_type ({volatile_type = v.vol_type}))
+
+let enum_to_entry sec id e =
+  let enumerator_to_entry e =
+    let tag =
+      {
+       enumerator_file_loc = None;
+       enumerator_value = Int64.to_int (e.enumerator_const);
+       enumerator_name = e.enumerator_name;
+     } in
+    new_entry (next_id ()) (DW_TAG_enumerator tag) in
+  let bs = sizeof_ikind enum_ikind in
+  let enum = {
+    enumeration_file_loc = translate_file_loc_opt sec e.enum_file_loc;
+    enumeration_byte_size = bs;
+    enumeration_declaration = Some false;
+    enumeration_name = Some e.enum_name;
+  } in
+  let enum = new_entry id (DW_TAG_enumeration_type enum) in
+  let child = List.map enumerator_to_entry e.enum_enumerators in
+  add_children enum child
+
+let fun_type_to_entry id f =
+  let children = if f.fun_prototyped then
+    let u = {
+      unspecified_parameter_file_loc = None;
+      unspecified_parameter_artificial = None;
+    } in
+    [new_entry (next_id ()) (DW_TAG_unspecified_parameter u)]
+  else
+    List.map (fun p ->
+      let fp = {
+        formal_parameter_file_loc = None;
+        formal_parameter_artificial = None;
+        formal_parameter_name = if p.param_name <> "" then Some p.param_name else None;
+        formal_parameter_type = p.param_type;
+        formal_parameter_variable_parameter = None;
+        formal_parameter_location = None;
+      } in
+      new_entry (next_id ()) (DW_TAG_formal_parameter fp)) f.fun_params;
+  in
+  let s = {
+    subroutine_type = f.fun_return_type;
+    subroutine_prototyped = f.fun_prototyped
+  } in
+  let s = new_entry id (DW_TAG_subroutine_type s) in
+  add_children s children
+
+let member_to_entry mem =
+  let mem = {
+    member_file_loc = None;
+    member_byte_size = mem.cfd_byte_size;
+    member_bit_offset = mem.cfd_bit_offset;
+    member_bit_size = mem.cfd_bit_size;
+    member_data_member_location =
+    (match mem.cfd_byte_offset with 
+    | None -> None 
+    | Some s -> Some (DataLocBlock (DW_OP_plus_uconst s)));
+    member_declaration = None;
+    member_name = Some (mem.cfd_name);
+    member_type = mem.cfd_typ;
+  } in
+  new_entry (next_id ()) (DW_TAG_member mem)
+
+let struct_to_entry sec id s =
+  let tag = {
+     structure_file_loc = translate_file_loc_opt sec s.ct_file_loc;
+     structure_byte_size = s.ct_sizeof;
+     structure_declaration = Some s.ct_declaration;
+     structure_name = if s.ct_name <> "" then Some s.ct_name else None;
+  } in
+  let entry = new_entry id (DW_TAG_structure_type tag) in
+  let child = List.map member_to_entry s.ct_members in
+  add_children entry child
+
+let union_to_entry sec id s =
+  let tag = {
+    union_file_loc =  translate_file_loc_opt sec s.ct_file_loc;
+    union_byte_size = s.ct_sizeof;
+    union_declaration = Some s.ct_declaration;
+    union_name = if s.ct_name <> "" then Some s.ct_name else None;
+  } in
+  let entry = new_entry id (DW_TAG_union_type tag) in
+  let child = List.map member_to_entry s.ct_members in
+  add_children entry child
+
+let composite_to_entry sec id s =
+  match s.ct_sou with
+  | Struct -> struct_to_entry sec id s
+  | Union -> union_to_entry sec id s
+
+let infotype_to_entry sec id = function
+  | IntegerType i -> int_type_to_entry id i
+  | FloatType f -> float_type_to_entry id f
+  | PointerType p -> pointer_to_entry id p
+  | ArrayType arr -> array_to_entry id arr
+  | CompositeType c -> composite_to_entry sec id c
+  | EnumType e -> enum_to_entry sec id e
+  | FunctionType f -> fun_type_to_entry id f
+  | Typedef t -> typedef_to_entry sec id t
+  | ConstType c -> const_to_entry id c
+  | VolatileType v -> volatile_to_entry id v
+  | Void -> void_to_entry id
+
+let needs_types id d =
+  let add_type id d =
+    if not (IntSet.mem id d) then
+        IntSet.add id d,true
+      else 
+        d,false in
+  let t = Hashtbl.find types id in
+  match t with
+  | IntegerType _ 
+  | FloatType _
+  | Void
+  | EnumType _ -> d,false
+  | Typedef t ->
+      add_type (get_opt_val t.typ) d
+  | PointerType p -> 
+      add_type p.pts d
+  | ArrayType arr -> 
+      add_type arr.arr_type d
+  | ConstType c ->
+      add_type c.cst_type d
+  | VolatileType v ->
+      add_type v.vol_type d
+  | FunctionType f ->
+      let d,c = match f.fun_return_type with
+      | Some t -> add_type t d 
+      | None -> d,false in
+      List.fold_left (fun (d,c) p ->
+        let d,c' = add_type p.param_type d in
+        d,c||c') (d,c) f.fun_params
+  | CompositeType c -> 
+      List.fold_left (fun (d,c) f ->
+        let d,c' = add_type f.cfd_typ d in
+        d,c||c') (d,false) c.ct_members
+
+let gen_types sec needed =
+  let rec aux d =
+    let d,c = IntSet.fold (fun id (d,c) ->
+      let d,c' = needs_types id d in
+      d,c||c') d (d,false) in
+    if c then
+      aux d
+    else
+      d in
+  let typs = aux needed in
+  List.rev (Hashtbl.fold (fun id t acc -> 
+    if IntSet.mem id typs then
+      (infotype_to_entry sec id t)::acc
+    else 
+      acc) types [])
+
+let global_variable_to_entry sec acc id v =
+  let var = {
+    variable_file_loc = translate_file_loc sec v.gvar_file_loc;
+    variable_declaration = Some v.gvar_declaration;
+    variable_external = Some v.gvar_external;
+    variable_name = v.gvar_name;
+    variable_type = v.gvar_type;
+    variable_location = match v.gvar_atom with Some a -> Some (LocSymbol a) | None -> None;
+  } in
+  new_entry id (DW_TAG_variable var),IntSet.add v.gvar_type acc
+
+let gen_splitlong op_hi op_lo =
+  let op_piece = DW_OP_piece 4 in
+  op_piece::op_hi@(op_piece::op_lo)
+  
+let translate_function_loc a = function 
+  | BA_addrstack (ofs) ->
+      let ofs = camlint_of_coqint ofs in
+      Some (LocSimple (DW_OP_bregx (a,ofs))),[]
+  | BA_splitlong (BA_addrstack hi,BA_addrstack lo)->
+      let hi = camlint_of_coqint hi 
+      and lo = camlint_of_coqint lo in
+      if lo = Int32.add hi 4l then
+        Some (LocSimple (DW_OP_bregx (a,hi))),[]
+      else
+        let op_hi = [DW_OP_bregx (a,hi)]
+        and op_lo = [DW_OP_bregx (a,lo)] in
+        Some (LocList (gen_splitlong op_hi op_lo)),[]
+  | _ -> None,[]
+      
+let range_entry_loc (sp,l) =
+  let rec aux = function
+    | BA i ->  [DW_OP_reg i]
+    | BA_addrstack ofs -> 
+        let ofs = camlint_of_coqint ofs in
+        [DW_OP_bregx (sp,ofs)]
+    | BA_splitlong (hi,lo) ->
+        let hi = aux hi
+        and lo = aux lo in
+        gen_splitlong hi lo
+    | _ -> assert false in
+  match aux l with
+  | [] -> assert false
+  | [a] -> LocSimple a
+  | a::rest -> LocList (a::rest)
+
+let location_entry f_id atom =
+  try
+    begin 
+      match (Hashtbl.find var_locations atom) with
+      | FunctionLoc (a,r) ->
+          translate_function_loc a r
+      | RangeLoc l ->
+          let l = List.map (fun i -> 
+            let hi = get_opt_val i.range_start
+            and lo = get_opt_val i.range_end in
+            let hi = Hashtbl.find label_translation (f_id,hi)
+            and lo = Hashtbl.find label_translation (f_id,lo) in
+            hi,lo,range_entry_loc i.var_loc) l in
+          let id = next_id () in
+        Some (LocRef id),[{loc = l;loc_id = id;}]
+    end
+  with Not_found -> None,[]
+
+let function_parameter_to_entry f_id (acc,bcc) p =
+  let loc,loc_list = location_entry f_id (get_opt_val p.parameter_atom) in
+  let p = {
+    formal_parameter_file_loc = None;
+    formal_parameter_artificial = None;
+    formal_parameter_name = Some p.parameter_name;
+    formal_parameter_type = p.parameter_type;
+    formal_parameter_variable_parameter = None;
+    formal_parameter_location = loc;
+  } in
+  new_entry (next_id ()) (DW_TAG_formal_parameter p),(IntSet.add p.formal_parameter_type acc,loc_list@bcc)
+
+let rec local_variable_to_entry sec f_id (acc,bcc) v id =
+  let loc,loc_list = location_entry f_id (get_opt_val v.lvar_atom) in
+  let var = {
+    variable_file_loc = translate_file_loc sec v.lvar_file_loc;
+    variable_declaration = None;
+    variable_external = None;
+    variable_name = v.lvar_name;
+    variable_type = v.lvar_type;
+    variable_location = loc;
+  } in
+  new_entry id (DW_TAG_variable var),(IntSet.add v.lvar_type acc,loc_list@bcc)
+
+and scope_to_entry sec f_id acc sc id =
+  let l_pc,h_pc = try
+    let r = Hashtbl.find scope_ranges id in
+    let lbl l = match l with 
+    | Some l -> Some (Hashtbl.find label_translation (f_id,l)) 
+    | None -> None in
+    begin
+      match r with
+      | [] -> None,None
+      | [a] -> lbl a.start_addr, lbl a.end_addr
+      | a::rest -> lbl (List.hd (List.rev rest)).start_addr,lbl a.end_addr
+    end
+  with Not_found -> None,None in
+  let scope = {
+    lexical_block_high_pc = h_pc;
+    lexical_block_low_pc = l_pc;
+  } in
+  let vars,acc = mmap (local_to_entry sec f_id) acc sc.scope_variables in
+  let entry = new_entry id (DW_TAG_lexical_block scope) in
+  add_children entry vars,acc
+
+and local_to_entry sec f_id acc id =
+  match Hashtbl.find local_variables id with
+  | LocalVariable v -> local_variable_to_entry sec f_id acc v id
+  | Scope v -> scope_to_entry sec f_id acc v id
+
+let fun_scope_to_entries sec f_id acc id =
+  match id with
+  | None -> [],acc
+  | Some id ->
+      let sc = Hashtbl.find local_variables id in
+      (match sc with
+      | Scope sc ->mmap (local_to_entry sec f_id) acc sc.scope_variables
+      | _ -> assert false)
+
+let function_to_entry sec (acc,bcc) id f =
+  let f_tag = {
+    subprogram_file_loc = translate_file_loc sec f.fun_file_loc;
+    subprogram_external = Some f.fun_external;
+    subprogram_name = f.fun_name;
+    subprogram_prototyped = true;
+    subprogram_type = f.fun_return_type;
+    subprogram_high_pc = f.fun_high_pc;
+    subprogram_low_pc = f.fun_low_pc;
+  } in
+  let f_id = get_opt_val f.fun_atom in
+  let acc = match f.fun_return_type with Some s -> IntSet.add s acc | None -> acc in
+  let f_entry =  new_entry id (DW_TAG_subprogram f_tag) in
+  let params,(acc,bcc) = mmap (function_parameter_to_entry f_id) (acc,bcc) f.fun_parameter in
+  let vars,(acc,bcc) = fun_scope_to_entries sec f_id (acc,bcc) f.fun_scope in
+  add_children f_entry (params@vars),(acc,bcc)
+     
+let definition_to_entry sec (acc,bcc) id t =
+  match t with
+  | GlobalVariable g -> let e,acc = global_variable_to_entry sec acc id g in
+    e,(acc,bcc)
+  | Function f -> function_to_entry sec (acc,bcc) id f
+
+module StringMap = Map.Make(String)
+
+let gen_debug_info sec_name var_section : debug_entries =
+  let defs = Hashtbl.fold (fun id t acc ->
+    let s = match t with
+    | GlobalVariable _ -> var_section
+    | Function f -> sec_name (get_opt_val f.fun_atom) in
+    let old = try StringMap.find s acc with Not_found -> [] in
+    StringMap.add s ((id,t)::old) acc) definitions StringMap.empty in
+  StringMap.fold (fun s defs acc ->
+    let defs,(ty,locs) = List.fold_left (fun (acc,bcc) (id,t) -> 
+      let t,bcc = definition_to_entry s bcc id t in
+      t::acc,bcc) ([],(IntSet.empty,[])) defs in
+    let line_start,low_pc,debug_start,_ = Hashtbl.find compilation_section_start s
+    and high_pc = Hashtbl.find compilation_section_end s in
+    let cp = {
+      compile_unit_name = !file_name;
+      compile_unit_low_pc = low_pc;
+      compile_unit_high_pc = high_pc;
+      compile_unit_stmt_list = line_start; 
+    } in
+    let cp = new_entry (next_id ()) (DW_TAG_compile_unit cp) in
+    let cp = add_children cp ((gen_types s ty) @ defs) in
+    (s,debug_start,cp,(low_pc,locs))::acc) defs []
diff --git a/driver/Driver.ml b/driver/Driver.ml
index f53de821..9b1a6e70 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 *)
 
@@ -682,6 +683,7 @@ let _ =
     Builtins.set C2C.builtins;
     CPragmas.initialize();
     parse_cmdline cmdline_actions;
+    DebugInit.init (); (* Initialize the debug functions *)
     let nolink = !option_c || !option_S || !option_E || !option_interp in
     if nolink && !option_o <> None && !num_source_files >= 2 then begin
       eprintf "Ambiguous '-o' option (multiple source files)\n";
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
index 439dd2b0..51169d86 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -101,7 +101,8 @@ module Cygwin_System : SYSTEM =
       | Section_user(s, wr, ex) ->
           sprintf ".section	\"%s\", \"%s\"\n"
             s (if ex then "xr" else if wr then "d" else "dr")
-      | Section_debug_info
+      | Section_debug_info _
+      | Section_debug_loc
       | Section_debug_abbrev -> "" (* Dummy value *)
 
     let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *)
@@ -150,7 +151,8 @@ module ELF_System : SYSTEM =
       | Section_user(s, wr, ex) ->
           sprintf ".section	\"%s\",\"a%s%s\",@progbits"
             s (if wr then "w" else "") (if ex then "x" else "")
-      | Section_debug_info
+      | Section_debug_info _
+      | Section_debug_loc
       | Section_debug_abbrev -> "" (* Dummy value *)
             
     let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *)
@@ -202,7 +204,8 @@ module MacOS_System : SYSTEM =
           sprintf ".section	\"%s\", %s, %s"
             (if wr then "__DATA" else "__TEXT") s
             (if ex then "regular, pure_instructions" else "regular")
-      | Section_debug_info
+      | Section_debug_info _
+      | Section_debug_loc
       | Section_debug_abbrev -> "" (* Dummy value *)
     
     let stack_alignment =  16 (* mandatory *)
@@ -770,7 +773,7 @@ module Target(System: SYSTEM):TARGET =
 
     let get_stmt_list_addr () = -1 (* Dummy constant *)
 
-    module DwarfAbbrevs = DwarfUtil.DefaultAbbrevs (* Dummy Abbrev types *)
+    let get_debug_start_addr () = -1 (* Dummy constant *)
 
     let label = label
        
diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml
index 68c095f0..c50b3230 100644
--- a/lib/Camlcoq.ml
+++ b/lib/Camlcoq.ml
@@ -295,8 +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
-
+    a 
 let extern_atom a =
   try
     Hashtbl.find string_of_atom a
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index a7e66701..5764aa8f 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -330,8 +330,9 @@ let p_section oc = function
   | Section_literal -> fprintf oc "{\"Section Name\":\"Literal\"}"
   | Section_jumptable -> fprintf oc "{\"Section Name\":\"Jumptable\"}"
   | Section_user (s,w,e) -> fprintf oc "{\"Section Name\":%s,\"Writable\":%B,\"Executable\":%B}" s w e
-  | Section_debug_info 
-  | Section_debug_abbrev -> () (* There should be no info in the debug sections *)
+  | Section_debug_info _
+  | Section_debug_abbrev 
+  | Section_debug_loc -> () (* There should be no info in the debug sections *)
 
 let p_int_opt oc = function
   | None -> fprintf oc "0"
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index fc0fc44e..5a365123 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -563,7 +563,7 @@ let num_crbit = function
   | CRbit_3 -> 3
   | CRbit_6 -> 6
 
-let expand_instruction instr =
+let expand_instruction_simple instr =
   match instr with
   | Pallocframe(sz, ofs,retofs) ->
       let variadic = (!current_function).fn_sig.sig_cc.cc_vararg in
@@ -637,22 +637,160 @@ let expand_instruction instr =
   | _ ->
       emit instr
 
-let expand_function fn =
+(* Translate to the integer identifier of the register as
+   the EABI specifies *)
+
+let int_reg_to_dwarf = function
+   | GPR0 -> 0  | GPR1 -> 1  | GPR2 -> 2  | GPR3 -> 3
+   | GPR4 -> 4  | GPR5 -> 5  | GPR6 -> 6  | GPR7 -> 7
+   | GPR8 -> 8  | GPR9 -> 9  | GPR10 -> 10 | GPR11 -> 11
+   | GPR12 -> 12 | GPR13 -> 13 | GPR14 -> 14 | GPR15 -> 15
+   | GPR16 -> 16 | GPR17 -> 17 | GPR18 -> 18 | GPR19 -> 19
+   | GPR20 -> 20 | GPR21 -> 21 | GPR22 -> 22 | GPR23 -> 23
+   | GPR24 -> 24 | GPR25 -> 25 | GPR26 -> 26 | GPR27 -> 27
+   | GPR28 -> 28 | GPR29 -> 29 | GPR30 -> 30 | GPR31 -> 31
+
+let float_reg_to_dwarf = function
+   | FPR0 -> 32  | FPR1 -> 33  | FPR2 -> 34  | FPR3 -> 35
+   | FPR4 -> 36  | FPR5 -> 37  | FPR6 -> 38  | FPR7 -> 39
+   | FPR8 -> 40  | FPR9 -> 41  | FPR10 -> 42 | FPR11 -> 43
+   | FPR12 -> 44 | FPR13 -> 45 | FPR14 -> 46 | FPR15 -> 47
+   | FPR16 -> 48 | FPR17 -> 49 | FPR18 -> 50 | FPR19 -> 51
+   | FPR20 -> 52 | FPR21 -> 53 | FPR22 -> 54| FPR23 -> 55
+   | FPR24 -> 56 | FPR25 -> 57 | FPR26 -> 58 | FPR27 -> 59
+   | FPR28 -> 60 | FPR29 -> 61 | FPR30 -> 62 | FPR31 -> 63
+
+let preg_to_dwarf_int = function
+   | IR r -> int_reg_to_dwarf r
+   | FR r -> float_reg_to_dwarf r
+   | _ -> assert false
+
+
+let translate_annot annot = 
+  let rec aux = function
+    | BA x -> Some (BA (preg_to_dwarf_int x))
+    | BA_int _
+    | BA_long _
+    | BA_float _
+    | BA_single _
+    | BA_loadglobal _
+    | BA_addrglobal _
+    | BA_loadstack _ -> None
+    | BA_addrstack ofs -> Some (BA_addrstack ofs)
+    | BA_splitlong (hi,lo) -> 
+        begin
+          match (aux hi,aux lo) with
+          | Some hi ,Some lo -> Some (BA_splitlong (hi,lo))
+          | _,_ -> None
+        end in
+  (match annot with
+  | [] -> None
+  | a::_ -> aux a)
+
+let expand_scope id lbl oldscopes newscopes =
+  let opening = List.filter (fun a -> not (List.mem a oldscopes)) newscopes
+  and closing = List.filter (fun a -> not (List.mem a newscopes)) oldscopes in
+  List.iter (fun i -> Debug.open_scope id i lbl) opening;
+  List.iter (fun i -> Debug.close_scope id i lbl) closing
+
+let expand_instruction id l =
+  let get_lbl = function
+    | None -> 
+        let lbl = new_label () in
+        emit (Plabel lbl);
+        lbl
+    | Some lbl -> lbl in
+  let rec  aux lbl scopes = function
+    | [] -> let lbl = get_lbl lbl in
+      Debug.function_end id lbl
+    | (Pbuiltin(EF_debug (kind,txt,_x),args,_) as i)::rest ->
+        let kind = (P.to_int kind) in
+        emit i;
+        begin
+          match kind with
+          | 1-> 
+              aux lbl scopes rest
+          | 2 ->
+              aux  lbl scopes rest
+          | 3 ->
+             begin 
+               match translate_annot args with
+               | Some a ->
+                   let lbl = get_lbl lbl in
+                   Debug.start_live_range txt lbl (1,a);
+                   aux (Some lbl) scopes rest
+               | None ->  aux lbl scopes rest
+             end
+          | 4 ->
+              let lbl = get_lbl lbl in
+              Debug.end_live_range txt lbl;
+              aux (Some lbl) scopes rest
+          | 5 ->
+              begin
+                match translate_annot args with
+                | Some a->
+                    Debug.stack_variable txt (1,a);
+                    aux lbl scopes rest
+                | _ ->  aux lbl scopes rest
+              end
+          | 6  ->
+              let lbl = get_lbl lbl in
+              let scopes' = List.map (function BA_int x -> Int32.to_int (camlint_of_coqint x) | _ -> assert false) args in
+              expand_scope id lbl scopes scopes';
+              aux (Some lbl) scopes' rest
+          | _ ->
+              aux None scopes rest
+        end
+    | i::rest -> expand_instruction_simple i; aux None scopes rest in
+  (* We need to move all closing debug annotations before the last real statement *)
+  let rec move_debug acc = function
+    | (Pbuiltin(EF_debug (kind,txt,_x),args,_) as i)::rest ->
+        move_debug (i::acc) rest (* Move the debug annotations forward *)
+    | b::rest -> List.rev (b::(List.rev acc)@rest) (* We found the first non debug location *)
+    | [] -> List.rev acc (* This actually can never happen *) in
+  aux None [] (move_debug [] (List.rev l))
+      
+
+let expand_function id fn =
   try
     set_current_function fn;
-    List.iter expand_instruction fn.fn_code;
+    if !Clflags.option_g then
+      expand_instruction id fn.fn_code
+    else
+      List.iter expand_instruction_simple fn.fn_code;
     Errors.OK (get_current_function ())
   with Error s ->
     Errors.Error (Errors.msg (coqstring_of_camlstring s))
 
-let expand_fundef = function
+let expand_fundef id = function
   | Internal f ->
-      begin match expand_function f with
+      begin match expand_function id f with
       | Errors.OK tf -> Errors.OK (Internal tf)
       | Errors.Error msg -> Errors.Error msg
       end
   | External ef ->
       Errors.OK (External ef)
 
+let rec transform_partial_prog transfun p =
+  match p with
+  | [] -> Errors.OK []
+  | (id,Gvar v)::l ->
+      (match transform_partial_prog transfun l with
+      | Errors.OK x -> Errors.OK ((id,Gvar v)::x)
+      | Errors.Error msg -> Errors.Error msg)
+  | (id,Gfun f)::l ->
+      (match transfun id f with
+      | Errors.OK tf ->
+          (match transform_partial_prog transfun l with
+          | Errors.OK x -> Errors.OK ((id,Gfun tf)::x)
+          | Errors.Error msg -> Errors.Error msg)
+      | Errors.Error msg ->
+          Errors.Error ((Errors.MSG (coqstring_of_camlstring "In function"))::((Errors.CTX
+          id) :: (Errors.MSG (coqstring_of_camlstring ": ") :: msg))))
+
 let expand_program (p: Asm.program) : Asm.program Errors.res =
-  AST.transform_partial_program expand_fundef p
+  match transform_partial_prog expand_fundef p.prog_defs with
+  | Errors.OK x-> 
+      Errors.OK { prog_defs = x; prog_public = p.prog_public; prog_main =
+      p.prog_main }
+  | Errors.Error msg -> Errors.Error msg
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index eca7a1b8..3c73f22d 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -78,6 +78,8 @@ let end_addr = ref (-1)
 
 let stmt_list_addr = ref (-1)
 
+let debug_start_addr = ref (-1)
+
 let label = elf_label
 
 module Linux_System : SYSTEM =
@@ -129,9 +131,10 @@ module Linux_System : SYSTEM =
       | Section_user(s, wr, ex) ->
           sprintf ".section	\"%s\",\"a%s%s\",@progbits"
             s (if wr then "w" else "") (if ex then "x" else "")
-      | Section_debug_info -> ".debug_info,\"\",@progbits"
+      | Section_debug_info _ -> ".debug_info,\"\",@progbits"
       | Section_debug_abbrev -> ".debug_abbrev,\"\",@progbits"
-    
+      | Section_debug_loc -> ".debug_loc,\"\",@progbits"
+            
     let section oc sec =
       let name = name_of_section sec in
       assert (name <> "COMM");
@@ -207,14 +210,20 @@ module Diab_System : SYSTEM =
             | true, false -> 'd'                (* data *)
             | false, true -> 'c'                (* text *)
             | false, false -> 'r')              (* const *)
-      | Section_debug_info -> ".debug_info,,n"
-      | Section_debug_abbrev -> ".debug_abbrev,,n"
+      | Section_debug_info s -> sprintf ".section	.debug_info%s,,n" (if s <> ".text" then s else "")
+      | Section_debug_abbrev -> ".section	.debug_abbrev,,n"
+      | Section_debug_loc -> ".section	.debug_loc,,n"
 
     let section oc sec =
       let name = name_of_section sec in
       assert (name <> "COMM");
-      fprintf oc "	%s\n" name
-
+      match sec with
+      | Section_debug_info s ->
+          fprintf oc "	%s\n" name;
+          if s <> ".text" then
+            fprintf oc "	.sectionlink	.debug_info\n"
+      | _ ->
+          fprintf oc "	%s\n" name
 
     let print_file_line oc file line =
       print_file_line_d2 oc comment file line
@@ -229,65 +238,51 @@ module Diab_System : SYSTEM =
     let cfi_rel_offset oc reg ofs = ()
         
     let print_prologue oc =
-      fprintf oc "	.xopt	align-fill-text=0x60000000\n";
-      if !Clflags.option_g then
-        begin
-          fprintf oc "	.text\n";
-          fprintf oc "	.section	.debug_line,,n\n";
-          let label_line_start = new_label () in
-          stmt_list_addr := label_line_start;
-          fprintf oc "%a:\n" label label_line_start;
-          fprintf oc "	.text\n";
-          let label_start = new_label () in
-          start_addr := label_start;
-          fprintf oc "%a:\n" label label_start;
-          fprintf oc "	.d2_line_start	.debug_line\n";
-        end
-
-    let filenum : (string,int) Hashtbl.t = Hashtbl.create 7
-
-    let additional_debug_sections: StringSet.t ref = ref StringSet.empty
-
+      fprintf oc "	.xopt	align-fill-text=0x60000000\n"
 
     let print_epilogue oc =
-      if !Clflags.option_g then
-        begin
-          fprintf oc "\n";
-          let label_end = new_label () in
-          end_addr := label_end;
-          fprintf oc "%a:\n" label label_end;
-          fprintf oc "	.text\n";
-          StringSet.iter (fun file ->
-            let label = new_label () in
-            Hashtbl.add filenum file label;
-            fprintf oc ".L%d:	.d2filenum \"%s\"\n" label file) !all_files;
-          fprintf oc "	.d2_line_end\n";
-          StringSet.iter (fun s ->
-            fprintf oc "	%s\n" s;
-            fprintf oc "	.d2_line_end\n") !additional_debug_sections
-        end
+      let end_label sec = 
+        fprintf oc "\n";
+        fprintf oc "	%s\n" sec;
+        let label_end = new_label () in
+        fprintf oc "%a:\n" label label_end;
+        label_end 
+      and entry_label f =
+        let label = new_label () in
+        fprintf oc ".L%d:	.d2filenum \"%s\"\n" label f;
+        label
+      and end_line () =   fprintf oc "	.d2_line_end\n" in
+      Debug.compute_file_enum end_label entry_label end_line
 
     let print_file_loc oc (file,col) =
-      fprintf oc "	.4byte		%a\n" label (Hashtbl.find filenum file);
+      fprintf oc "	.4byte		1\n";(* label (Hashtbl.find filenum file);*)
       fprintf oc "	.uleb128	%d\n" col
 
     let debug_section oc sec =
-      if !Clflags.option_g && Configuration.advanced_debug then
-        match sec with
-        | Section_user (name,_,_)  ->
-            let sec_name = name_of_section sec in
-            if not (StringSet.mem sec_name !additional_debug_sections) then
-              begin
-                let name = ".debug_line"^name in
-                additional_debug_sections := StringSet.add sec_name !additional_debug_sections;
-                fprintf oc "	.section	%s,,n\n" name;
-                fprintf oc "	.sectionlink	.debug_line\n";
-                section oc sec;
-                fprintf oc "	.d2_line_start	%s\n" name
-              end
-        | _ -> () (* Only the case of a user section is interresting *)
-      else
-        ()
+      match sec with
+      | Section_debug_abbrev 
+      | Section_debug_info _
+      | Section_debug_loc -> ()
+      | sec ->
+          let name = match sec with
+          | Section_user (name,_,_) -> name
+          | _ -> name_of_section sec in
+          if not (Debug.exists_section name) then 
+            let line_start = new_label ()
+            and low_pc = new_label ()
+            and debug_info = new_label () in
+            Debug.add_compilation_section_start name (line_start,low_pc,debug_info,name_of_section sec);
+            let line_name = ".debug_line" ^(if name <> ".text" then name else "") in 
+            fprintf oc "	.section	%s,,n\n" line_name;
+            if name <> ".text" then
+              fprintf oc "	.sectionlink	.debug_line\n";
+            fprintf oc "%a:\n" label line_start;
+            section oc sec;
+            fprintf oc "%a:\n" label low_pc;
+            fprintf oc "	.0byte	%a\n" label debug_info;
+            fprintf oc "	.d2_line_start	%s\n" line_name
+          else
+            ()
             
 
   end
@@ -855,14 +850,13 @@ module Target (System : SYSTEM):TARGET =
 
     let get_stmt_list_addr () = !stmt_list_addr
 
-    module DwarfAbbrevs = DwarfUtil.DefaultAbbrevs
+    let get_debug_start_addr () = !debug_start_addr
 
     let new_label = new_label            
 
     let section oc sec =
       section oc sec;
       debug_section oc sec
-
   end
 
 let sel_target () =