Merge branch 'gnu-debug'

Conflicts:
	debug/DebugInformation.ml

11 files changed, 255 insertions, 149 deletions

diff --git a/backend/Fileinfo.ml b/backend/Fileinfo.ml
new file mode 100644
index 00000000..afdea382
--- /dev/null
+++ b/backend/Fileinfo.ml
@@ -0,0 +1,79 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*          Bernhard Schommer, AbsInt Angewandte Informatik GmbH       *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+open Printf
+
+(* Printing annotations in asm syntax *)
+
+let filename_info : (string, int * Printlines.filebuf option) Hashtbl.t
+                  = Hashtbl.create 7
+
+let last_file = ref ""
+
+let reset_filenames () =
+  Hashtbl.clear filename_info; last_file := ""
+
+let close_filenames () =
+  Hashtbl.iter
+    (fun file (num, fb) ->
+       match fb with Some b -> Printlines.close b | None -> ())
+    filename_info;
+  reset_filenames()
+
+let enter_filename f =
+  let num = Hashtbl.length filename_info + 1 in
+  let filebuf =
+    if !Clflags.option_S || !Clflags.option_dasm then begin
+      try Some (Printlines.openfile f)
+      with Sys_error _ -> None
+    end else None in
+  Hashtbl.add filename_info f (num, filebuf);
+  (num, filebuf)
+
+(* Add file and line debug location, using GNU assembler-style DWARF2
+   directives *)
+
+let print_file_line oc pref file line =
+  if !Clflags.option_g && file <> "" then begin
+    let (filenum, filebuf) =
+      try
+        Hashtbl.find filename_info file
+      with Not_found ->
+        let (filenum, filebuf as res) = enter_filename file in
+        fprintf oc "	.file	%d %S\n" filenum file;
+        res in
+    fprintf oc "	.loc	%d %d\n" filenum line;
+    match filebuf with
+    | None -> ()
+    | Some fb -> Printlines.copy oc pref fb line line
+  end
+
+(* Add file and line debug location, using DWARF2 directives in the style
+   of Diab C 5 *)
+
+let print_file_line_d2 oc pref file line =
+  if !Clflags.option_g && file <> "" then begin
+    let (_, filebuf) =
+      try
+        Hashtbl.find filename_info file
+      with Not_found ->
+        enter_filename file in
+    if file <> !last_file then begin
+      fprintf oc "	.d2file	%S\n" file;
+      last_file := file
+    end;
+    fprintf oc "	.d2line	%d\n" line;
+    match filebuf with
+    | None -> ()
+    | Some fb -> Printlines.copy oc pref fb line line
+  end
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index dba578b9..594b43b7 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -122,12 +122,11 @@ module Printer(Target:TARGET) =
 let print_program oc p db =
   let module Target = (val (sel_target ()):TARGET) in
   let module Printer = Printer(Target) in
-  reset_filenames ();
+  Fileinfo.reset_filenames ();
   print_version_and_options oc Target.comment;
   Target.print_prologue oc;
   List.iter (Printer.print_globdef oc) p.prog_defs;
   Target.print_epilogue oc;
-  close_filenames ();
   if !Clflags.option_g && Configuration.advanced_debug then
     begin
       let atom_to_s s =
@@ -141,4 +140,5 @@ let print_program oc p db =
       | None -> ()
       | Some db ->
           Printer.DebugPrinter.print_debug oc db
-    end
+    end;
+  Fileinfo.close_filenames ()
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index b18481da..78399c04 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -14,7 +14,6 @@
 open AST
 open Asm
 open Camlcoq
-open DwarfTypes
 open Datatypes
 open Memdata
 open Printf
@@ -134,71 +133,6 @@ let cfi_rel_offset =
 let coqint oc n =
   fprintf oc "%ld" (camlint_of_coqint n)
 
