aboutsummaryrefslogtreecommitdiffstats
path: root/debug/DwarfPrinter.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-08-18 12:50:19 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-08-18 12:50:19 +0200
commitb4846ffadfa3fbb73ffa7d9c43e5218adeece8da (patch)
tree335b09957f37285721efe31dd185e3b50587d563 /debug/DwarfPrinter.ml
parent7fe3c745283dcfd7cd304bca68ae2cc3ea7cd4a5 (diff)
downloadcompcert-kvx-b4846ffadfa3fbb73ffa7d9c43e5218adeece8da.tar.gz
compcert-kvx-b4846ffadfa3fbb73ffa7d9c43e5218adeece8da.zip
Added support for the location of non static global variables.
Diffstat (limited to 'debug/DwarfPrinter.ml')
-rw-r--r--debug/DwarfPrinter.ml8
1 files changed, 7 insertions, 1 deletions
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml
index 67245ca8..70b68634 100644
--- a/debug/DwarfPrinter.ml
+++ b/debug/DwarfPrinter.ml
@@ -74,6 +74,7 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
| None -> ()
| Some (LocConst _) -> add_abbr_entry (0x2,location_const_type_abbr) buf
| Some (LocBlock _) -> add_abbr_entry (0x2,location_block_type_abbr) buf
+ | Some (LocSymbol _) -> add_abbr_entry (0x2,location_block_type_abbr) buf
(* Dwarf entity to string function *)
let abbrev_string_of_entity entity has_sibling =
@@ -294,7 +295,12 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
fprintf oc " .byte 0x%X\n" b
let print_loc oc loc =
- ()
+ match loc with
+ | LocSymbol s ->
+ fprintf oc " .sleb128 5\n";
+ fprintf oc " .byte 3\n";
+ fprintf oc " .4byte %s\n" s
+ | _ -> ()
let print_data_location oc dl =
()