From 2bf69a09c20c52685ce3c1933577b9aaa5e38e51 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 9 Nov 2017 14:27:23 +0100 Subject: Removed no longer used function. Bug 22525 --- x86/TargetPrinter.ml | 28 ---------------------------- 1 file changed, 28 deletions(-) (limited to 'x86') 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 = -- cgit