From 0ffd562ae1941e37471ac0c2b8f93bed1de26441 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 9 Oct 2015 11:06:24 +0200 Subject: Filled in the rest of the funciton needed for thte debug info under arm. The name_of_section function no returns the correct name for the debug sections, the prologue and epilogue directives are added and the labels for the live ranges are introduced in the Asmexpand pass. --- ia32/TargetPrinter.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'ia32/TargetPrinter.ml') diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index 19b4b10a..371be558 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -104,6 +104,7 @@ module Cygwin_System : SYSTEM = s (if ex then "xr" else if wr then "d" else "dr") | Section_debug_info _ | Section_debug_loc + | Section_debug_line _ | Section_debug_abbrev -> "" (* Dummy value *) let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) @@ -153,7 +154,8 @@ module ELF_System : SYSTEM = sprintf ".section \"%s\",\"a%s%s\",@progbits" s (if wr then "w" else "") (if ex then "x" else "") | Section_debug_info _ - | Section_debug_loc + | Section_debug_loc + | Section_debug_line _ | Section_debug_abbrev -> "" (* Dummy value *) let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) @@ -207,6 +209,7 @@ module MacOS_System : SYSTEM = (if ex then "regular, pure_instructions" else "regular") | Section_debug_info _ | Section_debug_loc + | Section_debug_line _ | Section_debug_abbrev -> "" (* Dummy value *) let stack_alignment = 16 (* mandatory *) -- cgit From b0c47e12f2bbff0905ad853b90169df16d87f6be Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 9 Oct 2015 16:36:16 +0200 Subject: Filled in missing functions for debug information on ia32. Like for arm and ppc the functions for section names and start and end addresses of compilation units are defined and the print_annot function is moved to Asmexpandaux.ml. --- ia32/TargetPrinter.ml | 47 +++++++++++++++++++++++++++++++---------------- 1 file changed, 31 insertions(+), 16 deletions(-) (limited to 'ia32/TargetPrinter.ml') diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index 371be558..95de40ca 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -102,10 +102,10 @@ module Cygwin_System : SYSTEM = | Section_user(s, wr, ex) -> sprintf ".section \"%s\", \"%s\"\n" s (if ex then "xr" else if wr then "d" else "dr") - | Section_debug_info _ - | Section_debug_loc - | Section_debug_line _ - | Section_debug_abbrev -> "" (* Dummy value *) + | Section_debug_info _ -> ".section .debug_info,\"dr\"" + | Section_debug_loc -> ".section .debug_loc,\"dr\"" + | Section_debug_line _ -> ".section .debug_line,\"dr\"" + | Section_debug_abbrev -> ".section .debug_abbrev,\"dr\"" (* Dummy value *) let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) @@ -153,10 +153,10 @@ module ELF_System : SYSTEM = | Section_user(s, wr, ex) -> sprintf ".section \"%s\",\"a%s%s\",@progbits" s (if wr then "w" else "") (if ex then "x" else "") - | Section_debug_info _ - | Section_debug_loc - | Section_debug_line _ - | Section_debug_abbrev -> "" (* Dummy value *) + | Section_debug_info _ -> ".section .debug_info,\"\",@progbits" + | Section_debug_loc -> ".section .debug_loc,\"\",@progbits" + | Section_debug_line _ -> ".section .debug_line,\"\",@progbits" + | Section_debug_abbrev -> ".section .debug_abbrev,\"\",@progbits" let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) @@ -207,10 +207,11 @@ module MacOS_System : SYSTEM = sprintf ".section \"%s\", %s, %s" (if wr then "__DATA" else "__TEXT") s (if ex then "regular, pure_instructions" else "regular") - | Section_debug_info _ - | Section_debug_loc - | Section_debug_line _ - | Section_debug_abbrev -> "" (* Dummy value *) + | Section_debug_info _ -> ".section __DWARF,__debug_info,regular,debug" + | Section_debug_loc -> ".section __DWARF,__debug_loc,regular,debug" + | Section_debug_line _ -> ".section __DWARF,__debug_line,regular,debug" + | Section_debug_abbrev -> ".section __DWARF,__debug_abbrev,regular,debug" (* Dummy value *) + let stack_alignment = 16 (* mandatory *) @@ -748,9 +749,16 @@ module Target(System: SYSTEM):TARGET = let print_var_info = print_var_info - let print_prologue _ = - need_masks := false - + let print_prologue oc = + need_masks := false; + if !Clflags.option_g then begin + section oc Section_text; + let low_pc = new_label () in + Debug.add_compilation_section_start ".text" low_pc; + fprintf oc "%a:\n" elf_label low_pc; + fprintf oc " .cfi_sections .debug_frame\n" + end + let print_epilogue oc = if !need_masks then begin section oc (Section_const true); @@ -765,7 +773,14 @@ module Target(System: SYSTEM):TARGET = fprintf oc "%a: .long 0x7FFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF\n" raw_symbol "__abss_mask" end; - System.print_epilogue oc + System.print_epilogue oc; + if !Clflags.option_g then begin + let high_pc = new_label () in + Debug.add_compilation_section_end ".text" high_pc; + Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f)); + section oc Section_text; + fprintf oc "%a:\n" elf_label high_pc + end let comment = comment -- cgit From 16315711d815580afa77f93424cc49c7362ab5b8 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 13 Oct 2015 14:57:31 +0200 Subject: Implement the usage of the debug_str section for the gcc backend. GCC prints all string larger than 3 characters in the debug_str section which reduces the size of the debug information since entries containing the same string now map to the same string in the debug_str sections. Bug 17392. --- ia32/TargetPrinter.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'ia32/TargetPrinter.ml') diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index 95de40ca..32e55ec1 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -105,8 +105,9 @@ module Cygwin_System : SYSTEM = | Section_debug_info _ -> ".section .debug_info,\"dr\"" | Section_debug_loc -> ".section .debug_loc,\"dr\"" | Section_debug_line _ -> ".section .debug_line,\"dr\"" - | Section_debug_abbrev -> ".section .debug_abbrev,\"dr\"" (* Dummy value *) - + | Section_debug_abbrev -> ".section .debug_abbrev,\"dr\"" + | Section_debug_str-> assert false (* Should not be used *) + let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) let print_align oc n = @@ -157,6 +158,7 @@ module ELF_System : SYSTEM = | Section_debug_loc -> ".section .debug_loc,\"\",@progbits" | Section_debug_line _ -> ".section .debug_line,\"\",@progbits" | Section_debug_abbrev -> ".section .debug_abbrev,\"\",@progbits" + | Section_debug_str -> ".section .debug_str,\"MS\",@progbits,1" let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) @@ -210,6 +212,7 @@ module MacOS_System : SYSTEM = | Section_debug_info _ -> ".section __DWARF,__debug_info,regular,debug" | Section_debug_loc -> ".section __DWARF,__debug_loc,regular,debug" | Section_debug_line _ -> ".section __DWARF,__debug_line,regular,debug" + | Section_debug_str -> ".section __DWARF,__debug_str,regular,debug" | Section_debug_abbrev -> ".section __DWARF,__debug_abbrev,regular,debug" (* Dummy value *) -- cgit From 60ab550a952c3d9719b2a91ec90c9b58769f6717 Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Wed, 14 Oct 2015 15:07:48 +0200 Subject: bug 17392: remove trailing whitespace in source files --- ia32/TargetPrinter.ml | 84 +++++++++++++++++++++++++-------------------------- 1 file changed, 42 insertions(+), 42 deletions(-) (limited to 'ia32/TargetPrinter.ml') diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index 32e55ec1..1ccfdcba 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -83,13 +83,13 @@ module Cygwin_System : SYSTEM = let raw_symbol oc s = fprintf oc "_%s" s - + let symbol oc symb = raw_symbol oc (extern_atom symb) let label oc lbl = fprintf oc "L%d" lbl - + let name_of_section = function | Section_text -> ".text" | Section_data i | Section_small_data i -> @@ -106,18 +106,18 @@ module Cygwin_System : SYSTEM = | Section_debug_loc -> ".section .debug_loc,\"dr\"" | Section_debug_line _ -> ".section .debug_line,\"dr\"" | Section_debug_abbrev -> ".section .debug_abbrev,\"dr\"" - | Section_debug_str-> assert false (* Should not be used *) - + | Section_debug_str-> assert false (* Should not be used *) + let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) let print_align oc n = fprintf oc " .align %d\n" n - - let print_mov_ra oc rd id = + + let print_mov_ra oc rd id = fprintf oc " movl $%a, %a\n" symbol id ireg rd let print_fun_info _ _ = () - + let print_var_info _ _ = () let print_epilogue _ = () @@ -134,10 +134,10 @@ module Cygwin_System : SYSTEM = (* Printer functions for ELF *) module ELF_System : SYSTEM = struct - + let raw_symbol oc s = fprintf oc "%s" s - + let symbol = elf_symbol let label = elf_label @@ -159,19 +159,19 @@ module ELF_System : SYSTEM = | Section_debug_line _ -> ".section .debug_line,\"\",@progbits" | Section_debug_abbrev -> ".section .debug_abbrev,\"\",@progbits" | Section_debug_str -> ".section .debug_str,\"MS\",@progbits,1" - + let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) - + let print_align oc n = fprintf oc " .align %d\n" n - - let print_mov_ra oc rd id = + + let print_mov_ra oc rd id = fprintf oc " movl $%a, %a\n" symbol id ireg rd let print_fun_info = elf_print_fun_info - + let print_var_info = elf_print_var_info - + let print_epilogue _ = () let print_comm_decl oc name sz al = @@ -186,7 +186,7 @@ module ELF_System : SYSTEM = (* Printer functions for MacOS *) module MacOS_System : SYSTEM = struct - + let raw_symbol oc s = fprintf oc "_%s" s @@ -214,30 +214,30 @@ module MacOS_System : SYSTEM = | Section_debug_line _ -> ".section __DWARF,__debug_line,regular,debug" | Section_debug_str -> ".section __DWARF,__debug_str,regular,debug" | Section_debug_abbrev -> ".section __DWARF,__debug_abbrev,regular,debug" (* Dummy value *) - - + + let stack_alignment = 16 (* mandatory *) - - (* Base-2 log of a Caml integer *) + + (* Base-2 log of a Caml integer *) let rec log2 n = assert (n > 0); if n = 1 then 0 else 1 + log2 (n lsr 1) let print_align oc n = fprintf oc " .align %d\n" (log2 n) - + let indirect_symbols : StringSet.t ref = ref StringSet.empty - let print_mov_ra oc rd id = + let print_mov_ra oc rd id = let id = extern_atom id in indirect_symbols := StringSet.add id !indirect_symbols; fprintf oc " movl L%a$non_lazy_ptr, %a\n" raw_symbol id ireg rd let print_fun_info _ _ = () - + let print_var_info _ _ = () - - let print_epilogue oc = + + let print_epilogue oc = fprintf oc " .section __IMPORT,__pointers,non_lazy_symbol_pointers\n"; StringSet.iter (fun s -> @@ -275,7 +275,7 @@ module Target(System: SYSTEM):TARGET = | Coq_inl n -> let n = camlint_of_coqint n in fprintf oc "%ld" n - | Coq_inr(id, ofs) -> + | Coq_inr(id, ofs) -> let ofs = camlint_of_coqint ofs in if ofs = 0l then symbol oc id @@ -292,13 +292,13 @@ module Target(System: SYSTEM):TARGET = | Cond_e -> "e" | Cond_ne -> "ne" | Cond_b -> "b" | Cond_be -> "be" | Cond_ae -> "ae" | Cond_a -> "a" | Cond_l -> "l" | Cond_le -> "le" | Cond_ge -> "ge" | Cond_g -> "g" - | Cond_p -> "p" | Cond_np -> "np" + | Cond_p -> "p" | Cond_np -> "np" let name_of_neg_condition = function | Cond_e -> "ne" | Cond_ne -> "e" | Cond_b -> "ae" | Cond_be -> "a" | Cond_ae -> "b" | Cond_a -> "be" | Cond_l -> "ge" | Cond_le -> "g" | Cond_ge -> "l" | Cond_g -> "le" - | Cond_p -> "np" | Cond_np -> "p" + | Cond_p -> "np" | Cond_np -> "p" (* Names of sections *) @@ -342,7 +342,7 @@ module Target(System: SYSTEM):TARGET = (* Built-in functions *) -(* Built-ins. They come in two flavors: +(* Built-ins. They come in two flavors: - annotation statements: take their arguments in registers or stack locations; generate no code; - inlined by the compiler: take their arguments in arbitrary @@ -652,7 +652,7 @@ module Target(System: SYSTEM):TARGET = (** Pseudo-instructions *) | Plabel(l) -> fprintf oc "%a:\n" label (transl_label l) - | Pallocframe(sz, ofs_ra, ofs_link) + | Pallocframe(sz, ofs_ra, ofs_link) | Pfreeframe(sz, ofs_ra, ofs_link) -> assert false | Pbuiltin(ef, args, res) -> @@ -670,13 +670,13 @@ module Target(System: SYSTEM):TARGET = | _ -> assert false end - + let print_literal64 oc (lbl, n) = fprintf oc "%a: .quad 0x%Lx\n" label lbl n let print_literal32 oc (lbl, n) = fprintf oc "%a: .long 0x%lx\n" label lbl n - - let print_jumptable oc jmptbl = + + let print_jumptable oc jmptbl = let print_jumptable oc (lbl, tbl) = fprintf oc "%a:" label lbl; List.iter @@ -688,7 +688,7 @@ module Target(System: SYSTEM):TARGET = List.iter (print_jumptable oc) !jumptables; jumptables := [] end - + let print_init oc = function | Init_int8 n -> fprintf oc " .byte %ld\n" (camlint_of_coqint n) @@ -710,7 +710,7 @@ module Target(System: SYSTEM):TARGET = if Z.gt n Z.zero then fprintf oc " .space %s\n" (Z.to_string n) | Init_addrof(symb, ofs) -> - fprintf oc " .long %a\n" + fprintf oc " .long %a\n" symbol_offset (symb, camlint_of_coqint ofs) let print_align = print_align @@ -741,7 +741,7 @@ module Target(System: SYSTEM):TARGET = let print_optional_fun_info _ = () - let get_section_names name = + let get_section_names name = match C2C.atom_sections name with | [t;l;j] -> (t, l, j) | _ -> (Section_text, Section_literal, Section_jumptable) @@ -749,10 +749,10 @@ module Target(System: SYSTEM):TARGET = let reset_constants = reset_constants let print_fun_info = print_fun_info - + let print_var_info = print_var_info - let print_prologue oc = + let print_prologue oc = need_masks := false; if !Clflags.option_g then begin section oc Section_text; @@ -762,7 +762,7 @@ module Target(System: SYSTEM):TARGET = fprintf oc " .cfi_sections .debug_frame\n" end - let print_epilogue oc = + let print_epilogue oc = if !need_masks then begin section oc (Section_const true); (* not Section_literal because not 8-bytes *) @@ -784,13 +784,13 @@ module Target(System: SYSTEM):TARGET = section oc Section_text; fprintf oc "%a:\n" elf_label high_pc end - + let comment = comment let default_falignment = 16 let label = label - + let new_label = new_label end @@ -798,7 +798,7 @@ end let sel_target () = let module S = (val (match Configuration.system with | "macosx" -> (module MacOS_System:SYSTEM) - | "linux" + | "linux" | "bsd" -> (module ELF_System:SYSTEM) | "cygwin" -> (module Cygwin_System:SYSTEM) | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported") ):SYSTEM) in -- cgit From 44845982f412810b0c18067987f2780ef6245fbb Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 15 Oct 2015 09:10:22 +0200 Subject: Use section type also for other targets. Bug 17392. --- ia32/TargetPrinter.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'ia32/TargetPrinter.ml') diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index 1ccfdcba..bd0c1d95 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -757,7 +757,7 @@ module Target(System: SYSTEM):TARGET = if !Clflags.option_g then begin section oc Section_text; let low_pc = new_label () in - Debug.add_compilation_section_start ".text" low_pc; + Debug.add_compilation_section_start Section_text low_pc; fprintf oc "%a:\n" elf_label low_pc; fprintf oc " .cfi_sections .debug_frame\n" end @@ -779,7 +779,7 @@ module Target(System: SYSTEM):TARGET = System.print_epilogue oc; if !Clflags.option_g then begin let high_pc = new_label () in - Debug.add_compilation_section_end ".text" high_pc; + Debug.add_compilation_section_end Section_text high_pc; Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f)); section oc Section_text; fprintf oc "%a:\n" elf_label high_pc -- cgit From 1e52bb2001964d87086cea00d0cb779e270b99ce Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 15 Oct 2015 13:15:28 +0200 Subject: First step to implemente address ranges for the gnu backend. In contrast to the dcc, the gcc uses address ranges to express non-contiguous range of addresses. As a first step we set the start and end addresses for the different address ranges for the compilation unit by using the start and end addresses of functions. Bug 17392. --- ia32/TargetPrinter.ml | 6 ------ 1 file changed, 6 deletions(-) (limited to 'ia32/TargetPrinter.ml') diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index bd0c1d95..e9238a99 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -756,9 +756,6 @@ module Target(System: SYSTEM):TARGET = need_masks := false; if !Clflags.option_g then begin section oc Section_text; - let low_pc = new_label () in - Debug.add_compilation_section_start Section_text low_pc; - fprintf oc "%a:\n" elf_label low_pc; fprintf oc " .cfi_sections .debug_frame\n" end @@ -778,11 +775,8 @@ module Target(System: SYSTEM):TARGET = end; System.print_epilogue oc; if !Clflags.option_g then begin - let high_pc = new_label () in - Debug.add_compilation_section_end Section_text high_pc; Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f)); section oc Section_text; - fprintf oc "%a:\n" elf_label high_pc end let comment = comment -- cgit From 24b4159b6a29328c529e0e59405e03ea192aa99e Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 16 Oct 2015 13:06:09 +0200 Subject: Implemented the usage of DW_AT_ranges for non-contiguous address ranges. The gcc produces DW_AT_ranges for non-contiguous address ranges, like compilation units containing functions which are placed in different ELF-sections or lexical scopes that are split up. With this commit CompCert also uses this DWARF v3 feature for gnu backend based targets. In order to ensure backward compability a flag is added which avoids this and produces debug info in DWARF v2 format. Bug 17392. --- ia32/TargetPrinter.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'ia32/TargetPrinter.ml') diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index e9238a99..e38fa1db 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -106,6 +106,7 @@ module Cygwin_System : SYSTEM = | Section_debug_loc -> ".section .debug_loc,\"dr\"" | Section_debug_line _ -> ".section .debug_line,\"dr\"" | Section_debug_abbrev -> ".section .debug_abbrev,\"dr\"" + | Section_debug_abbrev -> ".section .debug_ranges,\"dr\"" | Section_debug_str-> assert false (* Should not be used *) let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) @@ -158,6 +159,7 @@ module ELF_System : SYSTEM = | Section_debug_loc -> ".section .debug_loc,\"\",@progbits" | Section_debug_line _ -> ".section .debug_line,\"\",@progbits" | Section_debug_abbrev -> ".section .debug_abbrev,\"\",@progbits" + | Section_debug_ranges -> ".section .debug_ranges,\"\",@progbits" | Section_debug_str -> ".section .debug_str,\"MS\",@progbits,1" let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) @@ -213,7 +215,8 @@ module MacOS_System : SYSTEM = | Section_debug_loc -> ".section __DWARF,__debug_loc,regular,debug" | Section_debug_line _ -> ".section __DWARF,__debug_line,regular,debug" | Section_debug_str -> ".section __DWARF,__debug_str,regular,debug" - | Section_debug_abbrev -> ".section __DWARF,__debug_abbrev,regular,debug" (* Dummy value *) + | Section_debug_abbrev -> ".section __DWARF,__debug_ranges,regular,debug" + | Section_debug_abbrev -> ".section __DWARF,__debug_abbrev,regular,debug" let stack_alignment = 16 (* mandatory *) -- cgit From 32ab0017ba80baafd03230960beaf3e256637369 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 16 Oct 2015 13:14:15 +0200 Subject: Fixed typos in the arm and ia32 section printing. Bug 17392 --- ia32/TargetPrinter.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'ia32/TargetPrinter.ml') diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index e38fa1db..84ddb134 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -106,7 +106,7 @@ module Cygwin_System : SYSTEM = | Section_debug_loc -> ".section .debug_loc,\"dr\"" | Section_debug_line _ -> ".section .debug_line,\"dr\"" | Section_debug_abbrev -> ".section .debug_abbrev,\"dr\"" - | Section_debug_abbrev -> ".section .debug_ranges,\"dr\"" + | Section_debug_ranges -> ".section .debug_ranges,\"dr\"" | Section_debug_str-> assert false (* Should not be used *) let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) @@ -215,7 +215,7 @@ module MacOS_System : SYSTEM = | Section_debug_loc -> ".section __DWARF,__debug_loc,regular,debug" | Section_debug_line _ -> ".section __DWARF,__debug_line,regular,debug" | Section_debug_str -> ".section __DWARF,__debug_str,regular,debug" - | Section_debug_abbrev -> ".section __DWARF,__debug_ranges,regular,debug" + | Section_debug_ranges -> ".section __DWARF,__debug_ranges,regular,debug" | Section_debug_abbrev -> ".section __DWARF,__debug_abbrev,regular,debug" -- cgit From 5c408186f4f66d6955c9d2a682cec36231343f87 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 15:32:04 +0200 Subject: Also replace extern_atom by camlstring_of_coqstring for ia32/TargetPrinter.ml. Bug 17450 --- ia32/TargetPrinter.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'ia32/TargetPrinter.ml') diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index 84ddb134..4c436c45 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -662,13 +662,13 @@ module Target(System: SYSTEM):TARGET = begin match ef with | EF_annot(txt, targs) -> fprintf oc "%s annotation: " comment; - print_annot_text preg "%esp" oc (extern_atom txt) args + print_annot_text preg "%esp" oc (camlstring_of_coqstring txt) args | EF_debug(kind, txt, targs) -> print_debug_info comment print_file_line preg "%esp" oc (P.to_int kind) (extern_atom txt) args | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n\t" comment; - print_inline_asm preg oc (extern_atom txt) sg args res; + print_inline_asm preg oc (camlstring_of_coqstring txt) sg args res; fprintf oc "%s end inline assembly\n" comment | _ -> assert false -- cgit