diff options
Diffstat (limited to 'verilog/TargetPrinter.ml')
| -rw-r--r-- | verilog/TargetPrinter.ml | 80 |
1 files changed, 4 insertions, 76 deletions
diff --git a/verilog/TargetPrinter.ml b/verilog/TargetPrinter.ml index f0a54506..8950b8ca 100644 --- a/verilog/TargetPrinter.ml +++ b/verilog/TargetPrinter.ml @@ -131,25 +131,7 @@ module ELF_System : SYSTEM = let label = elf_label - let name_of_section = function - | Section_text -> ".text" - | Section_data i | Section_small_data i -> - if i then ".data" else common_section () - | Section_const i | Section_small_const i -> - if i || (not !Clflags.option_fcommon) then ".section .rodata" else "COMM" - | Section_string -> ".section .rodata" - | Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8" - | Section_jumptable -> ".text" - | 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_info,\"\",@progbits" - | 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" - | Section_ais_annotation -> sprintf ".section \"__compcert_ais_annotations\",\"\",@note" + let name_of_section = fun _ -> assert false let stack_alignment = 16 @@ -189,26 +171,7 @@ module MacOS_System : SYSTEM = let label oc lbl = fprintf oc "L%d" lbl - let name_of_section = function - | Section_text -> ".text" - | Section_data i | Section_small_data i -> - if i || (not !Clflags.option_fcommon) then ".data" else "COMM" - | Section_const i | Section_small_const i -> - if i || (not !Clflags.option_fcommon) then ".const" else "COMM" - | Section_string -> ".const" - | Section_literal -> ".literal8" - | Section_jumptable -> ".text" - | Section_user(s, wr, ex) -> - sprintf ".section \"%s\", %s, %s" - (if wr then "__DATA" else "__TEXT") s - (if ex then "regular, pure_instructions" else "regular") - | 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_ranges -> ".section __DWARF,__debug_ranges,regular,debug" - | Section_debug_abbrev -> ".section __DWARF,__debug_abbrev,regular,debug" - | Section_ais_annotation -> assert false (* Not supported under MacOS *) + let name_of_section = fun _ -> assert false let stack_alignment = 16 (* mandatory *) @@ -248,25 +211,7 @@ module Cygwin_System : SYSTEM = let label oc lbl = fprintf oc "L%d" lbl - let name_of_section = function - | Section_text -> ".text" - | Section_data i | Section_small_data i -> - if i then ".data" else common_section () - | Section_const i | Section_small_const i -> - if i || (not !Clflags.option_fcommon) then ".section .rdata,\"dr\"" else "COMM" - | Section_string -> ".section .rdata,\"dr\"" - | Section_literal -> ".section .rdata,\"dr\"" - | Section_jumptable -> ".text" - | 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_info,\"dr\"" - | Section_debug_loc -> ".section .debug_loc,\"dr\"" - | Section_debug_line _ -> ".section .debug_line,\"dr\"" - | Section_debug_abbrev -> ".section .debug_abbrev,\"dr\"" - | Section_debug_ranges -> ".section .debug_ranges,\"dr\"" - | Section_debug_str-> assert false (* Should not be used *) - | Section_ais_annotation -> assert false (* Not supported for coff binaries *) + let name_of_section = fun _ -> assert false let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) @@ -887,24 +832,7 @@ module Target(System: SYSTEM):TARGET = end let print_epilogue oc = - if !need_masks then begin - section oc (Section_const true); - (* not Section_literal because not 8-bytes *) - print_align oc 16; - fprintf oc "%a: .quad 0x8000000000000000, 0\n" - raw_symbol "__negd_mask"; - fprintf oc "%a: .quad 0x7FFFFFFFFFFFFFFF, 0xFFFFFFFFFFFFFFFF\n" - raw_symbol "__absd_mask"; - fprintf oc "%a: .long 0x80000000, 0, 0, 0\n" - raw_symbol "__negs_mask"; - fprintf oc "%a: .long 0x7FFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF\n" - raw_symbol "__abss_mask" - end; - System.print_epilogue oc; - if !Clflags.option_g then begin - Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f)); - section oc Section_text; - end + assert false let comment = comment |