-(* Printing annotations in asm syntax *)
-
-let filename_info : (string, int * Printlines.filebuf option) Hashtbl.t
-                  = Hashtbl.create 7
-
-let last_file = ref ""
-
-let reset_filenames () =
-  Hashtbl.clear filename_info; last_file := ""
-
-let close_filenames () =
-  Hashtbl.iter
-    (fun file (num, fb) ->
-       match fb with Some b -> Printlines.close b | None -> ())
-    filename_info;
-  reset_filenames()
-
-let enter_filename f =
-  let num = Hashtbl.length filename_info + 1 in
-  let filebuf =
-    if !Clflags.option_S || !Clflags.option_dasm then begin
-      try Some (Printlines.openfile f)
-      with Sys_error _ -> None
-    end else None in
-  Hashtbl.add filename_info f (num, filebuf);
-  (num, filebuf)
-
-(* Add file and line debug location, using GNU assembler-style DWARF2
-   directives *)
-
-let print_file_line oc pref file line =
-  if !Clflags.option_g && file <> "" then begin
-    let (filenum, filebuf) =
-      try
-        Hashtbl.find filename_info file
-      with Not_found ->
-        let (filenum, filebuf as res) = enter_filename file in
-        fprintf oc "	.file	%d %S\n" filenum file;
-        res in
-    fprintf oc "	.loc	%d %d\n" filenum line;
-    match filebuf with
-    | None -> ()
-    | Some fb -> Printlines.copy oc pref fb line line
-  end
-
-(* Add file and line debug location, using DWARF2 directives in the style
-   of Diab C 5 *)
-
-let print_file_line_d2 oc pref file line =
-  if !Clflags.option_g && file <> "" then begin
-    let (_, filebuf) =
-      try
-        Hashtbl.find filename_info file
-      with Not_found ->
-        enter_filename file in
-    if file <> !last_file then begin
-      fprintf oc "	.d2file	%S\n" file;
-      last_file := file
-    end;
-    fprintf oc "	.d2line	%d\n" line;
-    match filebuf with
-    | None -> ()
-    | Some fb -> Printlines.copy oc pref fb line line
-  end
-
 (** Programmer-supplied annotations (__builtin_annot). *)
 
 let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*"
diff --git a/debug/Debug.ml b/debug/Debug.ml
index 6da0927d..348310f6 100644
--- a/debug/Debug.ml
+++ b/debug/Debug.ml
@@ -45,11 +45,13 @@ type implem =
      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 add_compilation_section_start: string -> int -> unit;
+     mutable add_compilation_section_end: string -> int -> unit;
      mutable compute_file_enum: (string -> int) -> (string-> int) -> (unit -> unit) -> unit;
      mutable exists_section: string -> bool;
      mutable remove_unused: ident -> unit;
      mutable variable_printed: string -> unit;
+     mutable add_diab_info: string -> (int * int * string) -> unit;
    }
 
 let implem =
@@ -78,10 +80,12 @@ let implem =
    add_label = (fun _ _ _ -> ());
    atom_parameter = (fun _ _ _ -> ());
    add_compilation_section_start = (fun _ _ -> ());
+   add_compilation_section_end = (fun _ _ -> ());
    compute_file_enum = (fun _ _ _ -> ());
    exists_section = (fun _ -> true);
    remove_unused = (fun _ -> ());
    variable_printed = (fun _ -> ());
+   add_diab_info = (fun _ _ -> ());
 }
 
 let init_compile_unit name = implem.init name
@@ -108,7 +112,9 @@ 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 add_compilation_section_end sec addr = implem.add_compilation_section_end 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
 let remove_unused ident = implem.remove_unused ident
 let variable_printed ident = implem.variable_printed ident
+let add_diab_info sec addr = implem.add_diab_info sec addr
diff --git a/debug/Debug.mli b/debug/Debug.mli
index e9b566a5..98a13b30 100644
--- a/debug/Debug.mli
+++ b/debug/Debug.mli
@@ -43,11 +43,13 @@ type implem =
      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 add_compilation_section_start: string -> int -> unit;
+     mutable add_compilation_section_end: string -> int -> unit;
      mutable compute_file_enum: (string -> int) -> (string-> int) -> (unit -> unit) -> unit;
      mutable exists_section: string -> bool;
      mutable remove_unused: ident -> unit;
      mutable variable_printed: string -> unit;
