Added symbol functions for printing of the location for global variables.

3 files changed, 24 insertions, 24 deletions

diff --git a/debug/CtoDwarf.ml b/debug/CtoDwarf.ml
index 99b77e6f..ee594d9e 100644
--- a/debug/CtoDwarf.ml
+++ b/debug/CtoDwarf.ml
@@ -164,15 +164,14 @@ and fun_to_dwarf_tag rt args =
         false,[u],[]
     | Some [] -> true,[],[]
     | Some l ->
-        let c,e = mmap (fun acc (_,t) ->
+        let c,e = mmap (fun acc (i,t) ->
           let t,e = type_to_dwarf t in
           let fp =
             {
+             formal_parameter_id = i.stamp;
              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
@@ -301,12 +300,11 @@ let glob_var_to_dwarf (s,n,t,_) gloc =
    | Storage_static -> false
    | _ -> true) in
    let decl = {
+     variable_id = n.stamp;
      variable_file_loc = (Some gloc);
      variable_declaration = Some at_decl;
      variable_external = Some ext;
-     variable_location = if ext then Some (LocSymbol n.name) else None;
      variable_name = n.name;
-     variable_segment = None;
      variable_type = i;
    } in
    let decl = new_entry (DW_TAG_variable decl) in
@@ -322,9 +320,9 @@ let fundef_to_dwarf f gloc =
   | Storage_static -> false
   | _ -> true) in
   let fdef = {
+    subprogram_id = f.fd_name.stamp;
     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;
@@ -333,11 +331,10 @@ let fundef_to_dwarf f gloc =
     let t,e = type_to_dwarf t in
     let fp =
       {
+       formal_parameter_id = p.stamp;
        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
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml
index 70b68634..85efea6e 100644
--- a/debug/DwarfPrinter.ml
+++ b/debug/DwarfPrinter.ml
@@ -128,9 +128,9 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
           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_location  (get_location e.formal_parameter_id) buf;
           add_attr_some e.formal_parameter_name add_name;
-          add_location e.formal_parameter_segment buf;
+          add_location  (get_segment_location e.formal_parameter_id) buf;
           add_type buf;
           add_attr_some e.formal_parameter_variable_parameter (add_abbr_entry (0x4b,variable_parameter_type_abbr))
       | DW_TAG_label _ ->
@@ -203,9 +203,9 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
           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_location  (get_location e.variable_id) buf;
           add_name buf;
-          add_location e.variable_segment buf;
+          add_location  (get_segment_location e.variable_id) buf;
           add_type buf
       | DW_TAG_volatile_type _ ->
           prologue 0x35;
@@ -299,7 +299,7 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
       | LocSymbol s ->
           fprintf oc "	.sleb128	5\n";
           fprintf oc "	.byte		3\n";
-          fprintf oc "	.4byte		%s\n" s
+          fprintf oc "	.4byte		%a\n" symbol s
       | _ ->   ()
 
     let print_data_location oc dl =
@@ -365,9 +365,9 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
     let print_formal_parameter oc fp =
       print_file_loc oc fp.formal_parameter_file_loc;
       print_opt_value oc fp.formal_parameter_artificial print_flag;
-      print_opt_value oc fp.formal_parameter_location print_loc;
+      print_opt_value oc (get_location fp.formal_parameter_id) print_loc;
       print_opt_value oc fp.formal_parameter_name print_string;
-      print_opt_value oc fp.formal_parameter_segment print_loc;
+      print_opt_value oc  (get_segment_location fp.formal_parameter_id) print_loc;
       print_ref oc fp.formal_parameter_type;
       print_opt_value oc fp.formal_parameter_variable_parameter print_flag
 
@@ -406,7 +406,7 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
       let addr = 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;
+      print_opt_value oc (get_frame_base sp.subprogram_id) print_loc;
       print_opt_value oc addr print_subprogram_addr;
       print_string oc sp.subprogram_name;
       print_flag oc sp.subprogram_prototyped;
@@ -439,9 +439,9 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
       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_opt_value oc (get_location var.variable_id) print_loc;
       print_string oc var.variable_name;
-      print_opt_value oc var.variable_segment print_loc;
+      print_opt_value oc (get_segment_location var.variable_id) print_loc;
       print_ref oc var.variable_type
 
     let print_volatile_type oc vt =
diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli
index 4852e550..174f2403 100644
--- a/debug/DwarfTypes.mli
+++ b/debug/DwarfTypes.mli
@@ -13,6 +13,7 @@
 (* Types used for writing dwarf debug information *)
 
 open Sections
+open Camlcoq
 
 (* Basic types for the value of attributes *)
 
@@ -37,7 +38,7 @@ type address = int
 type block = string
 
 type location_value =
-  | LocSymbol of string
+  | LocSymbol of atom
   | LocConst of constant
   | LocBlock of block
 
@@ -93,11 +94,10 @@ type dw_tag_enumerator =
 
 type dw_tag_formal_parameter =
     {
+     formal_parameter_id:                 int;
      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;
    }
@@ -141,9 +141,9 @@ type dw_tag_structure_type =
 
 type dw_tag_subprogram =
     {
+     subprogram_id:         int;
      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;
@@ -184,12 +184,11 @@ type dw_tag_unspecified_parameter =
 
 type dw_tag_variable =
     {
+     variable_id:          int;
      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;
    }
 
@@ -270,4 +269,8 @@ module type DWARF_TARGET=
     val get_stmt_list_addr: unit -> int    
     val name_of_section: section_name -> string
     val get_fun_addr: string -> (int * int) option
+    val get_location: int -> location_value option
+    val get_segment_location: int -> location_value option
+    val get_frame_base: int -> location_value option
+    val symbol: out_channel -> atom -> unit
   end