diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-12-15 16:03:19 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-12-15 16:03:19 +0100 |
| commit | e86596ae60132b0821cb8b15409074e4cd76243a (patch) | |
| tree | 9af775756d597be1bc2110adbf040f4a47d3cf35 /powerpc | |
| parent | 6697f6e69fdf87e2de6f1f1b2846e3453c0e3a11 (diff) | |
| download | compcert-e86596ae60132b0821cb8b15409074e4cd76243a.tar.gz compcert-e86596ae60132b0821cb8b15409074e4cd76243a.zip | |
Added more printing code.
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/PrintDiab.ml | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/powerpc/PrintDiab.ml b/powerpc/PrintDiab.ml index b39e8e7a..0d9f74e6 100644 --- a/powerpc/PrintDiab.ml +++ b/powerpc/PrintDiab.ml @@ -219,7 +219,7 @@ module Diab_System = let print_debug_info oc entry = AbbrvPrinter.print_debug_abbrv oc entry; - let abbrv_start = AbbrvPrinter.get_abbrv_start_addr in + let abbrv_start = AbbrvPrinter.get_abbrv_start_addr () in let debug_start = new_label () in let print_info () = fprintf oc" .section .debug_info,,n\n" in @@ -228,8 +228,13 @@ module Diab_System = let debug_length_start = new_label () in (* Address used for length calculation *) let debug_end = new_label () in fprintf oc " .4byte %a-%a\n" label debug_end label debug_length_start; - fprintf oc "%a\n" label debug_length_start - + fprintf oc "%a\n" label debug_length_start; + fprintf oc " .2byte 0x2\n"; (* Dwarf version *) + fprintf oc " .4byte %a\n" label abbrv_start; (* Offset into the abbreviation *) + fprintf oc " .byte %X\n" !Machine.config.Machine.sizeof_ptr; (* Sizeof pointer type *) + (); + fprintf oc "%a\n" label debug_end; (* End of the debug section *) + fprintf oc " .sleb128 0\n" end:SYSTEM) |