diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2016-03-21 10:18:51 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2016-03-21 10:18:51 +0100 |
| commit | 20eef936dce1ef98b5b422c90cc9e072fb0d75ab (patch) | |
| tree | 2690be164dc36fad63fc0f42e943d0fcb0735532 /powerpc/TargetPrinter.ml | |
| parent | fdf4cac2439a7168bd005efbde4a1f76a00ada66 (diff) | |
| parent | 01e32a075023ce7b037d42d048b1904ba3d9a82b (diff) | |
| download | compcert-20eef936dce1ef98b5b422c90cc9e072fb0d75ab.tar.gz compcert-20eef936dce1ef98b5b422c90cc9e072fb0d75ab.zip | |
Merge pull request #92 from AbsInt/cleanup
This PR activates more OCaml warnings and turns all warnings into errors. Also some unused functions, variables and types are removed.
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 = |