diff options
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/Asmexpand.ml | 12 | ||||
| -rw-r--r-- | powerpc/TargetPrinter.ml | 9 |
2 files changed, 8 insertions, 13 deletions
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index bf7e4c3e..fb569a00 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -563,7 +563,7 @@ let num_crbit = function | CRbit_3 -> 3 | CRbit_6 -> 6 -let expand_instruction_simple instr = +let expand_instruction instr = match instr with | Pallocframe(sz, ofs,retofs) -> let variadic = (!current_function).fn_sig.sig_cc.cc_vararg in @@ -687,19 +687,13 @@ let translate_annot annot = | [] -> None | a::_ -> aux a) -let expand_scope id lbl oldscopes newscopes = - let opening = List.filter (fun a -> not (List.mem a oldscopes)) newscopes - and closing = List.filter (fun a -> not (List.mem a newscopes)) oldscopes in - List.iter (fun i -> Debug.open_scope id i lbl) opening; - List.iter (fun i -> Debug.close_scope id i lbl) closing - let expand_function id fn = try set_current_function fn; if !Clflags.option_g then - expand_debug id translate_annot expand_instruction_simple fn.fn_code + expand_debug id translate_annot expand_instruction fn.fn_code else - List.iter expand_instruction_simple fn.fn_code; + List.iter expand_instruction fn.fn_code; Errors.OK (get_current_function ()) with Error s -> Errors.Error (Errors.msg (coqstring_of_camlstring s)) diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 530e269d..0f0ed357 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -126,7 +126,9 @@ module Linux_System : SYSTEM = | Section_debug_info _ -> ".section .debug_info,\"\",@progbits" | Section_debug_abbrev -> ".section .debug_abbrev,\"\",@progbits" | Section_debug_loc -> ".section .debug_loc,\"\",@progbits" - + | Section_debug_line _ -> ".section .debug_line,\"\",@progbits\n" + + let section oc sec = let name = name_of_section sec in assert (name <> "COMM"); @@ -146,9 +148,7 @@ module Linux_System : SYSTEM = let cfi_rel_offset = cfi_rel_offset let print_prologue oc = - if !Clflags.option_g then - begin - (* TODO print file *) + if !Clflags.option_g then begin section oc Section_text; let low_pc = new_label () in Debug.add_compilation_section_start ".text" low_pc; @@ -220,6 +220,7 @@ module Diab_System : SYSTEM = | Section_debug_info s -> sprintf ".section .debug_info%s,,n" (if s <> ".text" then s else "") | Section_debug_abbrev -> ".section .debug_abbrev,,n" | Section_debug_loc -> ".section .debug_loc,,n" + | Section_debug_line s -> sprintf ".section .debug_line.%s,,n\n" s; let section oc sec = let name = name_of_section sec in |