+     mutable add_diab_info: string -> (int * int * string) -> unit;
    }
 
 val implem: implem
@@ -75,8 +77,10 @@ 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 add_compilation_section_start: string -> int -> unit
+val add_compilation_section_end: string -> int -> unit
 val compute_file_enum: (string -> int) -> (string-> int) -> (unit -> unit) -> unit
 val exists_section: string -> bool
 val remove_unused: ident -> unit
 val variable_printed: string -> unit
+val add_diab_info: string -> (int * int * string) -> unit
diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml
index 6046f894..36138882 100644
--- a/debug/DebugInformation.ml
+++ b/debug/DebugInformation.ml
@@ -644,27 +644,32 @@ let function_end atom loc =
   List.iter (fun id-> end_live_range (atom,id) loc) !open_vars;
   open_vars:= []
 
-let compilation_section_start: (string,int * int * int * string) Hashtbl.t = Hashtbl.create 7
+let compilation_section_start: (string,int) Hashtbl.t = Hashtbl.create 7
 let compilation_section_end: (string,int) Hashtbl.t = Hashtbl.create 7
 
+let diab_additional: (string,int * int * string) 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 add_diab_info sec addr =
+  Hashtbl.add diab_additional 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.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
+    line_end ()) diab_additional
 
 let printed_vars: StringSet.t ref = ref StringSet.empty
 
@@ -688,4 +693,5 @@ let init name =
   Hashtbl.reset compilation_section_end;
   Hashtbl.reset filenum;
   all_files := StringSet.singleton name;
+  Hashtbl.reset diab_additional;
   printed_vars := StringSet.empty;
diff --git a/debug/DebugInit.ml b/debug/DebugInit.ml
index d3ce8d18..5aac6566 100644
--- a/debug/DebugInit.ml
+++ b/debug/DebugInit.ml
@@ -27,7 +27,11 @@ let init_debug () =
   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.generate_debug_info <- 
