diff options
| -rw-r--r-- | debug/DwarfAbbrvPrinter.ml (renamed from debug/DwarfPrinter.ml) | 22 | ||||
| -rw-r--r-- | driver/Driver.ml | 2 | ||||
| -rw-r--r-- | powerpc/PrintDiab.ml | 34 |
3 files changed, 11 insertions, 47 deletions
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfAbbrvPrinter.ml index 3e804532..4a3ae5b1 100644 --- a/debug/DwarfPrinter.ml +++ b/debug/DwarfAbbrvPrinter.ml @@ -14,7 +14,7 @@ open DwarfTypes open DwarfUtil -module type DWARF_DEFS = +module type DWARF_ABBRV_DEFS = sig (* Functions used for the printing of the dwarf abbreviations *) val string_of_byte: bool -> string @@ -52,15 +52,11 @@ module type DWARF_DEFS = val data_location_ref_type_abbr: int val bound_const_type_abbr: int val bound_ref_type_abbr: int - (* Functions for the printing of the debug information *) - val info_section_start: out_channel -> unit - val print_entry: out_channel -> dw_entry -> int -> unit - val info_section_end: out_channel -> unit end -module DwarfPrinter(Defs:DWARF_DEFS) : +module DwarfAbbrvPrinter(Defs:DWARF_ABBRV_DEFS) : sig - val print_debug: out_channel -> dw_entry -> unit + val print_debug_abbrv: out_channel -> dw_entry -> unit end = (struct @@ -307,16 +303,8 @@ module DwarfPrinter(Defs:DWARF_DEFS) : Defs.abbrv_epilogue oc) abbrvs; Defs.abbrv_section_end oc - let print_debug oc entry = + let print_debug_abbrv oc entry = compute_abbrv entry; - print_abbrv oc; - Defs.info_section_start oc; - entry_iter_sib (fun sib entry -> - let has_sib = match sib with - | None -> false - | Some _ -> true in - let abbrv = get_abbrv entry has_sib in - Defs.print_entry oc entry abbrv) entry; - Defs.info_section_end oc + print_abbrv oc end) diff --git a/driver/Driver.ml b/driver/Driver.ml index fec87420..6ba30d74 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -499,7 +499,7 @@ let cmdline_actions = Exact "-fall", Self (fun _ -> set_all language_support_options); Exact "-fnone", Self (fun _ -> unset_all language_support_options); (* Debugging options *) - Exact "-g", Self (fun s -> option_g := true; push_linker_arg s); + Exact "-g", Self (fun s -> option_g := true); (* Code generation options -- more below *) Exact "-O0", Self (fun _ -> unset_all optimization_options); Exact "-O", Self (fun _ -> set_all optimization_options); diff --git a/powerpc/PrintDiab.ml b/powerpc/PrintDiab.ml index d8083168..d73c7691 100644 --- a/powerpc/PrintDiab.ml +++ b/powerpc/PrintDiab.ml @@ -16,7 +16,7 @@ open Printf open Datatypes open DwarfTypes open DwarfUtil -open DwarfPrinter +open DwarfAbbrvPrinter open Camlcoq open Sections open Asm @@ -96,21 +96,14 @@ module Diab_System = fprintf oc " .xopt asm-debug-on\n" - module DwarfDefs = - (struct + module AbbrvPrinter = DwarfAbbrvPrinter(struct let string_of_byte value = - if value then - " .byte 0x1\n" - else - - " .byte 0x0\n" + Printf.sprintf " .byte %s\n" (if value then "0x1" else "0x2") let string_of_abbrv_entry v = Printf.sprintf " .uleb128 %d\n" v - + let abbrv_start_addr = ref (-1) - - let debug_end_addr = ref (-1) let get_abbrv_start_addr () = !abbrv_start_addr @@ -161,23 +154,6 @@ module Diab_System = fprintf oc " .uleb128 0\n"; fprintf oc " .uleb128 0\n" - let info_section_start oc = - fprintf oc " .section .debug_info,,n\n"; - let debug_start = new_label () - and debug_end = new_label () in - debug_end_addr:= debug_end; - fprintf oc " .4byte %a-%a\n" label debug_end label debug_start; - fprintf oc "%a:\n" label debug_start; - fprintf oc " .2byte 0x2\n"; - fprintf oc " .4byte %a\n" label !abbrv_start_addr; - fprintf oc " .1byte %d\n" !Machine.config.Machine.sizeof_ptr - - let info_section_end oc = - fprintf oc "%a\n" label !debug_end_addr - - let print_entry oc entry abbrv = - () - - end:DWARF_DEFS) + end) end:SYSTEM) |