Implement the usage of the debug_str section for the gcc backend.

GCC prints all string larger than 3 characters in the debug_str
section which reduces the size of the debug information since entries
containing the same string now map to the same string in the
debug_str sections.
Bug 17392.

3 files changed, 537 insertions, 470 deletions

diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml
index e6d9cd5e..407850a5 100644
--- a/debug/DwarfPrinter.ml
+++ b/debug/DwarfPrinter.ml
@@ -57,8 +57,6 @@ module DwarfPrinter(Target: DWARF_TARGET):
 
     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_member_size = add_abbr_entry (0xb,member_size_abbr)
@@ -69,6 +67,16 @@ module DwarfPrinter(Target: DWARF_TARGET):
 
     let add_declaration = add_abbr_entry (0x3c,declaration_type_abbr)
 
+    let add_string buf id = function
+      | Simple_string _ -> add_abbr_entry (id,dw_form_string) buf
+      | Offset_string _ -> add_abbr_entry (id,dw_form_strp) buf
+
+    let add_name buf = add_string buf 0x3
+
+    let add_name_opt buf = function
+      | None -> ()
+      | Some s -> add_name buf s
+
     let add_location loc buf =
       match loc with
       | None -> ()
@@ -77,6 +85,8 @@ module DwarfPrinter(Target: DWARF_TARGET):
       | Some (LocSymbol _)
       | Some (LocSimple _) -> add_abbr_entry (0x2,location_block_type_abbr) buf
 
+   
+
     (* Dwarf entity to string function *)
     let abbrev_string_of_entity entity has_sibling =
       let buf = Buffer.create 12 in
@@ -100,15 +110,15 @@ module DwarfPrinter(Target: DWARF_TARGET):
           prologue 0x24;
           add_byte_size buf;
           add_attr_some b.base_type_encoding (add_abbr_entry (0x3e,encoding_type_abbr));
-          add_name buf
+          add_name buf b.base_type_name;
       | DW_TAG_compile_unit e ->
           prologue 0x11;
-          add_abbr_entry (0x1b,comp_dir_type_abbr) buf;
+          add_string buf 0x1b e.compile_unit_dir;
           add_low_pc buf;
           add_high_pc buf;
           add_abbr_entry (0x13,language_type_abbr) buf;
-          add_name buf;
-          add_abbr_entry (0x25,producer_type_abbr) buf;
+          add_name buf e.compile_unit_name;
+          add_string buf 0x25 e.compile_unit_prod_name;
           add_abbr_entry (0x10,stmt_list_type_abbr) buf;
       | DW_TAG_const_type _ ->
           prologue 0x26;
@@ -118,22 +128,22 @@ module DwarfPrinter(Target: DWARF_TARGET):
           add_attr_some e.enumeration_file_loc add_file_loc;
           add_byte_size buf;
           add_attr_some e.enumeration_declaration add_declaration;
-          add_attr_some e.enumeration_name add_name
+          add_name buf e.enumeration_name
       | DW_TAG_enumerator e ->
           prologue 0x28;
           add_abbr_entry (0x1c,value_type_abbr) buf;
-          add_name buf
+          add_name buf e.enumerator_name
       | DW_TAG_formal_parameter e ->
           prologue 0x5;
           add_attr_some e.formal_parameter_artificial (add_abbr_entry (0x34,artificial_type_abbr));
-          add_attr_some e.formal_parameter_name add_name;
+          add_name_opt buf e.formal_parameter_name;
           add_type buf;
           add_attr_some e.formal_parameter_variable_parameter (add_abbr_entry (0x4b,variable_parameter_type_abbr));
           add_location  e.formal_parameter_location buf
-      | DW_TAG_label _ ->
+      | DW_TAG_label e ->
           prologue 0xa;
           add_low_pc buf;
-          add_name buf;
+          add_name buf e.label_name;
       | DW_TAG_lexical_block a ->
           prologue 0xb;
           add_attr_some a.lexical_block_high_pc add_high_pc;
@@ -144,7 +154,7 @@ module DwarfPrinter(Target: DWARF_TARGET):
           add_attr_some e.member_bit_offset (add_abbr_entry (0xc,bit_offset_type_abbr));
           add_attr_some e.member_bit_size (add_abbr_entry (0xd,bit_size_type_abbr));
           add_attr_some e.member_declaration add_declaration;
