diff options
Diffstat (limited to 'powerpc/TargetPrinter.ml')
-rw-r--r-- | powerpc/TargetPrinter.ml | 25 |
1 files changed, 9 insertions, 16 deletions
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 3d183972..ae9d4191 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -14,12 +14,11 @@ open Printf open Fileinfo -open Datatypes +open !Datatypes open Maps open Camlcoq open Sections open AST -open Memdata open Asm open PrintAsmaux @@ -72,6 +71,14 @@ let float_reg_name = function | FPR24 -> "24" | FPR25 -> "25" | FPR26 -> "26" | FPR27 -> "27" | FPR28 -> "28" | FPR29 -> "29" | FPR30 -> "30" | FPR31 -> "31" +let num_crbit = function + | CRbit_0 -> 0 + | CRbit_1 -> 1 + | CRbit_2 -> 2 + | CRbit_3 -> 3 + | CRbit_6 -> 6 + + let label = elf_label module Linux_System : SYSTEM = @@ -303,9 +310,6 @@ module Target (System : SYSTEM):TARGET = (* Basic printing functions *) let symbol = symbol - let raw_symbol oc s = - fprintf oc "%s" s - let label = label let label_low oc lbl = @@ -314,14 +318,6 @@ module Target (System : SYSTEM):TARGET = let label_high oc lbl = fprintf oc ".L%d@ha" lbl - - let num_crbit = function - | CRbit_0 -> 0 - | CRbit_1 -> 1 - | CRbit_2 -> 2 - | CRbit_3 -> 3 - | CRbit_6 -> 6 - let crbit oc bit = fprintf oc "%d" (num_crbit bit) @@ -340,9 +336,6 @@ module Target (System : SYSTEM):TARGET = | FR r -> fprintf oc "f%s" (float_reg_name r) | _ -> assert false - let print_location oc loc = - if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc) - (* Encoding masks for rlwinm instructions *) let rolm_mask n = |