aboutsummaryrefslogtreecommitdiffstats
path: root/arm/TargetPrinter.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2017-11-09 14:27:23 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2017-11-09 14:27:23 +0100
commit2bf69a09c20c52685ce3c1933577b9aaa5e38e51 (patch)
tree322db4cdddcec685fabfef2ce89be382733972c4 /arm/TargetPrinter.ml
parent92ff9919ff370d914e597f3675670516ac71b6dc (diff)
downloadcompcert-kvx-2bf69a09c20c52685ce3c1933577b9aaa5e38e51.tar.gz
compcert-kvx-2bf69a09c20c52685ce3c1933577b9aaa5e38e51.zip
Removed no longer used function. Bug 22525
Diffstat (limited to 'arm/TargetPrinter.ml')
-rw-r--r--arm/TargetPrinter.ml26
1 files changed, 1 insertions, 25 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"