aboutsummaryrefslogtreecommitdiffstats
path: root/riscV
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2022-08-25 15:49:21 +0200
committerXavier Leroy <xavier.leroy@college-de-france.fr>2022-09-03 10:41:30 +0200
commitd5fda4fde03571e6dbc46729767924be7ac41920 (patch)
treee69a0b4b4b6ee32b0fa8f655194f024739405cbd /riscV
parentad6467099ac7147040c59c022635e61370168568 (diff)
downloadcompcert-d5fda4fde03571e6dbc46729767924be7ac41920.tar.gz
compcert-d5fda4fde03571e6dbc46729767924be7ac41920.zip
More simplifications for literal printing
Use the same code to split 64 bit literals into two 32 bit halfs as is used for 64 bit initialization data and print them in PrintAsm. This removes the need for a target specific printing function for 64 bit literals.
Diffstat (limited to 'riscV')
-rw-r--r--riscV/TargetPrinter.ml5
1 files changed, 0 insertions, 5 deletions
diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml
index 52a6853a..373bd1a5 100644
--- a/riscV/TargetPrinter.ml
+++ b/riscV/TargetPrinter.ml
@@ -130,11 +130,6 @@ module Target : TARGET =
let section oc sec =
fprintf oc " %s\n" (name_of_section sec)
-(* Associate labels to floating-point constants and to symbols. *)
-
- let print_literal64 oc n lbl =
- fprintf oc "%a: .quad 0x%Lx\n" label lbl n
-
(* Generate code to load the address of id + ofs in register r *)
let loadsymbol oc r id ofs =