Merge branch 'dwarf' of /local/schommer/trunk/build/compcert.ppc/compcert into dwarf

24 files changed, 1615 insertions, 42 deletions

diff --git a/Makefile b/Makefile
index 820908b0..afd26c4c 100644
--- a/Makefile
+++ b/Makefile
@@ -15,7 +15,7 @@
 
 include Makefile.config
 
-DIRS=lib common $(ARCH) backend cfrontend driver \
+DIRS=lib common $(ARCH) backend cfrontend driver debug\
   flocq/Core flocq/Prop flocq/Calc flocq/Appli exportclight \
   cparser cparser/validator
 
@@ -203,6 +203,7 @@ compcert.ini: Makefile.config VERSION
          echo "system=$(SYSTEM)"; \
          echo "has_runtime_lib=$(HAS_RUNTIME_LIB)"; \
          echo "asm_supports_cfi=$(ASM_SUPPORTS_CFI)"; \
+         echo "advanced_debug=$(ADVANCED_DEBUG)"; \
          echo "struct_passing_style=$(STRUCT_PASSING)"; \
          echo "struct_return_style=$(STRUCT_RETURN)"; \
          version=`cat VERSION`; \
diff --git a/Makefile.extr b/Makefile.extr
index fed2d78f..4e17e904 100644
--- a/Makefile.extr
+++ b/Makefile.extr
@@ -21,7 +21,7 @@ include Makefile.config
 
 DIRS=extraction \
   lib common $(ARCH) backend cfrontend cparser driver \
-  exportclight
+  exportclight debug
 
 # Directories containing Caml code that must be preprocessed by Camlp4
 
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index 9e45019e..b37683d3 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -1127,6 +1127,18 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
     let print_epilogue oc = ()
 
     let default_falignment = 4
+
+    let get_start_addr () = -1 (* Dummy constant *)
+
+    let get_end_addr () = -1 (* Dummy constant *)
+
+    let get_stmt_list_addr () = -1 (* Dummy constant *)
+
+    module DwarfAbbrevs = DwarfUtil.DefaultAbbrevs (* Dummy Abbrev types *)
+        
+    let label = print_label
+       
+    let new_label = new_label
   end
 
 let sel_target () = 
diff --git a/backend/PrintAnnot.ml b/backend/PrintAnnot.ml
index 0176224d..995f22dd 100644
--- a/backend/PrintAnnot.ml
+++ b/backend/PrintAnnot.ml
@@ -21,6 +21,13 @@ open AST
 open Memdata
 open Asm
 
+(** 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
+
+
 (** Line number annotations *)
 
 let filename_info : (string, int * Printlines.filebuf option) Hashtbl.t
@@ -66,10 +73,10 @@ let print_file_line oc pref file line =
     | Some fb -> Printlines.copy oc pref fb line line
   end
 
-(* Add file and line debug location, using DWARF1 directives in the style
+(* Add file and line debug location, using DWARF2 directives in the style
    of Diab C 5 *)
 
-let print_file_line_d1 oc pref file line =
+let print_file_line_d2 oc pref file line =
   if !Clflags.option_g && file <> "" then begin
     let (_, filebuf) =
       try
@@ -77,10 +84,10 @@ let print_file_line_d1 oc pref file line =
       with Not_found ->
         enter_filename file in
     if file <> !last_file then begin
-      fprintf oc "	.d1file	%S\n" file;
+      fprintf oc "	.d2file	%S\n" file;
       last_file := file
     end;
-    fprintf oc "	.d1line	%d\n" line;
+    fprintf oc "	.d2line	%d\n" line;
     match filebuf with
     | None -> ()
     | Some fb -> Printlines.copy oc pref fb line line
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index a6883339..11854ace 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -15,6 +15,7 @@ open AST
 open Asm
 open Camlcoq
 open Datatypes
+open DwarfPrinter
 open PrintAsmaux
 open Printf
 open Sections
@@ -23,6 +24,22 @@ 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 print_debug_label oc l =
+      if !Clflags.option_g && Configuration.advanced_debug then
+        fprintf oc "%a:\n" Target.label l
+      else
+        ()
+
+
     let print_location oc loc =
       if loc <> Cutil.no_loc then Target.print_file_line oc (fst loc) (snd loc)
           
@@ -37,16 +54,21 @@ module Printer(Target:TARGET) =
       if not (C2C.atom_is_static name) then
         fprintf oc "	.globl %a\n" Target.symbol name;
       Target.print_optional_fun_info oc;
+      let s,e = if !Clflags.option_g && Configuration.advanced_debug then
+        get_fun_addr name
+      else
+        -1,-1 in
+      print_debug_label oc s;
       fprintf oc "%a:\n" Target.symbol name;
       print_location oc (C2C.atom_location name);
       Target.cfi_startproc oc;
       Target.print_instructions oc fn;
       Target.cfi_endproc oc;
+      print_debug_label oc e;
       Target.print_fun_info oc name;
       Target.emit_constants oc lit;
       Target.print_jumptable oc jmptbl
-        
-
+    
     let print_init_data oc name id =
       if Str.string_match PrintCsyntax.re_string_literal (extern_atom name) 0
           && List.for_all (function Init_int8 _ -> true | _ -> false) id
@@ -87,10 +109,25 @@ module Printer(Target:TARGET) =
       | Gfun (Internal code) -> print_function oc name code
       | Gfun (External ef) ->   ()
       | Gvar v -> print_var oc name v
-            
+
+    module DwarfTarget: DwarfTypes.DWARF_TARGET =
+      struct
+        let label = Target.label
+        let name_of_section = Target.name_of_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 = Hashtbl.find addr_mapping s
+      end
+
+    module DebugPrinter = DwarfPrinter (DwarfTarget) (Target.DwarfAbbrevs)
+      
+     
   end
 
-let print_program oc p =
+let print_program oc p db =
   let module Target = (val (sel_target ()):TARGET) in
   let module Printer = Printer(Target) in
   PrintAnnot.reset_filenames ();
@@ -98,4 +135,11 @@ let print_program oc p =
   Target.print_prologue oc;
   List.iter (Printer.print_globdef oc) p.prog_defs;
   Target.print_epilogue oc;
-  PrintAnnot.close_filenames ()
+  PrintAnnot.close_filenames ();
+  if !Clflags.option_g && Configuration.advanced_debug then
+    begin
+      match db with
+      | None -> ()
+      | Some db ->
+          Printer.DebugPrinter.print_debug oc db
+    end
diff --git a/backend/PrintAsm.mli b/backend/PrintAsm.mli
index eb63f1be..0b2869b0 100644
--- a/backend/PrintAsm.mli
+++ b/backend/PrintAsm.mli
@@ -11,6 +11,4 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-open PrintAsmaux
-
-val print_program: out_channel -> Asm.program -> unit
+val print_program: out_channel -> Asm.program -> DwarfTypes.dw_entry option -> unit
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 64db2cb0..8bc961ef 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -14,6 +14,7 @@
 open AST
 open Asm
 open Camlcoq
+open DwarfTypes
 open Datatypes
 open Printf
 open Sections
@@ -43,6 +44,13 @@ module type TARGET =
       val comment: string
       val symbol: out_channel -> P.t -> unit
       val default_falignment: int
+      val get_start_addr: unit -> int
+      val get_end_addr: unit -> int
+      val get_stmt_list_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 *)
diff --git a/checklink/Check.ml b/checklink/Check.ml
index db0159c4..4924744c 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -75,6 +75,8 @@ let name_of_section_Linux: section_name -> string = function
 | Section_literal -> ".rodata.cst8"
 | Section_jumptable -> ".text"
 | Section_user(s, wr, ex) -> s
+| Section_debug_info -> ".debug_info"
+| Section_debug_abbrev -> ".debug_abbrev"
 
 (** Adapted from CompCert *)
 let name_of_section_Diab: section_name -> string = function
@@ -87,6 +89,8 @@ let name_of_section_Diab: section_name -> string = function
 | Section_literal -> ".text"
 | Section_jumptable -> ".text"
 | Section_user(s, wr, ex) -> s
+| Section_debug_info -> ".debug_info"
+| Section_debug_abbrev -> ".debug_abbrev"
 
 (** Taken from CompCert *)
 let name_of_section: section_name -> string =
diff --git a/common/Sections.ml b/common/Sections.ml
index c6d4c4c2..c0c95848 100644
--- a/common/Sections.ml
+++ b/common/Sections.ml
@@ -27,6 +27,8 @@ type section_name =
   | Section_literal
   | Section_jumptable
   | Section_user of string * bool (*writable*) * bool (*executable*)
+  | Section_debug_info
+  | Section_debug_abbrev
 
 type access_mode =
   | Access_default
diff --git a/common/Sections.mli b/common/Sections.mli
index 38b99db0..e878b9e5 100644
--- a/common/Sections.mli
+++ b/common/Sections.mli
@@ -26,6 +26,8 @@ type section_name =
   | Section_literal
   | Section_jumptable
   | Section_user of string * bool (*writable*) * bool (*executable*)
+  | Section_debug_info
+  | Section_debug_abbrev
 
 type access_mode =
   | Access_default
diff --git a/configure b/configure
index 46dc98da..ffc1d0d3 100755
--- a/configure
+++ b/configure
@@ -19,6 +19,7 @@ toolprefix=''
 target=''
 has_runtime_lib=true
 build_checklink=true
+advanced_debug=false
 
 usage='Usage: ./configure [options] target
 
@@ -113,7 +114,8 @@ case "$target" in
     asm_supports_cfi=false
     clinker="${toolprefix}dcc"
     libmath="-lm"
-    cchecklink=${build_checklink};;
+    cchecklink=${build_checklink}
+    advanced_debug=true;;
   arm*-*)
     arch="arm"
     case "$target" in
