Code cleanup.

Removed some unused variables, functions etc. and resolved some
problems which occur if all warnings except 3,4,9 and 29 are active.
Bug 18394.

1 files changed, 30 insertions, 37 deletions

diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 3d183972..93d73d5c 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
 
@@ -230,7 +229,7 @@ module Diab_System : SYSTEM =
       let name = name_of_section sec in
       assert (name <> "COMM");
       match sec with
-      | Section_debug_info (Some s) ->
+      | Section_debug_info (Some _) ->
           fprintf oc "	%s\n" name;
           fprintf oc "	.sectionlink	.debug_info\n"
       | _ ->
@@ -240,13 +239,13 @@ module Diab_System : SYSTEM =
       print_file_line_d2 oc comment file line
 
     (* Emit .cfi directives *)
-    let cfi_startproc oc = ()
+    let cfi_startproc _ = ()
 
-    let cfi_endproc oc = ()
+    let cfi_endproc _ = ()
 
-    let cfi_adjust oc delta = ()
+    let cfi_adjust _ _ = ()
 
-    let cfi_rel_offset oc reg ofs = ()
+    let cfi_rel_offset _ _ _ = ()
 
     let debug_section oc sec =
       match sec with
@@ -303,9 +302,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 =
@@ -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 =
@@ -387,7 +380,7 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	addis	%a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c
       | Paddze(r1, r2) ->
           fprintf oc "	addze	%a, %a\n" ireg r1 ireg r2
-      | Pallocframe(sz, ofs, _) ->
+      | Pallocframe _ ->
           assert false
       | Pand_(r1, r2, r3) ->
           fprintf oc "	and.	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
@@ -399,9 +392,9 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	andis.	%a, %a, %a\n" ireg r1 ireg r2 constant c
       | Pb lbl ->
           fprintf oc "	b	%a\n" label (transl_label lbl)
-      | Pbctr sg ->
+      | Pbctr _ ->
           fprintf oc "	bctr\n"
-      | Pbctrl sg ->
+      | Pbctrl _ ->
           fprintf oc "	bctrl\n"
       | Pbdnz lbl ->
           fprintf oc "	bdnz	%a\n" label (transl_label lbl)
@@ -416,9 +409,9 @@ module Target (System : SYSTEM):TARGET =
             fprintf oc "	b	%a\n" label (transl_label lbl);
             fprintf oc "%a:\n" label next
           end
-      | Pbl(s, sg) ->
+      | Pbl(s, _) ->
           fprintf oc "	bl	%a\n" symbol s
-      | Pbs(s, sg) ->
+      | Pbs(s, _) ->
           fprintf oc "	b	%a\n" symbol s
       | Pblr ->
           fprintf oc "	blr\n"
@@ -490,7 +483,7 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	extsh	%a, %a\n" ireg r1 ireg r2
       | Pextsw(r1, r2) ->
           fprintf oc "	extsw	%a, %a\n" ireg r1 ireg r2
-      | Pfreeframe(sz, ofs) ->
+      | Pfreeframe _ ->
           assert false
       | Pfabs(r1, r2) | Pfabss(r1, r2) ->
           fprintf oc "	fabs	%a, %a\n" freg r1 freg r2
@@ -500,17 +493,17 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	fadds	%a, %a, %a\n" freg r1 freg r2 freg r3
       | Pfcmpu(r1, r2) ->
           fprintf oc "	fcmpu	%a, %a, %a\n" creg 0 freg r1 freg r2
-      | Pfcfi(r1, r2) ->
+      | Pfcfi _ ->
           assert false
       | Pfcfid(r1, r2) ->
           fprintf oc "	fcfid	%a, %a\n" freg r1 freg r2
-      | Pfcfiu(r1, r2) ->
+      | Pfcfiu _ ->
           assert false
-      | Pfcti(r1, r2) ->
+      | Pfcti _ ->
           assert false
       | Pfctidz(r1, r2) ->
           fprintf oc "	fctidz	%a, %a\n" freg r1 freg r2
-      | Pfctiu(r1, r2) ->
+      | Pfctiu _ ->
           assert false
       | Pfctiw(r1, r2) ->
           fprintf oc "	fctiw	%a, %a\n" freg r1 freg r2
@@ -520,7 +513,7 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	fdiv	%a, %a, %a\n" freg r1 freg r2 freg r3
       | Pfdivs(r1, r2, r3) ->
           fprintf oc "	fdivs	%a, %a, %a\n" freg r1 freg r2 freg r3
-      | Pfmake(rd, r1, r2) ->
+      | Pfmake _ ->
           assert false
       | Pfmr(r1, r2) ->
           fprintf oc "	fmr	%a, %a\n" freg r1 freg r2
@@ -532,7 +525,7 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	fneg	%a, %a\n" freg r1 freg r2
       | Pfrsp(r1, r2) ->
           fprintf oc "	frsp	%a, %a\n" freg r1 freg r2
-      | Pfxdp(r1, r2) ->
+      | Pfxdp _ ->
           assert false
       | Pfsub(r1, r2, r3) ->
           fprintf oc "	fsub	%a, %a, %a\n" freg r1 freg r2 freg r3
@@ -610,7 +603,7 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	mbar	%ld\n" (camlint_of_coqint mo)
       | Pmfcr(r1) ->
           fprintf oc "	mfcr	%a\n" ireg r1
-      | Pmfcrbit(r1, bit) ->
+      | Pmfcrbit _ ->
           assert false
       | Pmflr(r1) ->
           fprintf oc "	mflr	%a\n" ireg r1
@@ -726,13 +719,13 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "%a:\n" label (transl_label lbl)
       | Pbuiltin(ef, args, res) ->
           begin match ef with
-          | EF_annot(txt, targs) ->
+          | EF_annot(txt, _) ->
               fprintf oc "%s annotation: " comment;
               print_annot_text preg_annot "r1" oc (camlstring_of_coqstring txt) args
-          | EF_debug(kind, txt, targs) ->
+          | EF_debug(kind, txt, _) ->
               print_debug_info comment print_file_line preg_annot "r1" oc
                                (P.to_int kind) (extern_atom txt) args
-          | EF_inline_asm(txt, sg, clob) ->
+          | EF_inline_asm(txt, sg, _) ->
               fprintf oc "%s begin inline assembly\n\t" comment;
               print_inline_asm preg oc (camlstring_of_coqstring txt) sg args res;
               fprintf oc "%s end inline assembly\n" comment
@@ -757,14 +750,14 @@ module Target (System : SYSTEM):TARGET =
        PowerPC instructions.  We can over-approximate. *)
 
     let instr_size = function
-      | Pbf(bit, lbl) -> 2
-      | Pbt(bit, lbl) -> 2
-      | Pbtbl(r, tbl) -> 5
-      | Plfi(r1, c) -> 2
-      | Plfis(r1, c) -> 2
-      | Plabel lbl -> 0
-      | Pbuiltin((EF_annot _ | EF_debug _), args, res) -> 0
-      | Pbuiltin(ef, args, res) -> 3
+      | Pbf _ -> 2
+      | Pbt _ -> 2
+      | Pbtbl _ -> 5
+      | Plfi _ -> 2
+      | Plfis _ -> 2
+      | Plabel _-> 0
+      | Pbuiltin ((EF_annot _ | EF_debug _), _, _) -> 0
+      | Pbuiltin _ -> 3
       | Pcfi_adjust _ | Pcfi_rel_offset _ -> 0
       | _ -> 1