diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-11-09 14:27:23 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-11-09 14:27:23 +0100 |
| commit | 2bf69a09c20c52685ce3c1933577b9aaa5e38e51 (patch) | |
| tree | 322db4cdddcec685fabfef2ce89be382733972c4 /riscV/TargetPrinter.ml | |
| parent | 92ff9919ff370d914e597f3675670516ac71b6dc (diff) | |
| download | compcert-kvx-2bf69a09c20c52685ce3c1933577b9aaa5e38e51.tar.gz compcert-kvx-2bf69a09c20c52685ce3c1933577b9aaa5e38e51.zip | |
Removed no longer used function. Bug 22525
Diffstat (limited to 'riscV/TargetPrinter.ml')
| -rw-r--r-- | riscV/TargetPrinter.ml | 21 |
1 files changed, 0 insertions, 21 deletions
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 |