@@ -357,6 +359,7 @@ LIBMATH=$libmath
 HAS_RUNTIME_LIB=$has_runtime_lib
 CCHECKLINK=$cchecklink
 ASM_SUPPORTS_CFI=$asm_supports_cfi
+ADVANCED_DEBUG=$advanced_debug
 EOF
 else
 cat >> Makefile.config <<'EOF'
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index deee9f08..9d41f8fa 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -94,6 +94,8 @@ val incomplete_type : Env.t -> typ -> bool
      declared but not defined struct or union, or array type  without a size. *)
 val sizeof_ikind: ikind -> int
   (* Return the size of the given integer kind. *)
+val sizeof_fkind: fkind -> int
+  (* Return the size of the given float kind. *)
 val is_signed_ikind: ikind -> bool
   (* Return true if the given integer kind is signed, false if unsigned. *)
 
diff --git a/cparser/Parse.ml b/cparser/Parse.ml
index 59b04e7a..645465c3 100644
--- a/cparser/Parse.ml
+++ b/cparser/Parse.ml
@@ -17,14 +17,19 @@
 
 module CharSet = Set.Make(struct type t = char let compare = compare end)
 
-let transform_program t p =
+let transform_program t p name =
   let run_pass pass flag p = if CharSet.mem flag t then pass p else p in
-  Rename.program
-  (run_pass StructReturn.program 's'
+  let p1 = (run_pass StructReturn.program 's'
   (run_pass PackedStructs.program 'p'
   (run_pass Bitfields.program 'f'
   (run_pass Unblock.program 'b'
-  p))))
+  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),debug
 
 let parse_transformations s =
   let t = ref CharSet.empty in
@@ -41,7 +46,7 @@ let parse_transformations s =
 let preprocessed_file transfs name sourcefile =
   Cerrors.reset();
   let ic = open_in sourcefile in
-  let p =
+  let p,d =
     try
       let t = parse_transformations transfs in
       let lb = Lexer.init name ic in
@@ -57,9 +62,9 @@ let preprocessed_file transfs name sourcefile =
              | Parser.Parser.Inter.Timeout_pr -> assert false
              | Parser.Parser.Inter.Parsed_pr (ast, _ ) -> ast) in
       let p1 = Timing.time "Elaboration" Elab.elab_file ast in
-      Timing.time2 "Emulations" transform_program t p1
+      Timing.time2 "Emulations" transform_program t p1 name
     with
     | Cerrors.Abort ->
-        [] in
+        [],None in
   close_in ic;
