aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--arm/TargetPrinter.ml26
-rw-r--r--backend/PrintAsmaux.ml1
-rw-r--r--powerpc/TargetPrinter.ml30
-rw-r--r--riscV/TargetPrinter.ml21
-rw-r--r--x86/TargetPrinter.ml28
5 files changed, 1 insertions, 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 =
generated by cgit (git 2.34.1) at 2024-06-11 18:37:22 +0000