From 2bf69a09c20c52685ce3c1933577b9aaa5e38e51 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 9 Nov 2017 14:27:23 +0100 Subject: Removed no longer used function. Bug 22525 --- arm/TargetPrinter.ml | 26 +------------------------- backend/PrintAsmaux.ml | 1 - powerpc/TargetPrinter.ml | 30 ------------------------------ riscV/TargetPrinter.ml | 21 --------------------- x86/TargetPrinter.ml | 28 ---------------------------- 5 files changed, 1 insertion(+), 105 deletions(-) diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 1493f9fc..0cd3c908 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -51,10 +51,7 @@ struct let symbol = elf_symbol - let symbol_offset oc (symb, ofs) = - symbol oc symb; - let ofs = camlint_of_coqint ofs in - if ofs <> 0l then fprintf oc " + %ld" ofs + let symbol_offset = elf_symbol_offset let int_reg_name = function | IR0 -> "r0" | IR1 -> "r1" | IR2 -> "r2" | IR3 -> "r3" @@ -839,27 +836,6 @@ struct (* Data *) - let print_init oc = function - | Init_int8 n -> - fprintf oc " .byte %ld\n" (camlint_of_coqint n) - | Init_int16 n -> - fprintf oc " .short %ld\n" (camlint_of_coqint n) - | Init_int32 n -> - fprintf oc " .word %ld\n" (camlint_of_coqint n) - | Init_int64 n -> - fprintf oc " .quad %Ld\n" (camlint64_of_coqint n) - | Init_float32 n -> - fprintf oc " .word 0x%lx %s %.15g \n" (camlint_of_coqint (Floats.Float32.to_bits n)) - comment (camlfloat_of_coqfloat32 n) - | Init_float64 n -> - fprintf oc " .quad %Ld %s %.18g\n" (camlint64_of_coqint (Floats.Float.to_bits n)) - comment (camlfloat_of_coqfloat n) - | Init_space n -> - if Z.gt n Z.zero then - fprintf oc " .space %s\n" (Z.to_string n) - | Init_addrof(symb, ofs) -> - fprintf oc " .word %a\n" symbol_offset (symb, ofs) - let print_prologue oc = fprintf oc " .syntax unified\n"; fprintf oc " .arch %s\n" diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 257b1ba4..3a2e0e7d 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -28,7 +28,6 @@ module type TARGET = val print_comm_symb: out_channel -> Z.t -> P.t -> int -> unit val print_var_info: out_channel -> P.t -> unit val print_fun_info: out_channel -> P.t -> unit - val print_init: out_channel -> init_data -> unit val reset_constants: unit -> unit val get_section_names: P.t -> section_name * section_name * section_name val print_file_line: out_channel -> string -> int -> unit diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index f15e6ec1..cf1d4aba 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -910,36 +910,6 @@ module Target (System : SYSTEM):TARGET = let print_literal32 oc n lbl = fprintf oc "%a: .long 0x%lx\n" label lbl n - let print_init oc = function - | Init_int8 n -> - fprintf oc " .byte %ld\n" (camlint_of_coqint n) - | Init_int16 n -> - fprintf oc " .short %ld\n" (camlint_of_coqint n) - | Init_int32 n -> - fprintf oc " .long %ld\n" (camlint_of_coqint n) - | Init_int64 n -> - let b = camlint64_of_coqint n in - fprintf oc " .long 0x%Lx, 0x%Lx\n" - (Int64.shift_right_logical b 32) - (Int64.logand b 0xFFFFFFFFL) - | Init_float32 n -> - fprintf oc " .long 0x%lx %s %.18g\n" - (camlint_of_coqint (Floats.Float32.to_bits n)) - comment (camlfloat_of_coqfloat32 n) - | Init_float64 n -> - let b = camlint64_of_coqint (Floats.Float.to_bits n) in - fprintf oc " .long 0x%Lx, 0x%Lx %s %.18g\n" - (Int64.shift_right_logical b 32) - (Int64.logand b 0xFFFFFFFFL) - comment (camlfloat_of_coqfloat n) - | Init_space n -> - 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" - symbol_offset (symb, ofs) - - let print_fun_info = elf_print_fun_info let emit_constants oc lit = diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml index 19d8103b..f0ff9637 100644 --- a/riscV/TargetPrinter.ml +++ b/riscV/TargetPrinter.ml @@ -636,27 +636,6 @@ module Target : TARGET = let address = if Archi.ptr64 then ".quad" else ".long" - let print_init oc = function - | Init_int8 n -> - fprintf oc " .byte %ld\n" (camlint_of_coqint n) - | Init_int16 n -> - fprintf oc " .short %ld\n" (camlint_of_coqint n) - | Init_int32 n -> - fprintf oc " .long %ld\n" (camlint_of_coqint n) - | Init_int64 n -> - fprintf oc " .quad %Ld\n" (camlint64_of_coqint n) - | Init_float32 n -> - fprintf oc " .long 0x%lx %s %.15g \n" (camlint_of_coqint (Floats.Float32.to_bits n)) - comment (camlfloat_of_coqfloat n) - | Init_float64 n -> - fprintf oc " .quad %Ld %s %.18g\n" (camlint64_of_coqint (Floats.Float.to_bits n)) - comment (camlfloat_of_coqfloat n) - | Init_space n -> - if Z.gt n Z.zero then - fprintf oc " .space %s\n" (Z.to_string n) - | Init_addrof(symb, ofs) -> - fprintf oc " %s %a\n" address symbol_offset (symb, ofs) - let print_prologue oc = fprintf oc " .option %s\n" (if Archi.pic_code() then "pic" else "nopic"); if !Clflags.option_g then begin diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml index b685c4cb..1525b49b 100644 --- a/x86/TargetPrinter.ml +++ b/x86/TargetPrinter.ml @@ -300,11 +300,6 @@ module Target(System: SYSTEM):TARGET = (* Basic printing functions *) - let symbol_offset oc (symb, ofs) = - symbol oc symb; - let ofs = Z.to_int64 ofs in - if ofs <> 0L then fprintf oc " + %Ld" ofs - let addressing_gen ireg oc (Addrmode(base, shift, cst)) = begin match cst with | Datatypes.Coq_inl n -> @@ -840,29 +835,6 @@ module Target(System: SYSTEM):TARGET = jumptables := [] end - let print_init oc = function - | Init_int8 n -> - fprintf oc " .byte %ld\n" (camlint_of_coqint n) - | Init_int16 n -> - fprintf oc " .short %ld\n" (camlint_of_coqint n) - | Init_int32 n -> - fprintf oc " .long %ld\n" (camlint_of_coqint n) - | Init_int64 n -> - fprintf oc " .quad %Ld\n" (camlint64_of_coqint n) - | Init_float32 n -> - fprintf oc " .long %ld %s %.18g\n" - (camlint_of_coqint (Floats.Float32.to_bits n)) - comment (camlfloat_of_coqfloat32 n) - | Init_float64 n -> - fprintf oc " .quad %Ld %s %.18g\n" - (camlint64_of_coqint (Floats.Float.to_bits n)) - comment (camlfloat_of_coqfloat n) - | Init_space n -> - if Z.gt n Z.zero then - fprintf oc " .space %a\n" z n - | Init_addrof(symb, ofs) -> - fprintf oc " %s %a\n" data_pointer symbol_offset (symb, ofs) - let print_align = print_align let print_comm_symb oc sz name align = -- cgit