+    if Configuration.system = "diab" then
+      (fun a b -> Some (Dwarfgen.gen_diab_debug_info a b))
+    else
+      (fun a b -> Some (Dwarfgen.gen_gnu_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;
@@ -43,10 +47,12 @@ let init_debug () =
   implem.add_label <- DebugInformation.add_label;
   implem.atom_parameter <- DebugInformation.atom_parameter;
   implem.add_compilation_section_start <- DebugInformation.add_compilation_section_start;
+  implem.add_compilation_section_end <- DebugInformation.add_compilation_section_end;
   implem.compute_file_enum <- DebugInformation.compute_file_enum;
   implem.exists_section <- DebugInformation.exists_section;
   implem.remove_unused <- DebugInformation.remove_unused;
-  implem.variable_printed <- DebugInformation.variable_printed
+  implem.variable_printed <- DebugInformation.variable_printed;
+  implem.add_diab_info <- DebugInformation.add_diab_info
 
 let init_none () =
   implem.init <- (fun _ -> ());
@@ -73,9 +79,11 @@ let init_none () =
   implem.add_label <- (fun _ _ _ -> ());
   implem.atom_parameter <- (fun _ _ _ -> ());
   implem.add_compilation_section_start <- (fun _ _ -> ());
+  implem.add_compilation_section_end <- (fun _ _ -> ());
   implem.exists_section <- (fun _ -> true);
   implem.remove_unused <- (fun _ -> ());
-  implem.variable_printed <- (fun _ -> ())
+  implem.variable_printed <- (fun _ -> ());
+  implem.add_diab_info <- (fun _ _ -> ())
 
 let init () =
   if !Clflags.option_g && Configuration.advanced_debug then
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml
index d0410b93..980c49db 100644
--- a/debug/DwarfPrinter.ml
+++ b/debug/DwarfPrinter.ml
@@ -246,9 +246,7 @@ module DwarfPrinter(Target: DWARF_TARGET):
       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
       section oc Section_debug_abbrev;
-      let lbl = new_label () in
-      abbrev_start_addr := lbl;
-      print_label oc lbl;
+      print_label oc !abbrev_start_addr;
       List.iter (fun (s,id) ->
         fprintf oc "	.uleb128	%d\n" id;
         output_string oc s;
@@ -258,6 +256,8 @@ module DwarfPrinter(Target: DWARF_TARGET):
 
     let debug_start_addr = ref (-1)
 
+    let debug_stmt_list = ref (-1)
+
     let entry_labels: (int,int) Hashtbl.t = Hashtbl.create 7
 
     (* Translate the ids to address labels *)
@@ -314,10 +314,13 @@ module DwarfPrinter(Target: DWARF_TARGET):
       fprintf oc "	.4byte		%a\n" label ref
 
     let print_file_loc oc = function
-      | Some (file,col) ->
+      | Some (Diab_file_loc (file,col)) ->
           fprintf oc "	.4byte		%a\n" label file;
           print_uleb128 oc col
-      | None -> ()
+      | Some (Gnu_file_loc (file,col)) ->
+          fprintf oc "	.4byte		%l\n" file;
+          print_uleb128 oc col 
+     | None -> ()
 
     let print_loc_expr oc = function
       | DW_OP_bregx (a,b) ->
@@ -417,7 +420,7 @@ module DwarfPrinter(Target: DWARF_TARGET):
       print_uleb128 oc 1;
       print_string oc tag.compile_unit_name;
       print_string oc prod_name;
-      print_addr oc tag.compile_unit_stmt_list
+      print_addr oc !debug_stmt_list
 
     let print_const_type oc ct =
       print_ref oc ct.const_type
@@ -558,14 +561,14 @@ module DwarfPrinter(Target: DWARF_TARGET):
 
     (* Print the debug abbrev section *)
     let print_debug_abbrev oc entries =
-      List.iter (fun (_,_,e,_) -> compute_abbrev e) entries;
+      List.iter (fun (_,_,_,e,_) -> compute_abbrev e) entries;
       print_abbrev oc
 
     (* Print the debug info section *)
-    let print_debug_info oc sec start entry  =
+    let print_debug_info oc start line_start entry  =
       Hashtbl.reset entry_labels;
       debug_start_addr:= start;
-      section oc (Section_debug_info sec);      
+      debug_stmt_list:= line_start;
       print_label oc start;
       let debug_length_start = new_label ()  (* Address used for length calculation *)
       and debug_end = new_label () in
@@ -590,12 +593,33 @@ module DwarfPrinter(Target: DWARF_TARGET):
     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 entries =
+    let print_diab_entries oc entries =
+      let abbrev_start = new_label () in
+      abbrev_start_addr := abbrev_start;  
       print_debug_abbrev oc entries;
-      List.iter (fun (s,d,e,_) -> print_debug_info oc s d e) entries;
+      List.iter (fun (s,d,l,e,_) ->
+        section oc (Section_debug_info s);      
+        print_debug_info oc d l e) entries;
       section oc Section_debug_loc;
-      List.iter (fun (_,_,_,l) -> print_location_list oc l) entries
+      List.iter (fun (_,_,_,_,l) -> print_location_list oc l) entries
+
+    let print_gnu_entries oc cp loc =
+      compute_abbrev cp;
+      let line_start = new_label ()
+      and start = new_label ()
+      and  abbrev_start = new_label () in
+      abbrev_start_addr := abbrev_start;
+      section oc (Section_debug_info "");
+      print_debug_info oc start line_start cp;
+      print_abbrev oc;
+      section oc Section_debug_loc;
+      print_location_list oc loc;
+      fprintf oc "	.section	.debug_line,\"\",@progbits\n";
+      print_label oc line_start
 
+    (* Print the debug info and abbrev section *)
+    let print_debug oc = function
+      | Diab entries -> print_diab_entries oc entries
+      | Gnu (cp,loc) -> print_gnu_entries oc cp loc
 
   end
diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli
index 6c0af52b..ed75b3d7 100644
--- a/debug/DwarfTypes.mli
+++ b/debug/DwarfTypes.mli
@@ -60,8 +60,10 @@ type bound_value =
 
 (* Types representing the attribute information per tag value *)
 
-type file_loc = int * constant
-
+type file_loc = 
+  | Diab_file_loc of int * constant
+  | Gnu_file_loc of int * constant
+     
 type dw_tag_array_type =
     {
      array_type_file_loc: file_loc option;
@@ -80,7 +82,6 @@ type dw_tag_compile_unit =
      compile_unit_name:      string;
      compile_unit_low_pc:    int;
      compile_unit_high_pc:   int;
-     compile_unit_stmt_list: int;
    }
 
 type dw_tag_const_type =
@@ -248,7 +249,13 @@ type location_entry =
    }
 type dw_locations = int * location_entry list
 
-type debug_entries = (string * int * dw_entry * dw_locations) list
+type diab_entries =  (string * int * int * dw_entry * dw_locations) list
+
+type gnu_entries = dw_entry * dw_locations
+
+type debug_entries =
+  | Diab of diab_entries
+  | Gnu of gnu_entries
 
 (* The target specific functions for printing the debug information *)
 module type DWARF_TARGET=
diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml
index 1ef00c31..d2cdecbf 100644
--- a/debug/Dwarfgen.ml
+++ b/debug/Dwarfgen.ml
@@ -85,20 +85,17 @@ let void_to_entry id =
   } 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
+let file_loc_opt file = function
   | None -> None
   | Some (f,l) ->
     try 
-      Some (translate_file_loc sec (f,l))
+      Some (file (f,l))
     with Not_found -> None
 
-let typedef_to_entry sec id t =
+let typedef_to_entry file 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_file_loc = file_loc_opt file t.typedef_file_loc;
     typedef_name = t.typedef_name;
     typedef_type = i;
   } in
