diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2022-08-25 15:49:21 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-09-03 10:41:30 +0200 |
| commit | d5fda4fde03571e6dbc46729767924be7ac41920 (patch) | |
| tree | e69a0b4b4b6ee32b0fa8f655194f024739405cbd /backend/PrintAsmaux.ml | |
| parent | ad6467099ac7147040c59c022635e61370168568 (diff) | |
| download | compcert-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 'backend/PrintAsmaux.ml')
| -rw-r--r-- | backend/PrintAsmaux.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 2241edfd..f5741113 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -33,7 +33,6 @@ module type TARGET = val cfi_startproc: out_channel -> unit val print_instructions: out_channel -> coq_function -> unit val cfi_endproc: out_channel -> unit - val print_literal64 : out_channel -> int64 -> int -> unit val print_jumptable: out_channel -> section_name -> unit val section: out_channel -> section_name -> unit val name_of_section: section_name -> string |