-  if Cerrors.check_errors() then None else Some p
+  if Cerrors.check_errors() then None,None else Some p,d
diff --git a/cparser/Parse.mli b/cparser/Parse.mli
index 58c3cfb9..ac8feb70 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
+val preprocessed_file: string -> string -> string -> C.program option * DwarfTypes.dw_entry option
 
 (* first arg: desired transformations
    second arg: source file name before preprocessing
diff --git a/debug/CtoDwarf.ml b/debug/CtoDwarf.ml
new file mode 100644
index 00000000..b1eea8f3
--- /dev/null
+++ b/debug/CtoDwarf.ml
@@ -0,0 +1,494 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 C
+open Cprint
+open Cutil
+open C2C
+open DwarfTypes
+open DwarfUtil
+open Env
+
+(* 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: (string, int) Hashtbl.t = Hashtbl.create 7
+
+(* Get the type id of a composite_type *)
+let get_composite_type (name: string): 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 size_to_subrange s =
+    let b = (match s with 
+    | None -> None
+    | Some i ->
+        let i = Int64.to_int i in
+        Some (BoundConst i)) in
+    let s = {
+      subrange_type = None;
+      subrange_upper_bound = b;
+    } in
+    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,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 (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.name 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 =
+  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 (n,t) gloc =
+  let i,t = type_to_dwarf t in
+  Hashtbl.add typedef_table n.name i;
+  let td = {
+    typedef_file_loc = Some (gloc);
+    typedef_name = n.name;
+    typedef_type = i;
+  } in 
+  let td = new_entry (DW_TAG_typedef td) in
+  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 at_decl = (match s with
+   | Storage_extern -> true
+   | _ -> false) in
+   let ext = (match s with
+   | Storage_static -> false
+   | _ -> true) in
+   let decl = {
+     variable_file_loc = (Some gloc);
+     variable_declaration = Some at_decl;
+     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 = Some false;
+    enumeration_name = n.name;
+  } in
+  let id = get_composite_type n.name 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 = Some false;
+    structure_name = n.name;
+  } in
+  let id = get_composite_type n.name 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 = m.fld_name;
+                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 = m.fld_name;
+              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
+  sou::e
+
+(* 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 = Some false;
+    union_name = n.name;
+  } in
+  let id = get_composite_type n.name 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 = f.fld_name;
+          member_type = t;
+        } in
+        new_entry (DW_TAG_member um),e@acc)[] m in
+  let sou = {
+    tag = tag;
+    children = children;
+    id = id;} in
+  sou::e
+
+(* Translate global declarations to there dwarf representation *)
+let globdecl_to_dwarf env (typs,decls) decl =
+  PrintAnnot.add_file (fst decl.gloc);
+  match decl.gdesc with
+  | Gtypedef (n,t) -> let ret = typedef_to_dwarf (n,t) decl.gloc 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) ->let ret = enum_to_dwarf (n,at,e) decl.gloc in
+    typs@ret,decls
+  | Gcompositedef (Struct,n,at,m) -> let ret = struct_to_dwarf (n,at,m) env decl.gloc in
+    typs@ret,decls
+  | Gcompositedef (Union,n,at,m) -> let ret = union_to_dwarf (n,at,m) env decl.gloc in
+    typs@ret,decls
+  | Gcompositedecl _
+  | Gpragma _ -> typs,decls       
+
+(* 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,defs = List.fold_left (globdecl_to_dwarf env) ([],[]) prog 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/DwarfPrinter.ml b/debug/DwarfPrinter.ml
new file mode 100644
index 00000000..dec3279e
--- /dev/null
+++ b/debug/DwarfPrinter.ml
@@ -0,0 +1,502 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.                                                 *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Printer for the Dwarf 2 debug information in ASM *)
+
+open DwarfTypes
+open DwarfUtil
+open Printf
+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):
+    sig
+      val print_debug: out_channel -> dw_entry -> unit
+    end =
+  struct
+
+    open Target
+    open DwarfAbbrevs
+
+    (* Byte value to string *)
+    let string_of_byte value =
+      sprintf "	.byte		%s\n" (if value then "0x1" else "0x0")
+
+    (* Print a label *)
+    let print_label oc lbl =
+      fprintf oc "%a:\n" label lbl
+
+    (* Helper functions for abbreviation printing *)
+    let add_byte buf value =
+      Buffer.add_string buf (string_of_byte value)
+
+    let add_abbr_uleb v buf =
+      Buffer.add_string buf (Printf.sprintf "	.uleb128	%d\n" v)
+
+    let add_abbr_entry (v1,v2) buf =
+      add_abbr_uleb v1 buf;
+      add_abbr_uleb v2 buf
+
+    let add_file_loc buf =
+      let file,line = file_loc_type_abbr in
+      add_abbr_entry (0x3a,file) buf;
+      add_abbr_entry (0x3b,line) buf
+
+    let add_type = add_abbr_entry (0x49,type_abbr)
+
+    let add_name = add_abbr_entry (0x3,name_type_abbr)
+
+    let add_byte_size = add_abbr_entry (0xb,byte_size_type_abbr)
+
+    let add_high_pc = add_abbr_entry (0x12,high_pc_type_abbr)
+
+    let add_low_pc = add_abbr_entry (0x11,low_pc_type_abbr)
+
+    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
+
+    (* Dwarf entity to string function *)
+    let abbrev_string_of_entity entity has_sibling =
+      let buf = Buffer.create 12 in
+      let add_attr_some v f =
+        match v with
+        | None -> ()
+        | Some _ -> f buf in
+      let prologue id =
+        let has_child = match entity.children with
+        | [] -> false
+        | _ -> true in
+        add_abbr_uleb id buf;
+        add_byte buf has_child;
+        if has_sibling then add_abbr_entry (0x1,sibling_type_abbr) buf;
+      in
+      (match entity.tag with
+      | DW_TAG_array_type e ->
+          prologue 0x1;
+          add_attr_some e.array_type_file_loc add_file_loc;
+          add_type buf
+      | DW_TAG_base_type b ->
+          prologue 0x24;
+          add_byte_size buf;
+          add_attr_some b.base_type_encoding (add_abbr_entry (0x3e,encoding_type_abbr));
+          add_name buf
+      | 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_abbr_entry (0x13,language_type_abbr) buf;
+          add_name buf;
+          add_abbr_entry (0x25,producer_type_abbr) buf;
+          add_abbr_entry (0x10,stmt_list_type_abbr) buf;
+      | DW_TAG_const_type _ ->
+          prologue 0x26;
+          add_type buf
+      | DW_TAG_enumeration_type e ->
+          prologue 0x4;
+          add_attr_some e.enumeration_file_loc add_file_loc;
+          add_byte_size buf;
+          add_attr_some e.enumeration_declaration add_declaration;
+          add_name buf
+      | DW_TAG_enumerator e ->
+          prologue 0x28;
+          add_attr_some e.enumerator_file_loc add_file_loc;
+          add_abbr_entry (0x1c,value_type_abbr) buf;
+          add_name buf
+      | DW_TAG_formal_parameter e ->
+          prologue 0x34;
+          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))
+      | DW_TAG_label _ ->
+          prologue 0xa;
+          add_low_pc buf;
+          add_name buf;
+      | DW_TAG_lexical_block _ ->
+          prologue 0xb;
+          add_high_pc buf;
+          add_low_pc buf
+      | DW_TAG_member e ->
+          prologue 0xd;
+          add_attr_some e.member_file_loc add_file_loc;
+          add_attr_some e.member_byte_size add_byte_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));
+          (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_name buf;
+          add_type buf
+      | DW_TAG_pointer_type _ ->
+          prologue 0xf;
+          add_type buf
+      | DW_TAG_structure_type e ->
+          prologue 0x13;
+          add_attr_some e.structure_file_loc add_file_loc;
+          add_attr_some e.structure_byte_size add_byte_size;
+          add_attr_some e.structure_declaration add_declaration;
+          add_name buf
+      | DW_TAG_subprogram e ->
+          prologue 0x2e;
+          add_attr_some e.subprogram_file_loc add_file_loc;
+          add_attr_some e.subprogram_external (add_abbr_entry (0x3f,external_type_abbr));
+          add_high_pc buf;
+          add_low_pc buf;
+          add_name buf;
+          add_abbr_entry (0x27,prototyped_type_abbr) buf;
+          add_attr_some e.subprogram_type add_type;
+      | DW_TAG_subrange_type e ->
+          prologue 0x21;
+          add_attr_some e.subrange_type add_type;
+          (match e.subrange_upper_bound with
+          | None -> ()
+          | Some (BoundConst _) -> add_abbr_entry (0x2f,bound_const_type_abbr) buf
+          | Some (BoundRef _) -> add_abbr_entry (0x2f,bound_ref_type_abbr) buf)
+      | DW_TAG_subroutine_type e ->
+          prologue 0x15;
+          add_attr_some e.subroutine_type add_type;
+          add_abbr_entry (0x27,prototyped_type_abbr) buf
+      | DW_TAG_typedef e ->
+          prologue 0x16;
+          add_attr_some e.typedef_file_loc add_file_loc;
+          add_name buf;
+          add_type buf
+      | DW_TAG_union_type e ->
+          prologue 0x17;
+          add_attr_some e.union_file_loc add_file_loc;
+          add_attr_some e.union_byte_size add_byte_size;
+          add_attr_some e.union_declaration add_declaration;
+          add_name buf
+      | DW_TAG_unspecified_parameter e ->
+          prologue 0x18;
+          add_attr_some e.unspecified_parameter_file_loc add_file_loc;
+          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_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;
+          add_type buf);
+      Buffer.contents buf
+
+    let abbrev_start_addr = ref (-1)
+
+    let curr_abbrev = ref 1
+
+    (* Function to get unique abbreviation ids *)
+    let next_abbrev () =
+      let abbrev = !curr_abbrev in
+      incr curr_abbrev;abbrev
+
+    (* Mapping from abbreviation string to abbrevaiton id *)
+    let abbrev_mapping: (string,int) Hashtbl.t = Hashtbl.create 7
+
+    (* Look up the id of the abbreviation and add it if it is missing *)
+    let get_abbrev entity has_sibling =
+      let abbrev_string = abbrev_string_of_entity entity has_sibling in
+      (try
+        Hashtbl.find abbrev_mapping abbrev_string
+      with Not_found ->
+        let id = next_abbrev () in
+        Hashtbl.add abbrev_mapping abbrev_string id;
+        id)
+
+    (* Compute the abbreviations of an entry and its children *)
+    let compute_abbrev entry =
+      entry_iter_sib (fun sib entry ->
+        let has_sib = match sib with
+        | None -> false
+        | Some _ -> true in
+        ignore (get_abbrev entry has_sib)) (fun _ -> ()) entry
+
+    (* Print the debug_abbrev section using the previous computed abbreviations*)
+    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);
+      let lbl = new_label () in
+      abbrev_start_addr := lbl;
+      print_label oc lbl;
+      List.iter (fun (s,id) ->
+        fprintf oc "	.uleb128	%d\n" id;
+        output_string oc s;
+        fprintf oc "	.uleb128	0\n";
+        fprintf oc "	.uleb128	0\n")  abbrevs;
+      fprintf oc "	.sleb128	0\n"
+
+    let debug_start_addr = ref (-1)
+
+    let entry_labels: (int,int) Hashtbl.t = Hashtbl.create 7
+
+    (* Translate the ids to address labels *)
+    let entry_to_label id =
+      try
+        Hashtbl.find entry_labels id
+      with Not_found ->
+        let label = new_label () in
+        Hashtbl.add entry_labels id label;
+        label
+
+    (* Helper functions for debug printing *)
+    let print_opt_value oc o f =
+      match o with
+      | 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)
+
+    let print_string oc s =
+      fprintf oc "	.asciz		\"%s\"\n" s
+
+    let print_uleb128 oc d =
+      fprintf oc "	.uleb128	%d\n" d
+
+    let print_sleb128 oc d =
+      fprintf oc "	.sleb128	%d\n" d
+
+    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_ref oc r =
+      let ref = entry_to_label r in
+      fprintf oc "	.4byte		%a\n" label ref
+
+    let print_addr oc a =
+      fprintf oc "	.4byte		%a\n" label a
+
+    let print_array_type oc at =
+      print_file_loc oc at.array_type_file_loc;
+      print_ref oc at.array_type
+
+    let print_bound_value oc = function
+      | BoundConst bc -> print_uleb128 oc bc
+      | BoundRef br -> print_ref oc br
+
+    let print_base_type oc bt =
+      print_byte oc bt.base_type_byte_size;
+      (match bt.base_type_encoding with
+      | Some e ->
+          let encoding = match e with
+          | DW_ATE_address -> 0x1
+          | DW_ATE_boolean -> 0x2
+          | DW_ATE_complex_float -> 0x3
+          | DW_ATE_float -> 0x4
+          | DW_ATE_signed -> 0x5
+          | DW_ATE_signed_char -> 0x6
+          | DW_ATE_unsigned -> 0x7
+          | DW_ATE_unsigned_char -> 0x8
+          in
+          print_byte oc encoding;
+      | None -> ());
+      print_string oc bt.base_type_name
+
+    let print_compilation_unit oc tag =
+      print_string oc (Sys.getcwd ());
+      print_addr oc (get_start_addr ());
+      print_addr oc (get_end_addr ());
+      print_uleb128 oc 1;
+      print_string oc tag.compile_unit_name;
+      print_string oc ("CompCert "^Configuration.version);
+      print_addr oc (get_stmt_list_addr ())
+
+    let print_const_type oc ct =
+      print_ref oc ct.const_type
+
+    let print_enumeration_type oc et =
+      print_file_loc oc et.enumeration_file_loc;
+      print_uleb128 oc et.enumeration_byte_size;
+      print_opt_value oc et.enumeration_declaration print_flag;
+      print_string oc et.enumeration_name
+
+    let print_enumerator oc en =
+      print_file_loc oc en.enumerator_file_loc;
+      print_sleb128 oc en.enumerator_value;
+      print_string oc en.enumerator_name
+
+    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
+
+    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
+
+    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_string oc mb.member_name;
+      print_ref oc mb.member_type
+
+    let print_pointer oc pt =
+      print_ref oc pt.pointer_type
+
+    let print_structure oc st =
+      print_file_loc oc st.structure_file_loc;
+      print_opt_value oc st.structure_byte_size print_uleb128;
+      print_opt_value oc st.structure_declaration print_flag;
+      print_string oc st.structure_name
+
+    let print_subprogram oc sp =
+      let s,e = get_fun_addr sp.subprogram_name in
+      print_file_loc oc sp.subprogram_file_loc;
+      print_opt_value oc sp.subprogram_external print_flag;
+      print_opt_value oc sp.subprogram_frame_base print_loc;
+      fprintf oc "	.4byte		%a\n" label s;
+      fprintf oc "	.4byte		%a\n" label e;
+      print_string oc sp.subprogram_name;
+      print_flag oc sp.subprogram_prototyped;
+      print_opt_value oc sp.subprogram_type print_ref
+
+    let print_subrange oc sr =
+      print_opt_value oc sr.subrange_type print_ref;
+      print_opt_value oc sr.subrange_upper_bound print_bound_value
+
+    let print_subroutine oc st =
+      print_opt_value oc st.subroutine_type print_ref;
+      print_flag oc st.subroutine_prototyped
+
+    let print_typedef oc td =
+      print_file_loc oc td.typedef_file_loc;
+      print_string oc td.typedef_name;
+      print_ref oc td.typedef_type
+
+    let print_union_type oc ut =
+      print_file_loc oc ut.union_file_loc;
+      print_opt_value oc ut.union_byte_size print_uleb128;
+      print_opt_value oc ut.union_declaration print_flag;
+      print_string oc ut.union_name
+
+    let print_unspecified_parameter oc up =
+      print_file_loc oc up.unspecified_parameter_file_loc;
+      print_opt_value oc up.unspecified_parameter_artificial print_flag
+
+    let print_variable oc var =
+      print_file_loc oc 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 =
+      print_ref oc vt.volatile_type
+
+    (* Print an debug entry *)
+    let  print_entry oc entry =
+      entry_iter_sib (fun sib entry ->
+        print_label oc (entry_to_label entry.id);
+        let has_sib = match sib with
+        | None -> false
+        | Some _ -> true in
+        let id = get_abbrev entry has_sib in
+        print_sleb128 oc id;
+        (match sib with
+        | None -> ()
+        | Some s -> let lbl = entry_to_label s in
+          fprintf oc "	.4byte		%a-%a\n" label lbl label !debug_start_addr);
+        begin
+          match entry.tag with
+          | DW_TAG_array_type arr_type -> print_array_type oc arr_type
+          | DW_TAG_compile_unit comp -> print_compilation_unit oc comp
+          | DW_TAG_base_type bt -> print_base_type oc bt
+          | DW_TAG_const_type ct -> print_const_type oc ct
+          | DW_TAG_enumeration_type et -> print_enumeration_type oc et
+          | DW_TAG_enumerator et -> print_enumerator oc et
+          | DW_TAG_formal_parameter fp -> print_formal_parameter oc fp
+          | DW_TAG_label lb -> print_tag_label oc lb
+          | DW_TAG_lexical_block lb -> print_lexical_block oc lb
+          | DW_TAG_member mb -> print_member oc mb
+          | DW_TAG_pointer_type pt -> print_pointer oc pt
+          | DW_TAG_structure_type st -> print_structure oc st
+          | DW_TAG_subprogram sb -> print_subprogram oc sb
+          | DW_TAG_subrange_type sb -> print_subrange oc sb
+          | DW_TAG_subroutine_type st -> print_subroutine oc st
+          | DW_TAG_typedef tp -> print_typedef oc tp
+          | DW_TAG_union_type ut -> print_union_type oc ut
+          | DW_TAG_unspecified_parameter up -> print_unspecified_parameter oc up
+          | DW_TAG_variable var -> print_variable oc var
+          | DW_TAG_volatile_type vt -> print_volatile_type oc vt
+        end) (fun e ->
+          if e.children <> [] then
+          print_sleb128 oc 0) entry
+
+    (* Print the debug abbrev section *)
+    let print_debug_abbrev oc entry =
+      compute_abbrev entry;
+      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 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;
+      print_label oc debug_length_start;
+      fprintf oc "	.2byte		0x2\n"; (* Dwarf version *)
+      print_addr oc !abbrev_start_addr; (* Offset into the abbreviation *)
+      print_byte oc !Machine.config.Machine.sizeof_ptr; (* Sizeof pointer type *)
+      print_entry oc entry;
+      print_sleb128 oc 0;
+      print_label oc debug_end (* End of the debug section *)
+
+
+    (* Print the debug info and abbrev section *)
+    let print_debug oc entry =
+      print_debug_abbrev oc entry;
+      print_debug_info oc entry
+
+  end
diff --git a/debug/DwarfPrinter.mli b/debug/DwarfPrinter.mli
new file mode 100644
index 00000000..9e0e6693
--- /dev/null
+++ b/debug/DwarfPrinter.mli
@@ -0,0 +1,18 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 DwarfTypes
+
+module DwarfPrinter: functor (Target: DWARF_TARGET) -> functor (DwarfAbbrevs: DWARF_ABBREVS) ->
+  sig
+    val print_debug: out_channel -> dw_entry -> unit
+  end
diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli
new file mode 100644
index 00000000..c02558b5
--- /dev/null
+++ b/debug/DwarfTypes.mli
@@ -0,0 +1,272 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.                                                 *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Types used for writing dwarf debug information *)
+
+open Sections
+
+(* Basic types for the value of attributes *)
+
+type constant = int
+
+type flag = bool
+
+type reference = int
+
+type encoding =
+  | DW_ATE_address
+  | DW_ATE_boolean
+  | DW_ATE_complex_float
+  | DW_ATE_float
+  | DW_ATE_signed
+  | DW_ATE_signed_char
+  | DW_ATE_unsigned
+  | DW_ATE_unsigned_char
+
+type address = int
+
+type block = string
+
+type location_value =
+  | LocConst of constant
+  | LocBlock of block
+
+type data_location_value =
+  | DataLocBlock of block
+  | DataLocRef of reference
+
+type bound_value =
+  | BoundConst of constant
+  | BoundRef of reference
+
+(* Types representing the attribute information per tag value *)
+
+type file_loc = string * constant
+
+type dw_tag_array_type =
+    {
+     array_type_file_loc: file_loc option;
+     array_type:          reference;
+   }
+
+type dw_tag_base_type =
+    {
+     base_type_byte_size: constant;
+     base_type_encoding:  encoding option;
+     base_type_name:      string;
+   }
+
+type dw_tag_compile_unit =
+    {
+     compile_unit_name:            string;
+   }
+
+type dw_tag_const_type =
+    {
+     const_type: reference;
+   }
+
+type dw_tag_enumeration_type =
+    {
+     enumeration_file_loc:    file_loc  option;
+     enumeration_byte_size:   constant;
+     enumeration_declaration: flag      option;
+     enumeration_name:        string;
+   }
+
+type dw_tag_enumerator =
+    {
+     enumerator_file_loc: file_loc option;
+     enumerator_value:    constant;
+     enumerator_name:     string;
+   }
+
+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;
+   }
+
+type dw_tag_label =
+    {
+     label_low_pc: address;
+     label_name:   string;
+   }
+
+type dw_tag_lexical_block =
+    {
+     lexical_block_high_pc: address;
+     lexical_block_low_pc:  address;
+   }
+
+type dw_tag_member =
+    {
+     member_file_loc:             file_loc            option;
+     member_byte_size:            constant            option;
+     member_bit_offset:           constant            option;
+     member_bit_size:             constant            option;
+     member_data_member_location: data_location_value option;
+     member_declaration:          flag                option;
+     member_name:                 string;
+     member_type:                 reference;
+   }
+
+type dw_tag_pointer_type =
+    {
+     pointer_type: reference;
+   }
+
+type dw_tag_structure_type =
+    {
+     structure_file_loc:    file_loc option;
+     structure_byte_size:   constant option;
+     structure_declaration: flag     option;
+     structure_name:        string;
+   }
+
+type dw_tag_subprogram =
+    {
+     subprogram_file_loc:   file_loc       option;
+     subprogram_external:   flag           option;
+     subprogram_frame_base: location_value option;
+     subprogram_name:       string;
+     subprogram_prototyped: flag;
+     subprogram_type:       reference      option;
+   }
+
+type dw_tag_subrange_type =
+    {
+     subrange_type:        reference   option;
+     subrange_upper_bound: bound_value option;
+   }
+
+type dw_tag_subroutine_type =
+    {
+     subroutine_type:       reference option;
+     subroutine_prototyped: flag;
+   }
+
+type dw_tag_typedef =
+    {
+     typedef_file_loc: file_loc option;
+     typedef_name:     string;
+     typedef_type:     reference;
+   }
+
+type dw_tag_union_type =
+    {
+     union_file_loc:    file_loc option;
+     union_byte_size:   constant option;
+     union_declaration: flag     option;
+     union_name:        string;
+   }
+
+type dw_tag_unspecified_parameter =
+    {
+     unspecified_parameter_file_loc:   file_loc option;
+     unspecified_parameter_artificial: flag     option;
+   }
+
+type dw_tag_variable =
+    {
+     variable_file_loc:    file_loc       option;
+     variable_declaration: flag           option;
+     variable_external:    flag           option;
+     variable_location:    location_value option;
+     variable_name:        string;
+     variable_segment:     location_value option;
+     variable_type:        reference;
+   }
+
+type dw_tag_volatile_type =
+    {
+     volatile_type: reference;
+   }
+
+type dw_tag =
+  | DW_TAG_array_type of dw_tag_array_type
+  | DW_TAG_base_type of dw_tag_base_type
+  | DW_TAG_compile_unit of dw_tag_compile_unit
+  | DW_TAG_const_type of dw_tag_const_type
+  | DW_TAG_enumeration_type of dw_tag_enumeration_type
+  | DW_TAG_enumerator of dw_tag_enumerator
+  | DW_TAG_formal_parameter of dw_tag_formal_parameter
+  | DW_TAG_label of dw_tag_label
+  | DW_TAG_lexical_block of dw_tag_lexical_block
+  | DW_TAG_member of dw_tag_member
+  | DW_TAG_pointer_type of dw_tag_pointer_type
+  | DW_TAG_structure_type of dw_tag_structure_type
+  | DW_TAG_subprogram of dw_tag_subprogram
+  | DW_TAG_subrange_type of dw_tag_subrange_type
+  | DW_TAG_subroutine_type of dw_tag_subroutine_type
+  | DW_TAG_typedef of dw_tag_typedef
+  | DW_TAG_union_type of dw_tag_union_type
+  | DW_TAG_unspecified_parameter of dw_tag_unspecified_parameter
+  | DW_TAG_variable of dw_tag_variable
+  | DW_TAG_volatile_type of dw_tag_volatile_type
+
+(* The type of the entries. *)
+
+type dw_entry =
+    {
+     tag:      dw_tag;
+     children: dw_entry list;
+     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 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 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
+  end
diff --git a/debug/DwarfUtil.ml b/debug/DwarfUtil.ml
new file mode 100644
index 00000000..e2c87a9d
--- /dev/null
+++ b/debug/DwarfUtil.ml
@@ -0,0 +1,118 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.                                                 *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Utility functions for the dwarf debuging type *)
+
+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
+  {
+   tag = tag;
+   children = [];
+   id = id;
+ }
+
+(* Add an entry as child to  another entry *)
+let add_child entry child =
+  {entry with children = child::entry.children;}
+
+
+(* Add entries as children to  another entry *)
+let add_children entry children =
+  {entry with children = entry.children@children;}
+
+
+let list_iter_with_next f list =
+  let rec aux = (function
+    | [] -> ()
+    | [a] -> f None a
+    | a::b::rest -> f (Some b.id) a; aux (b::rest)) in
+  aux list
+
+(* Iter over the tree and pass the sibling id *)
+let entry_iter_sib f g entry =
+  let rec aux sib entry =
+    f sib entry;
+    list_iter_with_next aux entry.children;
+    g entry in
+  aux None entry
+
+
+(* Fold over the tree in prefix order *)
+let rec entry_fold f acc entry =
+  let acc = f acc entry.tag in
+  List.fold_left (entry_fold f) acc entry.children
+
+(* Attribute form encoding *)
+let dw_form_addr     = 0x01
+let dw_form_block2   = 0x03
+let dw_form_block4   = 0x04
+let dw_form_data2    = 0x05
+let dw_form_data4    = 0x06
+let dw_form_data8    = 0x07
+let dw_form_string   = 0x08
+let dw_form_block    = 0x09
+let dw_form_block1   = 0x0a
+let dw_form_data1    = 0x0b
+let dw_form_flag     = 0x0c
+let dw_form_sdata    = 0x0d
+let dw_form_strp     = 0x0e
+let dw_form_udata    = 0x0f
+let dw_form_ref_addr = 0x10
+let dw_form_ref1     = 0x11
+let dw_form_ref2     = 0x12
+let dw_form_ref4     = 0x13
+let dw_form_ref8     = 0x14
+let dw_ref_udata     = 0x15
+let dw_ref_indirect  = 0x16
+
+(* 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 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
diff --git a/driver/Configuration.ml b/driver/Configuration.ml
index 237085de..2cea2b80 100644
--- a/driver/Configuration.ml
+++ b/driver/Configuration.ml
@@ -93,6 +93,12 @@ let asm_supports_cfi =
   | "false" -> false
   | v -> bad_config "asm_supports_cfi" [v]
 
+let advanced_debug =
+  match get_config_string "advanced_debug" with
+  | "true" -> true
+  | "false" -> false
+  | v -> bad_config "advanced_debug" [v]
+
 let version = get_config_string "version"
 
 type struct_passing_style =
diff --git a/driver/Configuration.mli b/driver/Configuration.mli
index 875bd692..20c45518 100644
--- a/driver/Configuration.mli
+++ b/driver/Configuration.mli
@@ -31,6 +31,8 @@ val stdlib_path: string
   (** Path to CompCert's library *)
 val has_runtime_lib: bool
   (** True if CompCert's library is available. *)
+val advanced_debug: bool
+  (** True if advanced debug is implement for the Target *)
 
 val version: string
   (** CompCert version string *)
diff --git a/driver/Driver.ml b/driver/Driver.ml
index ad7cf61e..d225ec4f 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -117,17 +117,17 @@ let parse_c_file sourcename ifile =
   ^ (if !option_fpacked_structs then "p" else "")
   in
   (* Parsing and production of a simplified C AST *)
-  let ast =
+  let ast,debug =
     match Parse.preprocessed_file simplifs sourcename ifile with
-    | None -> exit 2
-    | Some p -> p in
+    | None,_ -> exit 2
+    | Some p,d -> p,d in
   (* Save C AST if requested *)
   if !option_dparse then begin
     let ofile = output_filename sourcename ".c" ".parsed.c" in
     let oc = open_out ofile in
     Cprint.program (Format.formatter_of_out_channel oc) ast;
     close_out oc
-  end;
+  end; 
   (* Conversion to Csyntax *)
   let csyntax =
     match Timing.time "CompCert C generation" C2C.convertProgram ast with
@@ -141,7 +141,7 @@ let parse_c_file sourcename ifile =
     PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax;
     close_out oc
   end;
-  csyntax
+  csyntax,debug
 
 (* Dump Asm code in binary format for the validator *)
 
@@ -157,7 +157,7 @@ let dump_asm asm destfile =
 
 (* From CompCert C AST to asm *)
 
-let compile_c_ast sourcename csyntax ofile =
+let compile_c_ast sourcename csyntax ofile debug =
   (* Prepare to dump Clight, RTL, etc, if requested *)
   let set_dest dst opt ext =
     dst := if !opt then Some (output_filename sourcename ".c" ext)
@@ -181,13 +181,14 @@ let compile_c_ast sourcename csyntax ofile =
     dump_asm asm (output_filename sourcename ".c" ".sdump");
   (* Print Asm in text form *)
   let oc = open_out ofile in
-  PrintAsm.print_program oc asm;
+  PrintAsm.print_program oc asm debug;
   close_out oc
 
 (* From C source to asm *)
 
 let compile_c_file sourcename ifile ofile =
-  compile_c_ast sourcename (parse_c_file sourcename ifile) ofile
+  let ast,debug = parse_c_file sourcename ifile in
+  compile_c_ast sourcename ast ofile debug
 
 (* From Cminor to asm *)
 
@@ -212,7 +213,7 @@ let compile_cminor_file ifile ofile =
         exit 2
     | Errors.OK p ->
         let oc = open_out ofile in
-        PrintAsm.print_program oc p;
+        PrintAsm.print_program oc p None;
         close_out oc
   with Parsing.Parse_error ->
          eprintf "File %s, character %d: Syntax error\n"
@@ -266,7 +267,7 @@ let process_c_file sourcename =
     preprocess sourcename preproname;
     if !option_interp then begin
       Machine.config := Machine.compcert_interpreter !Machine.config;
-      let csyntax = parse_c_file sourcename preproname in
+      let csyntax,_ = parse_c_file sourcename preproname in
       safe_remove preproname;
       Interp.execute csyntax;
       ""
@@ -293,7 +294,7 @@ let process_c_file sourcename =
 
 let process_i_file sourcename =
   if !option_interp then begin
-    let csyntax = parse_c_file sourcename sourcename in
+    let csyntax,_ = parse_c_file sourcename sourcename in
     Interp.execute csyntax;
     ""
   end else if !option_S then begin
@@ -514,7 +515,7 @@ let cmdline_actions =
   Exact "-fall", Self (fun _ -> set_all language_support_options);
   Exact "-fnone", Self (fun _ -> unset_all language_support_options);
 (* Debugging options *)
-  Exact "-g", Self (fun s -> option_g := true; push_linker_arg s);
+  Exact "-g", Self (fun s -> option_g := true);
 (* Code generation options -- more below *)
   Exact "-O0", Self (fun _ -> unset_all optimization_options);
   Exact "-O", Self (fun _ -> set_all optimization_options);
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
index cb4905ef..92be0ff3 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -983,6 +983,19 @@ module Target(System: SYSTEM):TARGET =
     let comment = comment
 
     let default_falignment = 16
+
+    let get_start_addr () = -1 (* Dummy constant *)
+        
+    let get_end_addr () = -1 (* Dummy constant *)
+
+    let get_stmt_list_addr () = -1 (* Dummy constant *)
+
+    module DwarfAbbrevs = DwarfUtil.DefaultAbbrevs (* Dummy Abbrev types *)
+
+    let label = label
+       
+    let new_label = new_label
+
 end
 
 let sel_target () =
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 7e460f46..b3d228b3 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -38,6 +38,8 @@ module type SYSTEM =
       val cfi_adjust: out_channel -> int32 -> unit
       val cfi_rel_offset: out_channel -> string -> int32 -> unit
       val print_prologue: out_channel -> unit
+      val print_epilogue: out_channel -> unit
+      val print_file_loc: out_channel -> DwarfTypes.file_loc -> unit
     end
 
 let symbol = elf_symbol
@@ -68,6 +70,14 @@ let float_reg_name = function
   | FPR24 -> "24" | FPR25 -> "25" | FPR26 -> "26" | FPR27 -> "27"
   | FPR28 -> "28" | FPR29 -> "29" | FPR30 -> "30" | FPR31 -> "31"
 
+let start_addr = ref (-1)
+
+let end_addr = ref (-1)
+
+let stmt_list_addr = ref (-1)
+
+let label = elf_label
+
 module Linux_System : SYSTEM =
   struct
 
@@ -117,6 +127,9 @@ 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_abbrev -> ".debug_abbrev,\"\",@progbits"
+
 
     let print_file_line oc file line =
       PrintAnnot.print_file_line oc comment file line
@@ -131,6 +144,10 @@ module Linux_System : SYSTEM =
     let cfi_rel_offset = cfi_rel_offset
 
     let print_prologue oc = ()
+
+    let print_epilogue oc = ()
+
+    let print_file_loc _ _ = ()
   
   end
     
@@ -182,9 +199,11 @@ 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"
 
     let print_file_line oc file line =
-      PrintAnnot.print_file_line_d1 oc comment file line
+      PrintAnnot.print_file_line_d2 oc comment file line
 
     (* Emit .cfi directives *)
     let cfi_startproc oc = ()
@@ -198,8 +217,39 @@ module Diab_System : SYSTEM =
     let print_prologue oc =
       fprintf oc "	.xopt	align-fill-text=0x60000000\n";
       if !Clflags.option_g then
-        fprintf oc "	.xopt	asm-debug-on\n"
-  
+        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 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";
+          PrintAnnot.StringSet.iter (fun file ->
+            let label = new_label () in
+            Hashtbl.add filenum file label;
+            fprintf oc ".L%d:	.d2filenum \"%s\"\n" label file) !PrintAnnot.all_files;
+          fprintf oc "	.d2_line_end\n"
+        end
+
+    let print_file_loc oc (file,col) =
+      fprintf oc "	.4byte		%a\n" label (Hashtbl.find filenum file);
+      fprintf oc "	.uleb128	%d\n" col
   end
 
 module Target (System : SYSTEM):TARGET =
@@ -212,7 +262,7 @@ module Target (System : SYSTEM):TARGET =
     let raw_symbol oc s =
       fprintf oc "%s" s
 
-    let label = elf_label
+    let label = label
 
     let label_low oc lbl =
       fprintf oc ".L%d@l" lbl
@@ -729,8 +779,6 @@ module Target (System : SYSTEM):TARGET =
     let print_align oc align  =
       fprintf oc "	.balign	%d\n" align
 
-    let print_epilogue _ = ()
-
     let print_jumptable oc jmptbl = 
       let print_jumptable oc (lbl, tbl) =
         fprintf oc "%a:" label lbl;
@@ -745,6 +793,17 @@ module Target (System : SYSTEM):TARGET =
       end
 
     let default_falignment = 4
+        
+    let get_start_addr () = !start_addr
+
+    let get_end_addr () = !end_addr
+
+    let get_stmt_list_addr () = !stmt_list_addr
+
+    module DwarfAbbrevs = DwarfUtil.DefaultAbbrevs
+
+    let new_label = new_label
+
   end
 
 let sel_target () =