@@ -133,7 +130,7 @@ let const_to_entry id c =
 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 enum_to_entry file id e =
   let enumerator_to_entry e =
     let tag =
       {
@@ -144,7 +141,7 @@ let enum_to_entry sec id e =
     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_file_loc = file_loc_opt file e.enum_file_loc;
     enumeration_byte_size = bs;
     enumeration_declaration = Some false;
     enumeration_name = Some e.enum_name;
@@ -195,9 +192,9 @@ let member_to_entry mem =
   } in
   new_entry (next_id ()) (DW_TAG_member mem)
 
-let struct_to_entry sec id s =
+let struct_to_entry file id s =
   let tag = {
-     structure_file_loc = translate_file_loc_opt sec s.ct_file_loc;
+     structure_file_loc = file_loc_opt file s.ct_file_loc;
      structure_byte_size = s.ct_sizeof;
      structure_declaration = if s.ct_declaration then Some s.ct_declaration else None;
      structure_name = if s.ct_name <> "" then Some s.ct_name else None;
@@ -206,9 +203,9 @@ let struct_to_entry sec id s =
   let child = List.map member_to_entry s.ct_members in
   add_children entry child
 
-let union_to_entry sec id s =
+let union_to_entry file id s =
   let tag = {
-    union_file_loc =  translate_file_loc_opt sec s.ct_file_loc;
+    union_file_loc =  file_loc_opt file s.ct_file_loc;
     union_byte_size = s.ct_sizeof;
     union_declaration = if s.ct_declaration then Some s.ct_declaration else None;
     union_name = if s.ct_name <> "" then Some s.ct_name else None;
@@ -217,20 +214,20 @@ let union_to_entry sec id s =
   let child = List.map member_to_entry s.ct_members in
   add_children entry child
 
-let composite_to_entry sec id s =
+let composite_to_entry file id s =
   match s.ct_sou with
-  | Struct -> struct_to_entry sec id s
-  | Union -> union_to_entry sec id s
+  | Struct -> struct_to_entry file id s
+  | Union -> union_to_entry file id s
 
-let infotype_to_entry sec id = function
+let infotype_to_entry file 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
+  | CompositeType c -> composite_to_entry file id c
+  | EnumType e -> enum_to_entry file id e
   | FunctionType f -> fun_type_to_entry id f
-  | Typedef t -> typedef_to_entry sec id t
+  | Typedef t -> typedef_to_entry file id t
   | ConstType c -> const_to_entry id c
   | VolatileType v -> volatile_to_entry id v
   | Void -> void_to_entry id
@@ -269,7 +266,7 @@ let needs_types id d =
         let d,c' = add_type f.cfd_typ d in
         d,c||c') (d,false) c.ct_members
 
-let gen_types sec needed =
+let gen_types file needed =
   let rec aux d =
     let d,c = IntSet.fold (fun id (d,c) ->
       let d,c' = needs_types id d in
@@ -281,17 +278,17 @@ let gen_types sec needed =
   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
+      (infotype_to_entry file id t)::acc
     else 
       acc) types [])
 
-let global_variable_to_entry sec acc id v =
+let global_variable_to_entry file acc id v =
   let loc = match v.gvar_atom with
   | Some a when StringSet.mem (extern_atom a) !printed_vars ->
         Some (LocSymbol a)
   | _ -> None in
   let var = {
-    variable_file_loc = translate_file_loc sec v.gvar_file_loc;
+    variable_file_loc = file v.gvar_file_loc;
     variable_declaration = Some v.gvar_declaration;
     variable_external = Some v.gvar_external;
     variable_name = v.gvar_name;
@@ -365,13 +362,13 @@ let function_parameter_to_entry f_id (acc,bcc) p =
   } 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 rec local_variable_to_entry file f_id (acc,bcc) v id =
   match v.lvar_atom with
   | None -> None,(acc,bcc)
   | Some loc ->
       let loc,loc_list = location_entry f_id loc in
       let var = {
-        variable_file_loc = translate_file_loc sec v.lvar_file_loc;
+        variable_file_loc = file v.lvar_file_loc;
         variable_declaration = None;
         variable_external = None;
         variable_name = v.lvar_name;
@@ -380,7 +377,7 @@ let rec local_variable_to_entry sec f_id (acc,bcc) v id =
       } in
       Some (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 =
+and scope_to_entry file 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 
@@ -397,29 +394,29 @@ and scope_to_entry sec f_id acc sc id =
     lexical_block_high_pc = h_pc;
     lexical_block_low_pc = l_pc;
   } in
-  let vars,acc = mmap_opt (local_to_entry sec f_id) acc sc.scope_variables in
+  let vars,acc = mmap_opt (local_to_entry file 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 =
+and local_to_entry file f_id acc id =
   match Hashtbl.find local_variables id with
-  | LocalVariable v -> local_variable_to_entry sec f_id acc v id
+  | LocalVariable v -> local_variable_to_entry file f_id acc v id
   | Scope v -> let s,acc = 
-      (scope_to_entry sec f_id acc v id) in 
+      (scope_to_entry file f_id acc v id) in 
     Some s,acc
 
-let fun_scope_to_entries sec f_id acc id =
+let fun_scope_to_entries file 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_opt (local_to_entry sec f_id) acc sc.scope_variables
+      | Scope sc ->mmap_opt (local_to_entry file f_id) acc sc.scope_variables
       | _ -> assert false)
 
-let function_to_entry sec (acc,bcc) id f =
+let function_to_entry file (acc,bcc) id f =
   let f_tag = {
-    subprogram_file_loc = translate_file_loc sec f.fun_file_loc;
+    subprogram_file_loc = file f.fun_file_loc;
     subprogram_external = Some f.fun_external;
     subprogram_name = f.fun_name;
     subprogram_prototyped = true;
@@ -431,36 +428,59 @@ let function_to_entry sec (acc,bcc) id f =
   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
+  let vars,(acc,bcc) = fun_scope_to_entries file 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 =
+let definition_to_entry file (acc,bcc) id t =
   match t with
-  | GlobalVariable g -> let e,acc = global_variable_to_entry sec acc id g in
+  | GlobalVariable g -> let e,acc = global_variable_to_entry file acc id g in
     e,(acc,bcc)
-  | Function f -> function_to_entry sec (acc,bcc) id f
+  | Function f -> function_to_entry file (acc,bcc) id f
 
 module StringMap = Map.Make(String)
 
-let gen_debug_info sec_name var_section : debug_entries =
+let diab_file_loc sec (f,l)  =
+  Diab_file_loc (Hashtbl.find filenum (sec,f),l)
+
+let gen_diab_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 entries = 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
+      let t,bcc = definition_to_entry (diab_file_loc 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
+    let low_pc = Hashtbl.find compilation_section_start s
+    and line_start,debug_start,_ = Hashtbl.find diab_additional 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; 
+      compile_unit_high_pc = high_pc; 
     } 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 []
+    let cp = add_children cp ((gen_types (diab_file_loc s) ty) @ defs) in
+    (s,debug_start,line_start,cp,(low_pc,locs))::acc) defs [] in
+  Diab entries
+
+let gnu_file_loc (f,l) =
+    Gnu_file_loc ((fst (Hashtbl.find Fileinfo.filename_info f),l))
+
+let gen_gnu_debug_info sec_name var_section : debug_entries =
+  let low_pc = Hashtbl.find compilation_section_start ".text"
+  and high_pc = Hashtbl.find compilation_section_end ".text" in
+  let defs,(ty,locs) = Hashtbl.fold (fun  id t (acc,bcc) -> 
+    let t,bcc = definition_to_entry gnu_file_loc bcc id t in
+    t::acc,bcc) definitions ([],(IntSet.empty,[])) in
+  let types = gen_types gnu_file_loc ty in
+  let cp = {
+    compile_unit_name = !file_name;
+    compile_unit_low_pc = low_pc;
+    compile_unit_high_pc = high_pc; 
+  } in
+  let cp = new_entry (next_id ()) (DW_TAG_compile_unit cp) in
+  let cp = add_children cp (types@defs) in
+  Gnu (cp,(low_pc,locs))
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 05ff3366..579573b9 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -13,6 +13,7 @@
 (* Printing PPC assembly code in asm syntax *)
 
 open Printf
+open Fileinfo
 open Datatypes
 open Maps
 open Camlcoq
@@ -122,9 +123,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"
-      | Section_debug_loc -> ".debug_loc,\"\",@progbits"
+      | Section_debug_info _ -> ".section	.debug_info,\"\",@progbits"
+      | Section_debug_abbrev -> ".section	.debug_abbrev,\"\",@progbits"
+      | Section_debug_loc -> ".section	.debug_loc,\"\",@progbits"
             
     let section oc sec =
       let name = name_of_section sec in
@@ -144,10 +145,26 @@ module Linux_System : SYSTEM =
               
     let cfi_rel_offset = cfi_rel_offset
 
-    let print_prologue oc = ()
+    let print_prologue oc = 
+      if !Clflags.option_g then
+        begin
+      (* TODO print file *)
+          section oc Section_text;
+          let low_pc = new_label () in
+          Debug.add_compilation_section_start ".text" low_pc;
+          fprintf oc "%a:\n" label low_pc;
+          fprintf oc "	.cfi_sections	.debug_frame\n"
+        end
+
+    let print_epilogue oc =
+      if !Clflags.option_g then
+        begin
+          let high_pc = new_label () in
+          Debug.add_compilation_section_end ".text" high_pc;
+          section oc Section_text;
+          fprintf oc "%a:\n" label high_pc
+        end
 
-    let print_epilogue oc = ()
-        
     let debug_section _ _ = ()
   end
     
@@ -239,7 +256,8 @@ module Diab_System : SYSTEM =
             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);
+            Debug.add_diab_info name (line_start,debug_info,name_of_section sec);
+            Debug.add_compilation_section_start name low_pc;
             let line_name = ".debug_line" ^(if name <> ".text" then name else "") in 
             fprintf oc "	.section	%s,,n\n" line_name;
             if name <> ".text" then