Deactivate warning 27 and added back removed code.

The code was mostly there for documentation effort. So warning
27 is deactivated again.
Bug 18349

3 files changed, 12 insertions, 11 deletions

diff --git a/ia32/AsmToJSON.ml b/ia32/AsmToJSON.ml
index 60208fb3..3214491f 100644
--- a/ia32/AsmToJSON.ml
+++ b/ia32/AsmToJSON.ml
@@ -13,4 +13,5 @@
 (* Simple functions to serialize ia32 Asm to JSON *)
 
 (* Dummy function *)
-let p_program _ _ = ()
+let p_program oc prog =
+  ()
diff --git a/ia32/Asmexpand.ml b/ia32/Asmexpand.ml
index f2b6ad90..3a3548f9 100644
--- a/ia32/Asmexpand.ml
+++ b/ia32/Asmexpand.ml
@@ -93,7 +93,7 @@ let global_addr id ofs = Addrmode(None, None, Coq_inr(id, ofs))
 (* Unaligned memory accesses are quite fast on IA32, so use large
    memory accesses regardless of alignment. *)
 
-let expand_builtin_memcpy_small sz _ src dst =
+let expand_builtin_memcpy_small sz al src dst =
   let rec copy src dst sz =
     if sz >= 8 && !Clflags.option_ffpu then begin
 	emit (Pmovq_rm (XMM7, src));
@@ -114,7 +114,7 @@ let expand_builtin_memcpy_small sz _ src dst =
       end in
   copy (addressing_of_builtin_arg src) (addressing_of_builtin_arg dst) sz
 
-let expand_builtin_memcpy_big sz _ src dst =
+let expand_builtin_memcpy_big sz al src dst =
   if src <> BA (IR ESI) then emit (Plea (ESI, addressing_of_builtin_arg src));
   if dst <> BA (IR EDI) then emit (Plea (EDI, addressing_of_builtin_arg dst));
   emit (Pmov_ri (ECX,coqint_of_camlint (Int32.of_int (sz / 4))));
@@ -376,7 +376,7 @@ let expand_builtin_inline name args res =
 
 let expand_instruction instr =
   match instr with
-  | Pallocframe (sz, _, ofs_link) ->
+  | Pallocframe (sz, ofs_ra, ofs_link) ->
      let sz = sp_adjustment sz in
      let addr = linear_addr ESP (coqint_of_camlint (Int32.add sz 4l)) in
      let addr' = linear_addr ESP ofs_link in
@@ -386,13 +386,13 @@ let expand_instruction instr =
      emit (Plea (EDX,addr));
      emit (Pmov_mr (addr',EDX));
      PrintAsmaux.current_function_stacksize := sz
-  | Pfreeframe(sz, _, _) ->
+  | Pfreeframe(sz, ofs_ra, ofs_link) ->
      let sz = sp_adjustment sz in
      emit (Padd_ri (ESP,coqint_of_camlint sz))
   | Pbuiltin (ef,args, res) ->
      begin
        match ef with
-       | EF_builtin(name, _) ->
+       | EF_builtin(name, sg) ->
 	  expand_builtin_inline (camlstring_of_coqstring name) args res
        | EF_vload chunk ->
           expand_builtin_vload chunk args res
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
index 246c01f3..f2358487 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -618,18 +618,18 @@ module Target(System: SYSTEM):TARGET =
       (* Pseudo-instructions *)
       | Plabel(l) ->
           fprintf oc "%a:\n" label (transl_label l)
-      | Pallocframe _
-      | Pfreeframe _ ->
+      | Pallocframe(sz, ofs_ra, ofs_link)
+      | Pfreeframe(sz, ofs_ra, ofs_link) ->
 	 assert false
       | Pbuiltin(ef, args, res) ->
           begin match ef with
-          | EF_annot(txt, _) ->
+          | EF_annot(txt, targs) ->
               fprintf oc "%s annotation: " comment;
               print_annot_text preg "%esp" oc (camlstring_of_coqstring txt) args
-          | EF_debug(kind, txt, _) ->
+          | EF_debug(kind, txt, targs) ->
               print_debug_info comment print_file_line preg "%esp" oc
                                (P.to_int kind) (extern_atom txt) args
-          | EF_inline_asm(txt, sg, _) ->
+          | EF_inline_asm(txt, sg, clob) ->
               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