-          add_attr_some e.member_name add_name;
+          add_name buf e.member_name;
           add_type buf;
           (match e.member_data_member_location with
           | None -> ()
@@ -158,14 +168,14 @@ module DwarfPrinter(Target: DWARF_TARGET):
           add_attr_some e.structure_file_loc add_file_loc;
           add_attr_some e.structure_byte_size add_member_size;
           add_attr_some e.structure_declaration add_declaration;
-          add_attr_some e.structure_name add_name
+          add_name_opt buf e.structure_name
       | DW_TAG_subprogram e ->
           prologue 0x2e;
           add_file_loc buf;
           add_attr_some e.subprogram_external (add_abbr_entry (0x3f,external_type_abbr));
           add_attr_some e.subprogram_high_pc add_high_pc;
           add_attr_some e.subprogram_low_pc add_low_pc;
-          add_name buf;
+          add_name buf e.subprogram_name;
           add_abbr_entry (0x27,prototyped_type_abbr) buf;
           add_attr_some e.subprogram_type add_type;
       | DW_TAG_subrange_type e ->
@@ -182,14 +192,14 @@ module DwarfPrinter(Target: DWARF_TARGET):
       | DW_TAG_typedef e ->
           prologue 0x16;
           add_attr_some e.typedef_file_loc add_file_loc;
-          add_name buf;
+          add_name buf e.typedef_name;
           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_member_size;
           add_attr_some e.union_declaration add_declaration;
-          add_attr_some e.union_name add_name
+          add_name_opt buf e.union_name
       | DW_TAG_unspecified_parameter e ->
           prologue 0x18;
           add_attr_some e.unspecified_parameter_artificial (add_abbr_entry (0x34,artificial_type_abbr))
@@ -199,7 +209,7 @@ module DwarfPrinter(Target: DWARF_TARGET):
           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_name buf e.variable_name;
           add_type buf
       | DW_TAG_volatile_type _ ->
           prologue 0x35;
@@ -289,8 +299,10 @@ module DwarfPrinter(Target: DWARF_TARGET):
     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_string oc = function
+      | Simple_string s ->
+          fprintf oc "	.asciz		\"%s\"\n" s
+      | Offset_string o ->  print_loc_ref oc o
 
     let print_uleb128 oc d =
       fprintf oc "	.uleb128	%d\n" d
@@ -401,19 +413,12 @@ module DwarfPrinter(Target: DWARF_TARGET):
       print_string oc bt.base_type_name
 
     let print_compilation_unit oc tag =
-      let version_string =  
-        if Version.buildnr <> "" && Version.tag <> "" then
-          sprintf "%s, Build: %s, Tag: %s" Version.version Version.buildnr Version.tag
-        else
-          Version.version in
-      let prod_name = sprintf "AbsInt Angewandte Informatik GmbH:CompCert Version %s:(%s,%s,%s,%s)" 
-          version_string Configuration.arch Configuration.system Configuration.abi Configuration.model in
-      print_string oc (Sys.getcwd ());
+      print_string oc tag.compile_unit_dir;
       print_addr oc tag.compile_unit_low_pc;
       print_addr oc tag.compile_unit_high_pc;
       print_uleb128 oc 1;
       print_string oc tag.compile_unit_name;
-      print_string oc prod_name;
+      print_string oc tag.compile_unit_prod_name;
       print_addr oc !debug_stmt_list
 
     let print_const_type oc ct =
@@ -423,7 +428,7 @@ module DwarfPrinter(Target: DWARF_TARGET):
       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_opt_value oc et.enumeration_name print_string
+      print_string oc et.enumeration_name
 
     let print_enumerator oc en =
       print_sleb128 oc en.enumerator_value;
@@ -450,7 +455,7 @@ module DwarfPrinter(Target: DWARF_TARGET):
       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_declaration print_flag;
-      print_opt_value oc mb.member_name print_string;
+      print_string oc mb.member_name;
       print_ref oc mb.member_type;
       print_opt_value oc mb.member_data_member_location print_data_location
 
@@ -602,7 +607,7 @@ module DwarfPrinter(Target: DWARF_TARGET):
       section oc Section_debug_loc;
       List.iter (fun e -> print_location_list oc e.locs) entries
 
-    let print_gnu_entries oc cp loc =
+    let print_gnu_entries oc cp loc s =
       compute_abbrev cp;
       let line_start = new_label ()
       and start = new_label ()
@@ -614,11 +619,16 @@ module DwarfPrinter(Target: DWARF_TARGET):
       section oc Section_debug_loc;
       print_location_list oc loc;
       section oc (Section_debug_line "");
-      print_label oc line_start
+      print_label oc line_start;
+      section oc Section_debug_str;
+      List.iter (fun (id,s) ->
+        print_label oc (loc_to_label id);
+        fprintf oc "	.asciz		\"%s\"\n" s) s
+
 
     (* 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
+      | Gnu (cp,loc,s) -> print_gnu_entries oc cp loc s
 
   end
diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli
index 669ceabc..c7e5dce1 100644
--- a/debug/DwarfTypes.mli
+++ b/debug/DwarfTypes.mli
@@ -36,13 +36,11 @@ type encoding =
 
 type address = int
 
-type block = string
-
 type location_expression =
   | DW_OP_plus_uconst of constant
-  | DW_OP_bregx of int * int32
-  | DW_OP_piece of int
-  | DW_OP_reg of int
+  | DW_OP_bregx of constant * int32
+  | DW_OP_piece of constant
+  | DW_OP_reg of constant
 
 type location_value =
   | LocSymbol of atom
@@ -58,11 +56,15 @@ type bound_value =
   | BoundConst of constant
   | BoundRef of reference
 
+type string_const =
+  | Simple_string of string
+  | Offset_string of reference
+
 (* Types representing the attribute information per tag value *)
 
 type file_loc = 
-  | Diab_file_loc of int * constant
-  | Gnu_file_loc of int * constant
+  | Diab_file_loc of constant * constant
+  | Gnu_file_loc of constant * constant
      
 type dw_tag_array_type =
     {
@@ -72,15 +74,17 @@ type dw_tag_array_type =
 type dw_tag_base_type =
     {
      base_type_byte_size: constant;
-     base_type_encoding:  encoding option;
-     base_type_name:      string;
+     base_type_encoding:  encoding      option;
+     base_type_name:      string_const;
    }
 
 type dw_tag_compile_unit =
     {
-     compile_unit_name:      string;
-     compile_unit_low_pc:    int;
-     compile_unit_high_pc:   int;
+     compile_unit_name:      string_const;
+     compile_unit_low_pc:    constant;
+     compile_unit_high_pc:   constant;
+     compile_unit_dir:       string_const;
+     compile_unit_prod_name: string_const;
    }
 
 type dw_tag_const_type =
@@ -90,22 +94,22 @@ type dw_tag_const_type =
 
 type dw_tag_enumeration_type =
     {
-     enumeration_file_loc:    file_loc  option;
+     enumeration_file_loc:    file_loc     option;
      enumeration_byte_size:   constant;
-     enumeration_declaration: flag      option;
-     enumeration_name:        string    option;
+     enumeration_declaration: flag         option;
+     enumeration_name:        string_const;
    }
 
 type dw_tag_enumerator =
     {
      enumerator_value:    constant;
-     enumerator_name:     string;
+     enumerator_name:     string_const;
    }
 
 type dw_tag_formal_parameter =
     {
      formal_parameter_artificial:         flag           option;
-     formal_parameter_name:               string         option;
+     formal_parameter_name:               string_const   option;
      formal_parameter_type:               reference;
      formal_parameter_variable_parameter: flag           option;
      formal_parameter_location:           location_value option;
@@ -114,7 +118,7 @@ type dw_tag_formal_parameter =
 type dw_tag_label =
     {
      label_low_pc: address;
-     label_name:   string;
+     label_name:   string_const;
    }
 
 type dw_tag_lexical_block =
@@ -130,7 +134,7 @@ type dw_tag_member =
      member_bit_size:             constant            option;
      member_data_member_location: data_location_value option;
      member_declaration:          flag                option;
-     member_name:                 string              option;
+     member_name:                 string_const;
      member_type:                 reference;
    }
 
@@ -141,21 +145,21 @@ type dw_tag_pointer_type =
 
 type dw_tag_structure_type =
     {
-     structure_file_loc:    file_loc option;
-     structure_byte_size:   constant option;
-     structure_declaration: flag     option;
-     structure_name:        string   option;
+     structure_file_loc:    file_loc     option;
+     structure_byte_size:   constant     option;
+     structure_declaration: flag         option;
+     structure_name:        string_const option;
    }
 
 type dw_tag_subprogram =
     {
      subprogram_file_loc:   file_loc;
-     subprogram_external:   flag      option;
-     subprogram_name:       string;
+     subprogram_external:   flag          option;
+     subprogram_name:       string_const;
      subprogram_prototyped: flag;
-     subprogram_type:       reference option;
-     subprogram_high_pc:    reference option;
-     subprogram_low_pc:     reference option;
+     subprogram_type:       reference     option;
+     subprogram_high_pc:    reference     option;
+     subprogram_low_pc:     reference     option;
    }
 
 type dw_tag_subrange_type =
@@ -173,21 +177,21 @@ type dw_tag_subroutine_type =
 type dw_tag_typedef =
     {
      typedef_file_loc: file_loc option;
-     typedef_name:     string;
+     typedef_name:     string_const;
      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   option;
+     union_file_loc:    file_loc     option;
+     union_byte_size:   constant     option;
+     union_declaration: flag         option;
+     union_name:        string_const option;
    }
 
 type dw_tag_unspecified_parameter =
     {
-     unspecified_parameter_artificial: flag     option;
+     unspecified_parameter_artificial: flag option;
    }
 
 type dw_tag_variable =
@@ -195,7 +199,7 @@ type dw_tag_variable =
      variable_file_loc:    file_loc;
      variable_declaration: flag           option;
      variable_external:    flag           option;
-     variable_name:        string;
+     variable_name:        string_const;
      variable_type:        reference;
      variable_location:    location_value option;
    }
@@ -239,10 +243,10 @@ type dw_entry =
 (* The type for the location list. *)
 type location_entry =
     {
-     loc:     (int * int * location_value) list;
+     loc:     (address * address * location_value) list;
      loc_id:  reference;
    }
-type dw_locations = int option * location_entry list
+type dw_locations = constant option * location_entry list
 
 type diab_entry =
     {
@@ -255,7 +259,9 @@ type diab_entry =
 
 type diab_entries =  diab_entry list
 
-type gnu_entries = dw_entry * dw_locations
+type dw_string = (int * string) list
+
+type gnu_entries = dw_entry * dw_locations * dw_string
 
 type debug_entries =
   | Diab of diab_entries
diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml
index a3414831..78c4fffb 100644
--- a/debug/Dwarfgen.ml
+++ b/debug/Dwarfgen.ml
@@ -50,392 +50,444 @@ let rec mmap_opt f env = function
         | None -> tl',env2
       end
 
-(* Functions to translate the basetypes. *)
-let int_type_to_entry id i =
-   let encoding =
-    (match i.int_kind with
-    | IBool -> DW_ATE_boolean
-    | IChar ->
-        if !Machine.config.Machine.char_signed then 
-          DW_ATE_signed_char 
-        else 
-          DW_ATE_unsigned_char
-    | IInt | ILong | ILongLong | IShort | ISChar -> DW_ATE_signed
-    | _ -> DW_ATE_unsigned)in
-  let int = {
-    base_type_byte_size = sizeof_ikind i.int_kind;
-    base_type_encoding = Some encoding;
-    base_type_name = typ_to_string (TInt (i.int_kind,[]));} in
-  new_entry id (DW_TAG_base_type int)
-
-let float_type_to_entry id f = 
-  let byte_size = sizeof_fkind f.float_kind in
-  let float = {
-    base_type_byte_size = byte_size;
-    base_type_encoding = Some DW_ATE_float;
-    base_type_name = typ_to_string (TFloat (f.float_kind,[]));
-  } in
-  new_entry id (DW_TAG_base_type float)
+module type TARGET =
+    sig
+      val file_loc: string * int -> file_loc
+      val string_entry: string -> string_const
+    end
 
-let void_to_entry id =
-  let void = {
-    base_type_byte_size = 0;
-    base_type_encoding = None;
-    base_type_name = "void";
-  } in
-  new_entry id (DW_TAG_base_type void)
-
-let file_loc_opt file = function
-  | None -> None
-  | Some (f,l) ->
-    try 
-      Some (file (f,l))
-    with Not_found -> None
-
-let typedef_to_entry file id t =
-  let i = get_opt_val t.typ in
-  let td = {
-    typedef_file_loc = file_loc_opt file t.typedef_file_loc;
-    typedef_name = t.typedef_name;
-    typedef_type = i;
-  } in
-  new_entry id (DW_TAG_typedef td) 
+module Dwarfgenaux (Target: TARGET) =
+  struct
+    
+    include Target
+
+    let name_opt n = if n <> "" then Some (string_entry n) else None
+    
+    (* Functions to translate the basetypes. *)
+    let int_type_to_entry id i =
+      let encoding =
+        (match i.int_kind with
+        | IBool -> DW_ATE_boolean
+        | IChar ->
+            if !Machine.config.Machine.char_signed then 
+              DW_ATE_signed_char 
+            else 
+              DW_ATE_unsigned_char
+        | IInt | ILong | ILongLong | IShort | ISChar -> DW_ATE_signed
+        | _ -> DW_ATE_unsigned)in
+      let int = {
+        base_type_byte_size = sizeof_ikind i.int_kind;
+        base_type_encoding = Some encoding;
+        base_type_name = string_entry (typ_to_string (TInt (i.int_kind,[])));
+      } in
+      new_entry id (DW_TAG_base_type int)
+
+    let float_type_to_entry id f = 
+      let byte_size = sizeof_fkind f.float_kind in
+      let float = {
+        base_type_byte_size = byte_size;
+        base_type_encoding = Some DW_ATE_float;
+        base_type_name = string_entry (typ_to_string (TFloat (f.float_kind,[])));
+      } in
+      new_entry id (DW_TAG_base_type float)
 
-let pointer_to_entry id p =
-  let p = {pointer_type = p.pts} in
-  new_entry id (DW_TAG_pointer_type p)
+    let void_to_entry id =
+      let void = {
+        base_type_byte_size = 0;
+        base_type_encoding = None;
+        base_type_name = string_entry "void";
+      } in
+      new_entry id (DW_TAG_base_type void)
+
+    let file_loc_opt = function
+      | None -> None
+      | Some (f,l) ->
+          try 
+            Some (file_loc (f,l))
+          with Not_found -> None
+
+    let typedef_to_entry id t =
+      let i = get_opt_val t.typ in
+      let td = {
+        typedef_file_loc = file_loc_opt t.typedef_file_loc;
+        typedef_name = string_entry t.typedef_name;
+        typedef_type = i;
+      } in
+      new_entry id (DW_TAG_typedef td) 
 
-let array_to_entry id arr =
-  let arr_tag = {
-    array_type = arr.arr_type;
-  } in
-  let arr_entry = new_entry id (DW_TAG_array_type arr_tag) in
-  let children = List.map (fun a ->
-    let r = match a with
-    | None -> None
-    | Some i ->
-        let bound = Int64.to_int (Int64.sub i Int64.one) in
-        Some (BoundConst bound) in
-    let s = {
-       subrange_type = None;
-       subrange_upper_bound = r;
-    } in
-    new_entry (next_id ()) (DW_TAG_subrange_type s)) arr.arr_size in
-  add_children arr_entry children
-
-let const_to_entry id c =
-  new_entry id (DW_TAG_const_type ({const_type = c.cst_type}))
-
-let volatile_to_entry id v =
-  new_entry id (DW_TAG_volatile_type ({volatile_type = v.vol_type}))
-
-let enum_to_entry file id e =
-  let enumerator_to_entry e =
-    let tag =
-      {
-       enumerator_value = Int64.to_int (e.enumerator_const);
-       enumerator_name = e.enumerator_name;
-     } in
-    new_entry (next_id ()) (DW_TAG_enumerator tag) in
-  let bs = sizeof_ikind enum_ikind in
-  let enum = {
-    enumeration_file_loc = file_loc_opt file e.enum_file_loc;
-    enumeration_byte_size = bs;
-    enumeration_declaration = Some false;
-    enumeration_name = Some e.enum_name;
-  } in
-  let enum = new_entry id (DW_TAG_enumeration_type enum) in
-  let child = List.map enumerator_to_entry e.enum_enumerators in
-  add_children enum child
-
-let fun_type_to_entry id f =
-  let children = if f.fun_prototyped then
-    let u = {
-      unspecified_parameter_artificial = None;
-    } in
-    [new_entry (next_id ()) (DW_TAG_unspecified_parameter u)]
-  else
-    List.map (fun p ->
-      let fp = {
-        formal_parameter_artificial = None;
-        formal_parameter_name = if p.param_name <> "" then Some p.param_name else None;
-        formal_parameter_type = p.param_type;
-        formal_parameter_variable_parameter = None;
-        formal_parameter_location = None;
+    let pointer_to_entry id p =
+      let p = {pointer_type = p.pts} in
+      new_entry id (DW_TAG_pointer_type p)
+
+    let array_to_entry id arr =
+      let arr_tag = {
+        array_type = arr.arr_type;
       } in
-      new_entry (next_id ()) (DW_TAG_formal_parameter fp)) f.fun_params;
-  in
-  let s = {
-    subroutine_type = f.fun_return_type;
-    subroutine_prototyped = f.fun_prototyped
-  } in
-  let s = new_entry id (DW_TAG_subroutine_type s) in
-  add_children s children
-
-let member_to_entry mem =
-  let mem = {
-    member_byte_size = mem.cfd_byte_size;
-    member_bit_offset = mem.cfd_bit_offset;
-    member_bit_size = mem.cfd_bit_size;
-    member_data_member_location =
-    (match mem.cfd_byte_offset with 
-    | None -> None 
-    | Some s -> Some (DataLocBlock (DW_OP_plus_uconst s)));
-    member_declaration = None;
-    member_name = Some (mem.cfd_name);
-    member_type = mem.cfd_typ;
-  } in
-  new_entry (next_id ()) (DW_TAG_member mem)
-
-let struct_to_entry file id s =
-  let tag = {
-     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;
-  } in
-  let entry = new_entry id (DW_TAG_structure_type tag) in
-  let child = List.map member_to_entry s.ct_members in
-  add_children entry child
-
-let union_to_entry file id s =
-  let tag = {
-    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;
-  } in
-  let entry = new_entry id (DW_TAG_union_type tag) in
-  let child = List.map member_to_entry s.ct_members in
-  add_children entry child
-
-let composite_to_entry file id s =
-  match s.ct_sou with
-  | Struct -> struct_to_entry file id s
-  | Union -> union_to_entry file id s
-
-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 file id c
-  | EnumType e -> enum_to_entry file id e
-  | FunctionType f -> fun_type_to_entry id f
-  | 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
-
-let needs_types id d =
-  let add_type id d =
-    if not (IntSet.mem id d) then
-        IntSet.add id d,true
-      else 
-        d,false in
-  let t = Hashtbl.find types id in
-  match t with
-  | IntegerType _ 
-  | FloatType _
-  | Void
-  | EnumType _ -> d,false
-  | Typedef t ->
-      add_type (get_opt_val t.typ) d
-  | PointerType p -> 
-      add_type p.pts d
-  | ArrayType arr -> 
-      add_type arr.arr_type d
-  | ConstType c ->
-      add_type c.cst_type d
-  | VolatileType v ->
-      add_type v.vol_type d
-  | FunctionType f ->
-      let d,c = match f.fun_return_type with
-      | Some t -> add_type t d 
-      | None -> d,false in
-      List.fold_left (fun (d,c) p ->
-        let d,c' = add_type p.param_type d in
-        d,c||c') (d,c) f.fun_params
-  | CompositeType c -> 
-      List.fold_left (fun (d,c) f ->
-        let d,c' = add_type f.cfd_typ d in
-        d,c||c') (d,false) c.ct_members
-
-let gen_types file needed =
-  let rec aux d =
-    let d,c = IntSet.fold (fun id (d,c) ->
-      let d,c' = needs_types id d in
-      d,c||c') d (d,false) in
-    if c then
-      aux d
-    else
-      d in
-  let typs = aux needed in
-  List.rev (Hashtbl.fold (fun id t acc -> 
-    if IntSet.mem id typs then
-      (infotype_to_entry file id t)::acc
-    else 
-      acc) types [])
-
-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 = file v.gvar_file_loc;
-    variable_declaration = Some v.gvar_declaration;
-    variable_external = Some v.gvar_external;
-    variable_name = v.gvar_name;
-    variable_type = v.gvar_type;
-    variable_location = loc;
-  } in
-  new_entry id (DW_TAG_variable var),IntSet.add v.gvar_type acc
-
-let gen_splitlong op_hi op_lo =
-  let op_piece = DW_OP_piece 4 in
-  op_piece::op_hi@(op_piece::op_lo)
-  
-let translate_function_loc a = function 
-  | BA_addrstack (ofs) ->
-      let ofs = camlint_of_coqint ofs in
-      Some (LocSimple (DW_OP_bregx (a,ofs))),[]
-  | BA_splitlong (BA_addrstack hi,BA_addrstack lo)->
-      let hi = camlint_of_coqint hi 
-      and lo = camlint_of_coqint lo in
-      if lo = Int32.add hi 4l then
-        Some (LocSimple (DW_OP_bregx (a,hi))),[]
+      let arr_entry = new_entry id (DW_TAG_array_type arr_tag) in
+      let children = List.map (fun a ->
+        let r = match a with
+        | None -> None
+        | Some i ->
+            let bound = Int64.to_int (Int64.sub i Int64.one) in
+            Some (BoundConst bound) in
+        let s = {
+          subrange_type = None;
+          subrange_upper_bound = r;
+        } in
+        new_entry (next_id ()) (DW_TAG_subrange_type s)) arr.arr_size in
+      add_children arr_entry children
+
+    let const_to_entry id c =
+      new_entry id (DW_TAG_const_type ({const_type = c.cst_type}))
+
+    let volatile_to_entry id v =
+      new_entry id (DW_TAG_volatile_type ({volatile_type = v.vol_type}))
+
+    let enum_to_entry id e =
+      let enumerator_to_entry e =
+        let tag =
+          {
+           enumerator_value = Int64.to_int (e.enumerator_const);
+           enumerator_name = string_entry e.enumerator_name;
+         } in
+        new_entry (next_id ()) (DW_TAG_enumerator tag) in
+      let bs = sizeof_ikind enum_ikind in
+      let enum = {
+        enumeration_file_loc = file_loc_opt e.enum_file_loc;
+        enumeration_byte_size = bs;
+        enumeration_declaration = Some false;
+        enumeration_name = string_entry e.enum_name;
+      } in
+      let enum = new_entry id (DW_TAG_enumeration_type enum) in
+      let child = List.map enumerator_to_entry e.enum_enumerators in
+      add_children enum child
+
+    let fun_type_to_entry id f =
+      let children = if f.fun_prototyped then
+        let u = {
+          unspecified_parameter_artificial = None;
+        } in
+        [new_entry (next_id ()) (DW_TAG_unspecified_parameter u)]
       else
-        let op_hi = [DW_OP_bregx (a,hi)]
-        and op_lo = [DW_OP_bregx (a,lo)] in
-        Some (LocList (gen_splitlong op_hi op_lo)),[]
-  | _ -> None,[]
-      
-let range_entry_loc (sp,l) =
-  let rec aux = function
-    | BA i ->  [DW_OP_reg i]
-    | BA_addrstack ofs -> 
-        let ofs = camlint_of_coqint ofs in
-        [DW_OP_bregx (sp,ofs)]
-    | BA_splitlong (hi,lo) ->
-        let hi = aux hi
-        and lo = aux lo in
-        gen_splitlong hi lo
-    | _ -> assert false in
-  match aux l with
-  | [] -> assert false
-  | [a] -> LocSimple a
-  | a::rest -> LocList (a::rest)
-
-let location_entry f_id atom =
-  try
-    begin 
-      match (Hashtbl.find var_locations (f_id,atom)) with
-      | FunctionLoc (a,r) ->
-          translate_function_loc a r
-      | RangeLoc l ->
-          let l = List.rev_map (fun i -> 
-            let hi = get_opt_val i.range_start
-            and lo = get_opt_val i.range_end in
-            let hi = Hashtbl.find label_translation (f_id,hi)
-            and lo = Hashtbl.find label_translation (f_id,lo) in
-            hi,lo,range_entry_loc i.var_loc) l in
-          let id = next_id () in
-        Some (LocRef id),[{loc = l;loc_id = id;}]
-    end
-  with Not_found -> None,[]
-
-let function_parameter_to_entry f_id (acc,bcc) p =
-  let loc,loc_list = location_entry f_id (get_opt_val p.parameter_atom) in
-  let p = {
-    formal_parameter_artificial = None;
-    formal_parameter_name = Some p.parameter_name;
-    formal_parameter_type = p.parameter_type;
-    formal_parameter_variable_parameter = None;
-    formal_parameter_location = loc;
-  } in
-  new_entry (next_id ()) (DW_TAG_formal_parameter p),(IntSet.add p.formal_parameter_type acc,loc_list@bcc)
+        List.map (fun p ->
+          let fp = {
+            formal_parameter_artificial = None;
+            formal_parameter_name = name_opt p.param_name;
+            formal_parameter_type = p.param_type;
+            formal_parameter_variable_parameter = None;
+            formal_parameter_location = None;
+          } in
+          new_entry (next_id ()) (DW_TAG_formal_parameter fp)) f.fun_params;
+      in
+      let s = {
+        subroutine_type = f.fun_return_type;
+        subroutine_prototyped = f.fun_prototyped
+      } in
+      let s = new_entry id (DW_TAG_subroutine_type s) in
+      add_children s children
+
+    let member_to_entry mem =
+      let mem = {
+        member_byte_size = mem.cfd_byte_size;
+        member_bit_offset = mem.cfd_bit_offset;
+        member_bit_size = mem.cfd_bit_size;
+        member_data_member_location =
+        (match mem.cfd_byte_offset with 
+        | None -> None 
+        | Some s -> Some (DataLocBlock (DW_OP_plus_uconst s)));
+        member_declaration = None;
+        member_name = string_entry mem.cfd_name;
+        member_type = mem.cfd_typ;
+      } in
+      new_entry (next_id ()) (DW_TAG_member mem)
+
+    let struct_to_entry id s =
+      let tag = {
+        structure_file_loc = file_loc_opt 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 = name_opt s.ct_name;
+      } in
+      let entry = new_entry id (DW_TAG_structure_type tag) in
+      let child = List.map member_to_entry s.ct_members in
+      add_children entry child
+
+    let union_to_entry id s =
+      let tag = {
+        union_file_loc =  file_loc_opt 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 = name_opt s.ct_name;
+      } in
+      let entry = new_entry id (DW_TAG_union_type tag) in
+      let child = List.map member_to_entry s.ct_members in
+      add_children entry child
+
+    let composite_to_entry id s =
+      match s.ct_sou with
+      | Struct -> struct_to_entry id s
+      | Union -> union_to_entry id s
+
+    let infotype_to_entry 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 id c
+      | EnumType e -> enum_to_entry id e
+      | FunctionType f -> fun_type_to_entry id f
+      | Typedef t -> typedef_to_entry id t
+      | ConstType c -> const_to_entry id c
+      | VolatileType v -> volatile_to_entry id v
+      | Void -> void_to_entry id
+
+    let needs_types id d =
+      let add_type id d =
+        if not (IntSet.mem id d) then
+          IntSet.add id d,true
+        else 
+          d,false in
+      let t = Hashtbl.find types id in
+      match t with
+      | IntegerType _ 
+      | FloatType _
+      | Void
+      | EnumType _ -> d,false
+      | Typedef t ->
+          add_type (get_opt_val t.typ) d
+      | PointerType p -> 
+          add_type p.pts d
+      | ArrayType arr -> 
+          add_type arr.arr_type d
+      | ConstType c ->
+          add_type c.cst_type d
+      | VolatileType v ->
+          add_type v.vol_type d
+      | FunctionType f ->
+          let d,c = match f.fun_return_type with
+          | Some t -> add_type t d 
+          | None -> d,false in
+          List.fold_left (fun (d,c) p ->
+            let d,c' = add_type p.param_type d in
+            d,c||c') (d,c) f.fun_params
+      | CompositeType c -> 
+          List.fold_left (fun (d,c) f ->
+            let d,c' = add_type f.cfd_typ d in
+            d,c||c') (d,false) c.ct_members
+
+    let gen_types needed =
+      let rec aux d =
+        let d,c = IntSet.fold (fun id (d,c) ->
+          let d,c' = needs_types id d in
+          d,c||c') d (d,false) in
+        if c then
+          aux d
+        else
+          d in
+      let typs = aux needed in
+      List.rev (Hashtbl.fold (fun id t acc -> 
+        if IntSet.mem id typs then
+          (infotype_to_entry id t)::acc
+        else 
+          acc) types [])
 
-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 global_variable_to_entry 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 = file v.lvar_file_loc;
-        variable_declaration = None;
-        variable_external = None;
-        variable_name = v.lvar_name;
-        variable_type = v.lvar_type;
+        variable_file_loc = file_loc v.gvar_file_loc;
+        variable_declaration = Some v.gvar_declaration;
+        variable_external = Some v.gvar_external;
+        variable_name = string_entry v.gvar_name;
+        variable_type = v.gvar_type;
         variable_location = loc;
       } in
-      Some (new_entry id (DW_TAG_variable var)),(IntSet.add v.lvar_type acc,loc_list@bcc)
-
-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 
-    | Some l -> Some (Hashtbl.find label_translation (f_id,l)) 
-    | None -> None in
-    begin
-      match r with
-      | [] -> None,None
-      | [a] -> lbl a.start_addr, lbl a.end_addr
-      | a::rest -> lbl (List.hd (List.rev rest)).start_addr,lbl a.end_addr
-    end
-  with Not_found -> None,None in
-  let scope = {
-    lexical_block_high_pc = h_pc;
-    lexical_block_low_pc = l_pc;
-  } in
-  let vars,acc = mmap_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 file f_id acc id =
-  match Hashtbl.find local_variables id with
-  | LocalVariable v -> local_variable_to_entry file f_id acc v id
-  | Scope v -> let s,acc = 
-      (scope_to_entry file f_id acc v id) in 
-    Some s,acc
-
-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 file f_id) acc sc.scope_variables
-      | _ -> assert false)
-
-let function_to_entry file (acc,bcc) id f =
-  let f_tag = {
-    subprogram_file_loc = file f.fun_file_loc;
-    subprogram_external = Some f.fun_external;
-    subprogram_name = f.fun_name;
-    subprogram_prototyped = true;
-    subprogram_type = f.fun_return_type;
-    subprogram_high_pc = f.fun_high_pc;
-    subprogram_low_pc = f.fun_low_pc;
-  } in
-  let f_id = get_opt_val f.fun_atom in
-  let acc = match f.fun_return_type with Some s -> IntSet.add s acc | None -> acc in
-  let f_entry =  new_entry id (DW_TAG_subprogram f_tag) in
-  let params,(acc,bcc) = mmap (function_parameter_to_entry f_id) (acc,bcc) f.fun_parameter in
-  let vars,(acc,bcc) = fun_scope_to_entries file f_id (acc,bcc) f.fun_scope in
-  add_children f_entry (params@vars),(acc,bcc)
-     
-let definition_to_entry file (acc,bcc) id t =
-  match t with
-  | GlobalVariable g -> let e,acc = global_variable_to_entry file acc id g in
-    e,(acc,bcc)
-  | Function f -> function_to_entry file (acc,bcc) id f
+      new_entry id (DW_TAG_variable var),IntSet.add v.gvar_type acc
+
+    let gen_splitlong op_hi op_lo =
+      let op_piece = DW_OP_piece 4 in
+      op_piece::op_hi@(op_piece::op_lo)
+                         
+    let translate_function_loc a = function 
+      | BA_addrstack (ofs) ->
+          let ofs = camlint_of_coqint ofs in
+          Some (LocSimple (DW_OP_bregx (a,ofs))),[]
+      | BA_splitlong (BA_addrstack hi,BA_addrstack lo)->
+          let hi = camlint_of_coqint hi 
+          and lo = camlint_of_coqint lo in
+          if lo = Int32.add hi 4l then
+            Some (LocSimple (DW_OP_bregx (a,hi))),[]
+          else
+            let op_hi = [DW_OP_bregx (a,hi)]
+            and op_lo = [DW_OP_bregx (a,lo)] in
+            Some (LocList (gen_splitlong op_hi op_lo)),[]
+      | _ -> None,[]
+            
+    let range_entry_loc (sp,l) =
+      let rec aux = function
+        | BA i ->  [DW_OP_reg i]
+        | BA_addrstack ofs -> 
+            let ofs = camlint_of_coqint ofs in
+            [DW_OP_bregx (sp,ofs)]
+        | BA_splitlong (hi,lo) ->
+            let hi = aux hi
+            and lo = aux lo in
+            gen_splitlong hi lo
+        | _ -> assert false in
+      match aux l with
+      | [] -> assert false
+      | [a] -> LocSimple a
+      | a::rest -> LocList (a::rest)
+
+    let location_entry f_id atom =
+      try
+        begin 
+          match (Hashtbl.find var_locations (f_id,atom)) with
+          | FunctionLoc (a,r) ->
+              translate_function_loc a r
+          | RangeLoc l ->
+              let l = List.rev_map (fun i -> 
+                let hi = get_opt_val i.range_start
+                and lo = get_opt_val i.range_end in
+                let hi = Hashtbl.find label_translation (f_id,hi)
+                and lo = Hashtbl.find label_translation (f_id,lo) in
+                hi,lo,range_entry_loc i.var_loc) l in
+              let id = next_id () in
+              Some (LocRef id),[{loc = l;loc_id = id;}]
+        end
+      with Not_found -> None,[]
+
+    let function_parameter_to_entry f_id (acc,bcc) p =
+      let loc,loc_list = location_entry f_id (get_opt_val p.parameter_atom) in
+      let p = {
+        formal_parameter_artificial = None;
+        formal_parameter_name = name_opt p.parameter_name;
+        formal_parameter_type = p.parameter_type;
+        formal_parameter_variable_parameter = None;
+        formal_parameter_location = loc;
+      } in
+      new_entry (next_id ()) (DW_TAG_formal_parameter p),(IntSet.add p.formal_parameter_type acc,loc_list@bcc)
+
+    let rec local_variable_to_entry 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 = file_loc v.lvar_file_loc;
+            variable_declaration = None;
+            variable_external = None;
+            variable_name = string_entry v.lvar_name;
+            variable_type = v.lvar_type;
+            variable_location = loc;
+          } in
+          Some (new_entry id (DW_TAG_variable var)),(IntSet.add v.lvar_type acc,loc_list@bcc)
+
+    and scope_to_entry  f_id acc sc id =
+      let l_pc,h_pc = try
+        let r = Hashtbl.find scope_ranges id in
+        let lbl l = match l with 
+        | Some l -> Some (Hashtbl.find label_translation (f_id,l)) 
+        | None -> None in
+        begin
+          match r with
+          | [] -> None,None
+          | [a] -> lbl a.start_addr, lbl a.end_addr
+          | a::rest -> lbl (List.hd (List.rev rest)).start_addr,lbl a.end_addr
+        end
+      with Not_found -> None,None in
+      let scope = {
+        lexical_block_high_pc = h_pc;
+        lexical_block_low_pc = l_pc;
+      } in
+      let vars,acc = mmap_opt (local_to_entry  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 f_id acc id =
+      match Hashtbl.find local_variables id with
+      | LocalVariable v -> local_variable_to_entry f_id acc v id
+      | Scope v -> let s,acc = 
+          (scope_to_entry f_id acc v id) in 
+        Some s,acc
+
+    let fun_scope_to_entries 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 f_id) acc sc.scope_variables
+          | _ -> assert false)
+
+    let function_to_entry (acc,bcc) id f =
+      let f_tag = {
+        subprogram_file_loc = file_loc f.fun_file_loc;
+        subprogram_external = Some f.fun_external;
+        subprogram_name = string_entry f.fun_name;
+        subprogram_prototyped = true;
+        subprogram_type = f.fun_return_type;
+        subprogram_high_pc = f.fun_high_pc;
+        subprogram_low_pc = f.fun_low_pc;
+      } in
+      let f_id = get_opt_val f.fun_atom in
+      let acc = match f.fun_return_type with Some s -> IntSet.add s acc | None -> acc in
+      let f_entry =  new_entry id (DW_TAG_subprogram f_tag) in
+      let params,(acc,bcc) = mmap (function_parameter_to_entry f_id) (acc,bcc) f.fun_parameter in
+      let vars,(acc,bcc) = fun_scope_to_entries f_id (acc,bcc) f.fun_scope in
+      add_children f_entry (params@vars),(acc,bcc)
+        
+    let definition_to_entry (acc,bcc) id t =
+      match t with
+      | GlobalVariable g -> let e,acc = global_variable_to_entry acc id g in
+        e,(acc,bcc)
+      | Function f -> function_to_entry (acc,bcc) id f
+
+  end
 
 module StringMap = Map.Make(String)
 
 let diab_file_loc sec (f,l)  =
   Diab_file_loc (Hashtbl.find filenum (sec,f),l)
 
+let prod_name =
+  let version_string =  
+    if Version.buildnr <> "" && Version.tag <> "" then
+      Printf.sprintf "%s, Build: %s, Tag: %s" Version.version Version.buildnr Version.tag
+    else
+      Version.version in
+  Printf.sprintf "AbsInt Angewandte Informatik GmbH:CompCert Version %s:(%s,%s,%s,%s)" 
+    version_string Configuration.arch Configuration.system Configuration.abi Configuration.model
+
+let diab_gen_compilation_section s defs acc =
+  let module Gen = Dwarfgenaux(struct
+    let file_loc = diab_file_loc s
+    let string_entry s =  Simple_string s end) in
+  let defs,(ty,locs) = List.fold_left (fun (acc,bcc) (id,t) -> 
+    let t,bcc = Gen.definition_to_entry  bcc id t in
+    t::acc,bcc) ([],(IntSet.empty,[])) defs in
+  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 = Simple_string !file_name;
+    compile_unit_low_pc = low_pc;
+    compile_unit_high_pc = high_pc;
+    compile_unit_dir = Simple_string (Sys.getcwd ());
+    compile_unit_prod_name = Simple_string prod_name
+  } in
+  let cp = new_entry (next_id ()) (DW_TAG_compile_unit cp) in
+  let cp = add_children cp ((Gen.gen_types ty) @ defs) in
+  {
+    section_name = s;
+    start_label = debug_start;
+    line_label = line_start;
+    entry = cp;
+    locs = Some low_pc,locs;
+  }::acc
+ 
 let gen_diab_debug_info sec_name var_section : debug_entries =
   let defs = Hashtbl.fold (fun id t acc ->
     let s = match t with
@@ -443,49 +495,48 @@ let gen_diab_debug_info sec_name var_section : debug_entries =
     | 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
-  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 (diab_file_loc s) bcc id t in
-      t::acc,bcc) ([],(IntSet.empty,[])) defs in
-    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; 
-    } in
-    let cp = new_entry (next_id ()) (DW_TAG_compile_unit cp) in
-    let cp = add_children cp ((gen_types (diab_file_loc s) ty) @ defs) in
-    let entry = {
-      section_name = s;
-      start_label = debug_start;
-      line_label = line_start;
-      entry = cp;
-      locs = Some low_pc,locs;
-    } in
-    entry::acc) defs [] in
+  let entries = StringMap.fold diab_gen_compilation_section defs [] in
   Diab entries
 
 let gnu_file_loc (f,l) =
-    Gnu_file_loc ((fst (Hashtbl.find Fileinfo.filename_info f),l))
+  Gnu_file_loc ((fst (Hashtbl.find Fileinfo.filename_info f),l))
 
+let string_table: (string,int) Hashtbl.t = Hashtbl.create 7
+
+let gnu_string_entry s =
+  if String.length s < 4 || Configuration.system = "cygwin" then (*Cygwin does not use the debug_str seciton *)
+    Simple_string s
+  else
+    try
+      Offset_string (Hashtbl.find string_table s)
+    with Not_found ->
+      let id = next_id () in
+      Hashtbl.add string_table s id;
+      Offset_string id
+        
 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 module Gen = Dwarfgenaux (struct 
+    let file_loc = gnu_file_loc
+    let string_entry = gnu_string_entry
+  end) in
   let defs,(ty,locs),sec = Hashtbl.fold (fun  id t (acc,bcc,sec) -> 
     let s = match t with
     | GlobalVariable _ -> var_section
     | Function f -> sec_name (get_opt_val f.fun_atom) in
-    let t,bcc = definition_to_entry gnu_file_loc bcc id t in
+    let t,bcc = Gen.definition_to_entry bcc id t in
     t::acc,bcc,StringSet.add s sec) definitions ([],(IntSet.empty,[]),StringSet.empty) in
-  let types = gen_types gnu_file_loc ty in
+  let types = Gen.gen_types ty in
   let cp = {
-    compile_unit_name = !file_name;
+    compile_unit_name = gnu_string_entry !file_name;
     compile_unit_low_pc = low_pc;
-    compile_unit_high_pc = high_pc; 
+    compile_unit_high_pc = high_pc;
+    compile_unit_dir = gnu_string_entry (Sys.getcwd ());
+    compile_unit_prod_name = gnu_string_entry prod_name;
   } in
   let cp = new_entry (next_id ()) (DW_TAG_compile_unit cp) in
   let cp = add_children cp (types@defs) in
   let loc_pc = if StringSet.cardinal sec > 1 then None else Some low_pc in
-  Gnu (cp,(loc_pc,locs))
+  let string_table = Hashtbl.fold (fun s i acc -> (i,s)::acc) string_table [] in
+  Gnu (cp,(loc_pc,locs),string_table)