Merge branch 'master' into json_export

28 files changed, 381 insertions, 317 deletions

diff --git a/arm/Machregs.v b/arm/Machregs.v
index f373b434..f46f2904 100644
--- a/arm/Machregs.v
+++ b/arm/Machregs.v
@@ -10,6 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+Require Import String.
 Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
@@ -75,6 +76,28 @@ End IndexedMreg.
 
 Definition is_stack_reg (r: mreg) : bool := false.
 
+(** ** Names of registers *)
+
+Local Open Scope string_scope.
+
+Definition register_names :=
+  ("R0", R0) ::  ("R1", R1) ::  ("R2", R2) ::  ("R3", R3) ::
+  ("R4", R4) ::  ("R5", R5) ::  ("R6", R6) ::  ("R7", R7) ::
+  ("R8", R8) ::  ("R9", R9) ::  ("R10", R10) :: ("R11", R11) ::
+  ("R12", R12) ::
+  ("F0", F0) ::  ("F1", F1) ::  ("F2", F2) :: ("F3", F3) ::
+  ("F4", F4) ::  ("F5", F5) ::  ("F6", F6) :: ("F7", F7) ::
+  ("F8", F8) ::  ("F9", F9) ::  ("F10", F10) :: ("F11", F11) ::
+  ("F12", F12) ::("F13", F13) ::("F14", F14) :: ("F15", F15) :: nil.
+
+Definition register_by_name (s: string) : option mreg :=
+  let fix assoc (l: list (string * mreg)) : option mreg :=
+    match l with
+    | nil => None
+    | (s1, r1) :: l' => if string_dec s s1 then Some r1 else assoc l'
+    end
+  in assoc register_names.
+
 (** ** Destroyed registers, preferred registers *)
 
 Definition destroyed_by_op (op: operation): list mreg :=
@@ -95,9 +118,20 @@ Definition destroyed_by_cond (cond: condition): list mreg :=
 Definition destroyed_by_jumptable: list mreg :=
   nil.
 
+Fixpoint destroyed_by_clobber (cl: list string): list mreg :=
+  match cl with
+  | nil => nil
+  | c1 :: cl =>
+      match register_by_name c1 with
+      | Some r => r :: destroyed_by_clobber cl
+      | None   => destroyed_by_clobber cl
+      end
+  end.
+
 Definition destroyed_by_builtin (ef: external_function): list mreg :=
   match ef with
   | EF_memcpy sz al => if zle sz 32 then F7 :: nil else R2 :: R3 :: R12 :: nil
+  | EF_inline_asm txt sg clob => destroyed_by_clobber clob
   | _ => nil
   end.
 
diff --git a/arm/Machregsaux.ml b/arm/Machregsaux.ml
index 44e6b192..d59ec8b8 100644
--- a/arm/Machregsaux.ml
+++ b/arm/Machregsaux.ml
@@ -12,41 +12,24 @@
 
 (** Auxiliary functions on machine registers *)
 
+open Camlcoq
 open Machregs
 
-let register_names = [
-  ("R0", R0);  ("R1", R1);  ("R2", R2);  ("R3", R3);
-  ("R4", R4);  ("R5", R5);  ("R6", R6);  ("R7", R7);
-  ("R8", R8);  ("R9", R9);  ("R10", R10); ("R11", R11);
-  ("R12", R12);
-  ("F0", F0);  ("F1", F1);  ("F2", F2); ("F3", F3);
-  ("F4", F4);  ("F5", F5);  ("F6", F6); ("F7", F7);
-  ("F8", F8);  ("F9", F9);  ("F10", F10); ("F11", F11);
-  ("F12", F12);("F13", F13);("F14", F14); ("F15", F15)
-]
+let register_names : (mreg, string) Hashtbl.t = Hashtbl.create 31
+
+let _ =
+  List.iter
+    (fun (s, r) -> Hashtbl.add register_names r (camlstring_of_coqstring s))
+    Machregs.register_names
 
 let scratch_register_names = [ "R14" ]
 
 let name_of_register r =
-  let rec rev_assoc = function
-  | [] -> None
-  | (a, b) :: rem -> if b = r then Some a else rev_assoc rem
-  in rev_assoc register_names
+  try Some (Hashtbl.find register_names r) with Not_found -> None
 
 let register_by_name s =
-  try
-    Some(List.assoc (String.uppercase s) register_names)
-  with Not_found ->
-    None
+  Machregs.register_by_name (coqstring_of_camlstring (String.uppercase s))
 
 let can_reserve_register r =
   List.mem r Conventions1.int_callee_save_regs
   || List.mem r Conventions1.float_callee_save_regs
-
-let mregs_of_clobber idl =
-  List.fold_left
-    (fun l c ->
-      match register_by_name (Camlcoq.extern_atom c) with
-      | Some r -> r :: l
-      | None -> l)
-    [] idl
diff --git a/arm/Machregsaux.mli b/arm/Machregsaux.mli
index f0feec96..d4877a62 100644
--- a/arm/Machregsaux.mli
+++ b/arm/Machregsaux.mli
@@ -16,4 +16,3 @@ val name_of_register: Machregs.mreg -> string option
 val register_by_name: string -> Machregs.mreg option
 val scratch_register_names: string list
 val can_reserve_register: Machregs.mreg -> bool
-val mregs_of_clobber: Camlcoq.atom list -> Machregs.mreg list
diff --git a/arm/PrintOp.ml b/arm/PrintOp.ml
index 96d13943..886f6de3 100644
--- a/arm/PrintOp.ml
+++ b/arm/PrintOp.ml
@@ -52,6 +52,14 @@ let print_condition reg pp = function
       fprintf pp "%a %sf 0.0" reg r1 (comparison_name c)
   | (Cnotcompfzero c, [r1]) ->
       fprintf pp "%a not(%sf) 0.0" reg r1 (comparison_name c)
+  | (Ccompfs c, [r1;r2]) ->
+      fprintf pp "%a %sfs %a" reg r1 (comparison_name c) reg r2
+  | (Cnotcompfs c, [r1;r2]) ->
+      fprintf pp "%a not(%sfs) %a" reg r1 (comparison_name c) reg r2
+  | (Ccompfszero c, [r1]) ->
+      fprintf pp "%a %sfs 0.0" reg r1 (comparison_name c)
+  | (Cnotcompfszero c, [r1]) ->
+      fprintf pp "%a not(%sfs) 0.0" reg r1 (comparison_name c)
   | _ ->
       fprintf pp "<bad condition>"
 
@@ -59,6 +67,7 @@ let print_operation reg pp = function
   | Omove, [r1] -> reg pp r1
   | Ointconst n, [] -> fprintf pp "%ld" (camlint_of_coqint n)
   | Ofloatconst n, [] -> fprintf pp "%F" (camlfloat_of_coqfloat n)
+  | Osingleconst n, [] -> fprintf pp "%Ff" (camlfloat_of_coqfloat32 n)
   | Oaddrsymbol(id, ofs), [] ->
       fprintf pp "\"%s\" + %ld" (extern_atom id) (camlint_of_coqint ofs)
   | Oaddrstack ofs, [] ->
@@ -100,9 +109,21 @@ let print_operation reg pp = function
   | Osubf, [r1;r2] -> fprintf pp "%a -f %a" reg r1 reg r2
   | Omulf, [r1;r2] -> fprintf pp "%a *f %a" reg r1 reg r2
   | Odivf, [r1;r2] -> fprintf pp "%a /f %a" reg r1 reg r2
+  | Onegfs, [r1] -> fprintf pp "negfs(%a)" reg r1
+  | Oabsfs, [r1] -> fprintf pp "absfs(%a)" reg r1
+  | Oaddfs, [r1;r2] -> fprintf pp "%a +fs %a" reg r1 reg r2
+  | Osubfs, [r1;r2] -> fprintf pp "%a -fs %a" reg r1 reg r2
+  | Omulfs, [r1;r2] -> fprintf pp "%a *fs %a" reg r1 reg r2
+  | Odivfs, [r1;r2] -> fprintf pp "%a /fs %a" reg r1 reg r2
   | Osingleoffloat, [r1] -> fprintf pp "singleoffloat(%a)" reg r1
   | Ointoffloat, [r1] -> fprintf pp "intoffloat(%a)" reg r1
+  | Ointuoffloat, [r1] -> fprintf pp "intuoffloat(%a)" reg r1
   | Ofloatofint, [r1] -> fprintf pp "floatofint(%a)" reg r1
+  | Ofloatofintu, [r1] -> fprintf pp "floatofintu(%a)" reg r1
+  | Ointofsingle, [r1] -> fprintf pp "intofsingle(%a)" reg r1
+  | Ointuofsingle, [r1] -> fprintf pp "intuofsingle(%a)" reg r1
+  | Osingleofint, [r1] -> fprintf pp "singleofint(%a)" reg r1
+  | Osingleofintu, [r1] -> fprintf pp "singleofintu(%a)" reg r1
   | Omakelong, [r1;r2] -> fprintf pp "makelong(%a,%a)" reg r1 reg r2
   | Olowlong, [r1] -> fprintf pp "lowlong(%a)" reg r1
   | Ohighlong, [r1] -> fprintf pp "highlong(%a)" reg r1
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index c77572db..505c3265 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -300,7 +300,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
 (* Emit .file / .loc debugging directives *)
        
     let print_file_line oc file line =
-      PrintAnnot.print_file_line oc comment file line
+      print_file_line oc comment file line
         
     let print_location oc loc =
       if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc)
@@ -320,12 +320,12 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
           (int_of_string (Str.matched_group 2 txt))
       end else begin
         fprintf oc "%s annotation: " comment;
-        PrintAnnot.print_annot_stmt preg "sp" oc txt targs args
+        print_annot_stmt preg "sp" oc txt targs args
       end
           
     let print_annot_val oc txt args res =
       fprintf oc "%s annotation: " comment;
-      PrintAnnot.print_annot_val preg oc txt args;
+      print_annot_val preg oc txt args;
       match args, res with
       | [IR src], [IR dst] ->
           if dst = src then 0 else (fprintf oc "	mov	%a, %a\n" ireg dst ireg src; 1)
@@ -1005,7 +1005,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
               print_annot_val oc (extern_atom txt) args res
           | EF_inline_asm(txt, sg, clob) ->
               fprintf oc "%s begin inline assembly\n\t" comment;
-              PrintAnnot.print_inline_asm preg oc (extern_atom txt) sg args res;
+              print_inline_asm preg oc (extern_atom txt) sg args res;
               fprintf oc "%s end inline assembly\n" comment;
               5 (* hoping this is an upper bound...  *)
           | _ ->
diff --git a/backend/Bounds.v b/backend/Bounds.v
index 7528b66e..04c1328d 100644
--- a/backend/Bounds.v
+++ b/backend/Bounds.v
@@ -87,8 +87,6 @@ Section BOUNDS.
 
 Variable f: function.
 
-Parameter mregs_of_clobber: list ident -> list mreg.
-
 (** In the proof of the [Stacking] pass, we only need to bound the
   registers written by an instruction.  Therefore, this function
   returns these registers, ignoring registers used only as
@@ -103,7 +101,6 @@ Definition regs_of_instr (i: instruction) : list mreg :=
   | Lstore chunk addr args src => nil
   | Lcall sig ros => nil
   | Ltailcall sig ros => nil
-  | Lbuiltin (EF_inline_asm txt typs clob) args res => res ++ mregs_of_clobber clob
   | Lbuiltin ef args res => res ++ destroyed_by_builtin ef
   | Lannot ef args => nil
   | Llabel lbl => nil
@@ -354,9 +351,7 @@ Proof.
 (* call *)
   eapply size_arguments_bound; eauto.
 (* builtin *)
-  apply H1. destruct e; apply in_or_app; auto.
-  change (destroyed_by_builtin (EF_inline_asm text sg clobbers)) with (@nil mreg) in H2.
-  simpl in H2; tauto.
+  apply H1. apply in_or_app; auto.
 (* annot *)
   apply H0. rewrite slots_of_locs_charact; auto. 
 Qed.
diff --git a/backend/PrintAnnot.ml b/backend/PrintAnnot.ml
deleted file mode 100644
index 88f5d8d6..00000000
--- a/backend/PrintAnnot.ml
+++ /dev/null
@@ -1,182 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(* Printing annotations in asm syntax *)
-
-open Printf
-open Datatypes
-open Integers
-open Floats
-open Camlcoq
-open AST
-open Memdata
-open Asm
-
-(** All files used in the debug entries *)
-module StringSet = Set.Make(String)
-let all_files : StringSet.t ref = ref StringSet.empty
-let add_file file =
-  all_files := StringSet.add file !all_files
-
-
-(** Line number annotations *)
-
-let filename_info : (string, int * Printlines.filebuf option) Hashtbl.t
-                  = Hashtbl.create 7
-
-let last_file = ref ""
-
-let reset_filenames () =
-  Hashtbl.clear filename_info; last_file := ""
-
-let close_filenames () =
-  Hashtbl.iter
-    (fun file (num, fb) ->
-       match fb with Some b -> Printlines.close b | None -> ())
-    filename_info;
-  reset_filenames()
-
-let enter_filename f =
-  let num = Hashtbl.length filename_info + 1 in
-  let filebuf =
-    if !Clflags.option_S || !Clflags.option_dasm then begin
-      try Some (Printlines.openfile f)
-      with Sys_error _ -> None
-    end else None in
-  Hashtbl.add filename_info f (num, filebuf);
-  (num, filebuf)
-
-(* Add file and line debug location, using GNU assembler-style DWARF2
-   directives *)
-
-let print_file_line oc pref file line =
-  if !Clflags.option_g && file <> "" then begin
-    let (filenum, filebuf) =
-      try
-        Hashtbl.find filename_info file
-      with Not_found ->
-        let (filenum, filebuf as res) = enter_filename file in
-        fprintf oc "	.file	%d %S\n" filenum file;
-        res in
-    fprintf oc "	.loc	%d %d\n" filenum line;
-    match filebuf with
-    | None -> ()
-    | Some fb -> Printlines.copy oc pref fb line line
-  end
-
-(* Add file and line debug location, using DWARF2 directives in the style
-   of Diab C 5 *)
-
-let print_file_line_d2 oc pref file line =
-  if !Clflags.option_g && file <> "" then begin
-    let (_, filebuf) =
-      try
-        Hashtbl.find filename_info file
-      with Not_found ->
-        enter_filename file in
-    if file <> !last_file then begin
-      fprintf oc "	.d2file	%S\n" file;
-      last_file := file
-    end;
-    fprintf oc "	.d2line	%d\n" line;
-    match filebuf with
-    | None -> ()
-    | Some fb -> Printlines.copy oc pref fb line line
-  end
-
-(** "True" annotations *)
-
-let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*"
-
-let rec print_annot print_preg sp_reg_name oc = function
-  | AA_base x -> print_preg oc x
-  | AA_int n -> fprintf oc "%ld" (camlint_of_coqint n)
-  | AA_long n -> fprintf oc "%Ld" (camlint64_of_coqint n)
-  | AA_float n -> fprintf oc "%.18g" (camlfloat_of_coqfloat n)
-  | AA_single n -> fprintf oc "%.18g" (camlfloat_of_coqfloat32 n)
-  | AA_loadstack(chunk, ofs) ->
-      fprintf oc "mem(%s + %ld, %ld)"
-         sp_reg_name
-         (camlint_of_coqint ofs)
-         (camlint_of_coqint (size_chunk chunk))
-  | AA_addrstack ofs ->
-      fprintf oc "(%s + %ld)"
-         sp_reg_name
-         (camlint_of_coqint ofs)
-  | AA_loadglobal(chunk, id, ofs) ->
-      fprintf oc "mem(\"%s\" + %ld, %ld)"
-         (extern_atom id)
-         (camlint_of_coqint ofs)
-         (camlint_of_coqint (size_chunk chunk))
-  | AA_addrglobal(id, ofs) ->
-      fprintf oc "(\"%s\" + %ld)"
-         (extern_atom id)
-         (camlint_of_coqint ofs)
-  | AA_longofwords(hi, lo) ->
-      fprintf oc "(%a * 0x100000000 + %a)"
-        (print_annot print_preg sp_reg_name) hi
-        (print_annot print_preg sp_reg_name) lo
-
-let print_annot_text print_preg sp_reg_name oc txt args =
-  let print_fragment = function
-  | Str.Text s ->
-      output_string oc s
-  | Str.Delim "%%" ->
-      output_char oc '%'
-  | Str.Delim s ->
-      let n = int_of_string (String.sub s 1 (String.length s - 1)) in
-      try
-        print_annot print_preg sp_reg_name oc (List.nth args (n-1))
-      with Failure _ ->
-        fprintf oc "<bad parameter %s>" s in
-  List.iter print_fragment (Str.full_split re_annot_param txt);
-  fprintf oc "\n"
-
-let print_annot_stmt print_preg sp_reg_name oc txt tys args =
-  print_annot_text print_preg sp_reg_name oc txt args
-
-let print_annot_val print_preg oc txt args =
-  print_annot_text print_preg "<internal error>" oc txt
-    (List.map (fun r -> AA_base r) args)
-
-(** Inline assembly *)
-
-let re_asm_param = Str.regexp "%%\\|%[0-9]+"
-
-let print_inline_asm print_preg oc txt sg args res =
-  let operands =
-    if sg.sig_res = None then args else res @ args in
-  let print_fragment = function
-  | Str.Text s ->
-      output_string oc s
-  | Str.Delim "%%" ->
-      output_char oc '%'
-  | Str.Delim s ->
-      let n = int_of_string (String.sub s 1 (String.length s - 1)) in
-      try
-        print_preg oc (List.nth operands n)
-      with Failure _ ->
-        fprintf oc "<bad parameter %s>" s in
-  List.iter print_fragment (Str.full_split re_asm_param txt);
-  fprintf oc "\n"
-
-
-(** Print CompCert version and command-line as asm comment *)
-
-let print_version_and_options oc comment =
-  fprintf oc "%s File generated by CompCert %s\n" comment Configuration.version;
-  fprintf oc "%s Command line:" comment;
-  for i = 1 to Array.length Sys.argv - 1 do
-    fprintf oc " %s" Sys.argv.(i)
-  done;
-  fprintf oc "\n"
-
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index 0438a40f..e91b4e03 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -130,12 +130,12 @@ module Printer(Target:TARGET) =
 let print_program oc p db =
   let module Target = (val (sel_target ()):TARGET) in
   let module Printer = Printer(Target) in
-  PrintAnnot.reset_filenames ();
-  PrintAnnot.print_version_and_options oc Target.comment;
+  reset_filenames ();
+  print_version_and_options oc Target.comment;
   Target.print_prologue oc;
   List.iter (Printer.print_globdef oc) p.prog_defs;
   Target.print_epilogue oc;
-  PrintAnnot.close_filenames ();
+  close_filenames ();
   if !Clflags.option_g && Configuration.advanced_debug then
     begin
       match db with
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 8bc961ef..497760c1 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -16,6 +16,7 @@ open Asm
 open Camlcoq
 open DwarfTypes
 open Datatypes
+open Memdata
 open Printf
 open Sections
 
@@ -140,3 +141,162 @@ let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$"
 (* Basic printing functions *)
 let coqint oc n =
   fprintf oc "%ld" (camlint_of_coqint n)
+
+(* Printing annotations in asm syntax *)
+(** All files used in the debug entries *)
+module StringSet = Set.Make(String)
+let all_files : StringSet.t ref = ref StringSet.empty
+let add_file file =
+  all_files := StringSet.add file !all_files
+
+
+let filename_info : (string, int * Printlines.filebuf option) Hashtbl.t
+                  = Hashtbl.create 7
+
+let last_file = ref ""
+
+let reset_filenames () =
+  Hashtbl.clear filename_info; last_file := ""
+
+let close_filenames () =
+  Hashtbl.iter
+    (fun file (num, fb) ->
+       match fb with Some b -> Printlines.close b | None -> ())
+    filename_info;
+  reset_filenames()
+
+let enter_filename f =
+  let num = Hashtbl.length filename_info + 1 in
+  let filebuf =
+    if !Clflags.option_S || !Clflags.option_dasm then begin
+      try Some (Printlines.openfile f)
+      with Sys_error _ -> None
+    end else None in
+  Hashtbl.add filename_info f (num, filebuf);
+  (num, filebuf)
+
+(* Add file and line debug location, using GNU assembler-style DWARF2
+   directives *)
+
+let print_file_line oc pref file line =
+  if !Clflags.option_g && file <> "" then begin
+    let (filenum, filebuf) =
+      try
+        Hashtbl.find filename_info file
+      with Not_found ->
+        let (filenum, filebuf as res) = enter_filename file in
+        fprintf oc "	.file	%d %S\n" filenum file;
+        res in
+    fprintf oc "	.loc	%d %d\n" filenum line;
+    match filebuf with
+    | None -> ()
+    | Some fb -> Printlines.copy oc pref fb line line
+  end
+
+(* Add file and line debug location, using DWARF2 directives in the style
+   of Diab C 5 *)
+
+let print_file_line_d2 oc pref file line =
+  if !Clflags.option_g && file <> "" then begin
+    let (_, filebuf) =
+      try
+        Hashtbl.find filename_info file
+      with Not_found ->
+        enter_filename file in
+    if file <> !last_file then begin
+      fprintf oc "	.d2file	%S\n" file;
+      last_file := file
+    end;
+    fprintf oc "	.d2line	%d\n" line;
+    match filebuf with
+    | None -> ()
+    | Some fb -> Printlines.copy oc pref fb line line
+  end
+
+					    
+(** "True" annotations *)
+
+let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*"
+
+let rec print_annot print_preg sp_reg_name oc = function
+  | AA_base x -> print_preg oc x
+  | AA_int n -> fprintf oc "%ld" (camlint_of_coqint n)
+  | AA_long n -> fprintf oc "%Ld" (camlint64_of_coqint n)
+  | AA_float n -> fprintf oc "%.18g" (camlfloat_of_coqfloat n)
+  | AA_single n -> fprintf oc "%.18g" (camlfloat_of_coqfloat32 n)
+  | AA_loadstack(chunk, ofs) ->
+      fprintf oc "mem(%s + %ld, %ld)"
+         sp_reg_name
+         (camlint_of_coqint ofs)
+         (camlint_of_coqint (size_chunk chunk))
+  | AA_addrstack ofs ->
+      fprintf oc "(%s + %ld)"
+         sp_reg_name
+         (camlint_of_coqint ofs)
+  | AA_loadglobal(chunk, id, ofs) ->
+      fprintf oc "mem(\"%s\" + %ld, %ld)"
+         (extern_atom id)
+         (camlint_of_coqint ofs)
+         (camlint_of_coqint (size_chunk chunk))
+  | AA_addrglobal(id, ofs) ->
+      fprintf oc "(\"%s\" + %ld)"
+         (extern_atom id)
+         (camlint_of_coqint ofs)
+  | AA_longofwords(hi, lo) ->
+      fprintf oc "(%a * 0x100000000 + %a)"
+        (print_annot print_preg sp_reg_name) hi
+        (print_annot print_preg sp_reg_name) lo
+
+let print_annot_text print_preg sp_reg_name oc txt args =
+  let print_fragment = function
+  | Str.Text s ->
+      output_string oc s
+  | Str.Delim "%%" ->
+      output_char oc '%'
+  | Str.Delim s ->
+      let n = int_of_string (String.sub s 1 (String.length s - 1)) in
+      try
+        print_annot print_preg sp_reg_name oc (List.nth args (n-1))
+      with Failure _ ->
+        fprintf oc "<bad parameter %s>" s in
+  List.iter print_fragment (Str.full_split re_annot_param txt);
+  fprintf oc "\n"
+
+let print_annot_stmt print_preg sp_reg_name oc txt tys args =
+  print_annot_text print_preg sp_reg_name oc txt args
+
+let print_annot_val print_preg oc txt args =
+  print_annot_text print_preg "<internal error>" oc txt
+    (List.map (fun r -> AA_base r) args)
+
+(** Inline assembly *)
+
+let re_asm_param = Str.regexp "%%\\|%[0-9]+"
+
+let print_inline_asm print_preg oc txt sg args res =
+  let operands =
+    if sg.sig_res = None then args else res @ args in
+  let print_fragment = function
+  | Str.Text s ->
+      output_string oc s
+  | Str.Delim "%%" ->
+      output_char oc '%'
+  | Str.Delim s ->
+      let n = int_of_string (String.sub s 1 (String.length s - 1)) in
+      try
+        print_preg oc (List.nth operands n)
+      with Failure _ ->
+        fprintf oc "<bad parameter %s>" s in
+  List.iter print_fragment (Str.full_split re_asm_param txt);
+  fprintf oc "\n"
+
+
+(** Print CompCert version and command-line as asm comment *)
+
+let print_version_and_options oc comment =
+  fprintf oc "%s File generated by CompCert %s\n" comment Configuration.version;
+  fprintf oc "%s Command line:" comment;
+  for i = 1 to Array.length Sys.argv - 1 do
+    fprintf oc " %s" Sys.argv.(i)
+  done;
+  fprintf oc "\n"
diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml
index c286e946..aa4efc53 100644
--- a/backend/Regalloc.ml
+++ b/backend/Regalloc.ml
@@ -585,13 +585,11 @@ let add_interfs_instr g instr live =
           (* like a move *)
           IRC.add_pref g arg res
       | EF_inline_asm(txt, sg, clob), _, _ ->
-          (* clobbered regs interfere with live set
-             and also with res and args for GCC compatibility *)
+          (* clobbered regs interfere with res and args for GCC compatibility *)
           List.iter (fun c ->
-            match Machregsaux.register_by_name (extern_atom c) with
+            match Machregs.register_by_name c with
             | None -> ()
             | Some mr ->
-                add_interfs_destroyed g across [mr];
                 add_interfs_list_mreg g args mr;
                 if sg.sig_res <> None then add_interfs_list_mreg g res mr)
             clob          
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 94f13aa1..6ecdb14e 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -847,7 +847,7 @@ let convertAsm loc env txt outputs inputs clobber =
   let (txt', output', inputs') = 
     ExtendedAsm.transf_asm loc env txt outputs inputs clobber in
   let clobber' =
-    List.map intern_string clobber in
+    List.map (fun s -> coqstring_of_camlstring (String.uppercase s)) clobber in
   let ty_res =
     match output' with None -> TVoid [] | Some e -> e.etyp in
   (* Build the Ebuiltin expression *)
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 39de282b..bde61cc7 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -299,9 +299,9 @@ and extended_asm p txt res args clob =
   begin match clob with
   | [] -> ()
   | c1 :: cl ->
-      fprintf p "@ : @[<hov 0>%S" (extern_atom c1);
+      fprintf p "@ : @[<hov 0>%S" (camlstring_of_coqstring c1);
       List.iter
-        (fun c -> fprintf p ",@ %S" (extern_atom c))
+        (fun c -> fprintf p ",@ %S" (camlstring_of_coqstring c))
         cl;
       fprintf p "@]"
   end;
diff --git a/common/AST.v b/common/AST.v
index 2550844b..08a19789 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -584,7 +584,7 @@ Inductive external_function : Type :=
      (** Another form of annotation that takes one argument, produces
          an event carrying the text and the value of this argument,
          and returns the value of the argument. *)
-  | EF_inline_asm (text: ident) (sg: signature) (clobbers: list ident).
+  | EF_inline_asm (text: ident) (sg: signature) (clobbers: list String.string).
      (** Inline [asm] statements.  Semantically, treated like an
          annotation with no parameters ([EF_annot text nil]).  To be
          used with caution, as it can invalidate the semantic
@@ -642,7 +642,7 @@ Proof.
   generalize ident_eq signature_eq chunk_eq typ_eq zeq Int.eq_dec; intros.
   decide equality.
   apply list_eq_dec. auto.
-  apply list_eq_dec. auto.
+  apply list_eq_dec. apply String.string_dec. 
 Defined.
 Global Opaque external_function_eq.
 
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 10af10a1..fe74a786 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1801,12 +1801,20 @@ let enter_or_refine_ident local loc env s sto ty =
         | None ->
             warning loc "redefinition of '%s' with incompatible type" s; ty in
       let new_sto =
-        if old_sto = Storage_extern then sto else
-        if sto = Storage_extern then old_sto else
-        if old_sto = sto then sto else begin
-          warning loc "redefinition of '%s' with incompatible storage class" s;
-          sto
-        end in
+	(* The only case not allowed is removing static *)
+	match old_sto,sto with
+	| Storage_static,Storage_static
+	| Storage_extern,Storage_extern
+	| Storage_register,Storage_register
+	| Storage_default,Storage_default -> sto
+	| _,Storage_static ->
+	   error loc "static redefinition of '%s' after non-static definition" s; sto
+	| Storage_static,_ -> Storage_static (* Static stays static *)
+	| Storage_extern,_ -> sto
+	| _,Storage_extern -> old_sto
+	| _,Storage_register
+	| Storage_register,_ -> Storage_register
+      in
       (id, new_sto, Env.add_ident env id new_sto new_ty)
   | Some(id, II_enum v) when Env.in_current_scope env id ->
       error loc "illegal redefinition of enumerator '%s'" s;
@@ -1854,7 +1862,7 @@ let enter_decdefs local loc env sto dl =
 let elab_fundef env spec name body loc =
   let (s, sto, inline, ty, env1) = elab_name env spec name in
   if sto = Storage_register then
-    error loc "a function definition cannot have 'register' storage class";
+    fatal_error loc "a function definition cannot have 'register' storage class";
   (* Fix up the type.  We can have params = None but only for an
      old-style parameterless function "int f() {...}" *)
   let ty =
diff --git a/cparser/ExtendedAsm.ml b/cparser/ExtendedAsm.ml
index 94d23102..fbf8d569 100644
--- a/cparser/ExtendedAsm.ml
+++ b/cparser/ExtendedAsm.ml
@@ -161,9 +161,10 @@ let transf_outputs loc env = function
 let check_clobbers loc clob =
   List.iter
     (fun c ->
-      if Machregsaux.register_by_name c <> None
-      || List.mem c Machregsaux.scratch_register_names
-      || c = "memory" || c = "cc"
+      let c' = String.uppercase c in
+      if Machregsaux.register_by_name c' <> None
+      || List.mem c' Machregsaux.scratch_register_names
+      || c' = "MEMORY" || c' = "CC"
       then ()
       else error "%aError: unrecognized asm register clobber '%s'" 
                  formatloc loc c)
diff --git a/debug/CtoDwarf.ml b/debug/CtoDwarf.ml
index b1eea8f3..a352e99f 100644
--- a/debug/CtoDwarf.ml
+++ b/debug/CtoDwarf.ml
@@ -459,7 +459,7 @@ let union_to_dwarf (n,at,m) env gloc =
 
 (* Translate global declarations to there dwarf representation *)
 let globdecl_to_dwarf env (typs,decls) decl =
-  PrintAnnot.add_file (fst decl.gloc);
+  PrintAsmaux.add_file (fst decl.gloc);
   match decl.gdesc with
   | Gtypedef (n,t) -> let ret = typedef_to_dwarf (n,t) decl.gloc in
     typs@ret,decls
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 4c400036..f7e99545 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -77,9 +77,6 @@ Extract Constant Allocation.regalloc => "Regalloc.regalloc".
 (* Linearize *)
 Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux".
 
-(* Bounds *)
-Extract Constant Bounds.mregs_of_clobber => "Machregsaux.mregs_of_clobber".
-
 (* SimplExpr *)
 Extract Constant SimplExpr.first_unused_ident => "Camlcoq.first_unused_ident".
 Extraction Inline SimplExpr.ret SimplExpr.error SimplExpr.bind SimplExpr.bind2.
diff --git a/ia32/Machregs.v b/ia32/Machregs.v
index a9f2b6c4..65e27599 100644
--- a/ia32/Machregs.v
+++ b/ia32/Machregs.v
@@ -69,6 +69,25 @@ End IndexedMreg.
 Definition is_stack_reg (r: mreg) : bool :=
   match r with FP0 => true | _ => false end.
 
+(** ** Names of registers *)
+
+Local Open Scope string_scope.
+
+Definition register_names :=
+  ("EAX", AX) :: ("EBX", BX) :: ("ECX", CX) :: ("EDX", DX) ::
+  ("ESI", SI) :: ("EDI", DI) :: ("EBP", BP) ::
+  ("XMM0", X0) :: ("XMM1", X1) :: ("XMM2", X2) :: ("XMM3", X3) ::
+  ("XMM4", X4) :: ("XMM5", X5) :: ("XMM6", X6) :: ("XMM7", X7) ::
+  ("ST0", FP0) :: nil.
+
+Definition register_by_name (s: string) : option mreg :=
+  let fix assoc (l: list (string * mreg)) : option mreg :=
+    match l with
+    | nil => None
+    | (s1, r1) :: l' => if string_dec s s1 then Some r1 else assoc l'
+    end
+  in assoc register_names.
+
 (** ** Destroyed registers, preferred registers *)
 
 Definition destroyed_by_op (op: operation): list mreg :=
@@ -100,7 +119,15 @@ Definition destroyed_by_cond (cond: condition): list mreg :=
 Definition destroyed_by_jumptable: list mreg :=
   nil.
 
-Local Open Scope string_scope.
+Fixpoint destroyed_by_clobber (cl: list string): list mreg :=
+  match cl with
+  | nil => nil
+  | c1 :: cl =>
+      match register_by_name c1 with
+      | Some r => r :: destroyed_by_clobber cl
+      | None   => destroyed_by_clobber cl
+      end
+  end.
 
 Definition builtin_write16_reversed := ident_of_string "__builtin_write16_reversed".
 Definition builtin_write32_reversed := ident_of_string "__builtin_write32_reversed".
@@ -115,6 +142,7 @@ Definition destroyed_by_builtin (ef: external_function): list mreg :=
       if ident_eq id builtin_write16_reversed
       || ident_eq id builtin_write32_reversed
       then CX :: DX :: nil else nil
+  | EF_inline_asm txt sg clob => destroyed_by_clobber clob
   | _ => nil
   end.
 
diff --git a/ia32/Machregsaux.ml b/ia32/Machregsaux.ml
index 5e98b58b..6485e752 100644
--- a/ia32/Machregsaux.ml
+++ b/ia32/Machregsaux.ml
@@ -12,38 +12,25 @@
 
 (** Auxiliary functions on machine registers *)
 
+open Camlcoq
 open Machregs
 
-let register_names = [
-  ("EAX", AX); ("EBX", BX); ("ECX", CX); ("EDX", DX);
-  ("ESI", SI); ("EDI", DI); ("EBP", BP);
-  ("XMM0", X0); ("XMM1", X1); ("XMM2", X2); ("XMM3", X3);
-  ("XMM4", X4); ("XMM5", X5); ("XMM6", X6); ("XMM7", X7);
-  ("ST0", FP0)
-]
+let register_names : (mreg, string) Hashtbl.t = Hashtbl.create 31
+
+let _ =
+  List.iter
+    (fun (s, r) -> Hashtbl.add register_names r (camlstring_of_coqstring s))
+    Machregs.register_names
 
 let scratch_register_names = []
 
 let name_of_register r =
-  let rec rev_assoc = function
-  | [] -> None
-  | (a, b) :: rem -> if b = r then Some a else rev_assoc rem
-  in rev_assoc register_names
+  try Some (Hashtbl.find register_names r) with Not_found -> None
 
 let register_by_name s =
-  try
-    Some(List.assoc (String.uppercase s) register_names)
-  with Not_found ->
-    None
+  Machregs.register_by_name (coqstring_of_camlstring (String.uppercase s))
 
 let can_reserve_register r =
   List.mem r Conventions1.int_callee_save_regs
   || List.mem r Conventions1.float_callee_save_regs
 
-let mregs_of_clobber idl =
-  List.fold_left
-    (fun l c ->
-      match register_by_name (Camlcoq.extern_atom c) with
-      | Some r -> r :: l
-      | None -> l)
-    [] idl
diff --git a/ia32/Machregsaux.mli b/ia32/Machregsaux.mli
index f0feec96..d4877a62 100644
--- a/ia32/Machregsaux.mli
+++ b/ia32/Machregsaux.mli
@@ -16,4 +16,3 @@ val name_of_register: Machregs.mreg -> string option
 val register_by_name: string -> Machregs.mreg option
 val scratch_register_names: string list
 val can_reserve_register: Machregs.mreg -> bool
-val mregs_of_clobber: Camlcoq.atom list -> Machregs.mreg list
diff --git a/ia32/PrintOp.ml b/ia32/PrintOp.ml
index fb9a7cc5..1f7f4a65 100644
--- a/ia32/PrintOp.ml
+++ b/ia32/PrintOp.ml
@@ -38,6 +38,10 @@ let print_condition reg pp = function
       fprintf pp "%a %sf %a" reg r1 (comparison_name c) reg r2
   | (Cnotcompf c, [r1;r2]) ->
       fprintf pp "%a not(%sf) %a" reg r1 (comparison_name c) reg r2
+  | (Ccompfs c, [r1;r2]) ->
+      fprintf pp "%a %sfs %a" reg r1 (comparison_name c) reg r2
+  | (Cnotcompfs c, [r1;r2]) ->
+      fprintf pp "%a not(%sfs) %a" reg r1 (comparison_name c) reg r2
   | (Cmaskzero n, [r1]) ->
       fprintf pp "%a & 0x%lx == 0" reg r1 (camlint_of_coqint n)
   | (Cmasknotzero n, [r1]) ->
@@ -100,10 +104,18 @@ let print_operation reg pp = function
   | Osubf, [r1;r2] -> fprintf pp "%a -f %a" reg r1 reg r2
   | Omulf, [r1;r2] -> fprintf pp "%a *f %a" reg r1 reg r2
   | Odivf, [r1;r2] -> fprintf pp "%a /f %a" reg r1 reg r2
+  | Onegfs, [r1] -> fprintf pp "negfs(%a)" reg r1
+  | Oabsfs, [r1] -> fprintf pp "absfs(%a)" reg r1
+  | Oaddfs, [r1;r2] -> fprintf pp "%a +fs %a" reg r1 reg r2
+  | Osubfs, [r1;r2] -> fprintf pp "%a -fs %a" reg r1 reg r2
+  | Omulfs, [r1;r2] -> fprintf pp "%a *fs %a" reg r1 reg r2
+  | Odivfs, [r1;r2] -> fprintf pp "%a /fs %a" reg r1 reg r2
   | Osingleoffloat, [r1] -> fprintf pp "singleoffloat(%a)" reg r1
   | Ofloatofsingle, [r1] -> fprintf pp "floatofsingle(%a)" reg r1
   | Ointoffloat, [r1] -> fprintf pp "intoffloat(%a)" reg r1
   | Ofloatofint, [r1] -> fprintf pp "floatofint(%a)" reg r1
+  | Ointofsingle, [r1] -> fprintf pp "intofsingle(%a)" reg r1
+  | Osingleofint, [r1] -> fprintf pp "singleofint(%a)" reg r1
   | Omakelong, [r1;r2] -> fprintf pp "makelong(%a,%a)" reg r1 reg r2
   | Olowlong, [r1] -> fprintf pp "lowlong(%a)" reg r1
   | Ohighlong, [r1] -> fprintf pp "highlong(%a)" reg r1
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
index ca07a172..a53a8fbd 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -323,7 +323,7 @@ module Target(System: SYSTEM):TARGET =
 (* Emit .file / .loc debugging directives *)
 
     let print_file_line oc file line =
-      PrintAnnot.print_file_line oc comment file line
+      print_file_line oc comment file line
 
     let print_location oc loc =
       if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc)
@@ -345,12 +345,12 @@ module Target(System: SYSTEM):TARGET =
           (int_of_string (Str.matched_group 2 txt))
       end else begin
         fprintf oc "%s annotation: " comment;
-        PrintAnnot.print_annot_stmt preg "%esp" oc txt targs args
+        print_annot_stmt preg "%esp" oc txt targs args
       end
 
     let print_annot_val oc txt args res =
       fprintf oc "%s annotation: " comment;
-      PrintAnnot.print_annot_val preg oc txt args;
+      print_annot_val preg oc txt args;
       match args, res with
       | [IR src], [IR dst] ->
           if dst <> src then fprintf oc "	movl	%a, %a\n" ireg src ireg dst
@@ -873,7 +873,7 @@ module Target(System: SYSTEM):TARGET =
               print_annot_val oc (extern_atom txt) args res
           | EF_inline_asm(txt, sg, clob) ->
               fprintf oc "%s begin inline assembly\n\t" comment;
-              PrintAnnot.print_inline_asm preg oc (extern_atom txt) sg args res;
+              print_inline_asm preg oc (extern_atom txt) sg args res;
               fprintf oc "%s end inline assembly\n" comment
           | _ ->
               assert false
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index f7ed7793..3b7cbb76 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -10,6 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+Require Import String.
 Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
@@ -97,6 +98,36 @@ End IndexedMreg.
 
 Definition is_stack_reg (r: mreg) : bool := false.
 
+(** ** Names of registers *)
+
+Local Open Scope string_scope.
+
+Definition register_names :=
+  ("R3", R3) ::  ("R4", R4) ::  ("R5", R5) ::  ("R6", R6) ::
+  ("R7", R7) ::  ("R8", R8) ::  ("R9", R9) ::  ("R10", R10) ::
+  ("R11", R11) :: ("R12", R12) ::
+  ("R14", R14) :: ("R15", R15) :: ("R16", R16) ::
+  ("R17", R17) :: ("R18", R18) :: ("R19", R19) :: ("R20", R20) ::
+  ("R21", R21) :: ("R22", R22) :: ("R23", R23) :: ("R24", R24) ::
+  ("R25", R25) :: ("R26", R26) :: ("R27", R27) :: ("R28", R28) ::
+  ("R29", R29) :: ("R30", R30) :: ("R31", R31) ::
+  ("F0", F0) :: ("F1", F1) ::  ("F2", F2) ::  ("F3", F3) ::  ("F4", F4) ::
+  ("F5", F5) ::  ("F6", F6) ::  ("F7", F7) ::  ("F8", F8) ::
+  ("F9", F9) ::  ("F10", F10) :: ("F11", F11) :: ("F12", F12) ::
+  ("F13", F13) :: ("F14", F14) :: ("F15", F15) ::
+  ("F16", F16) :: ("F17", F17) :: ("F18", F18) :: ("F19", F19) ::
+  ("F20", F20) :: ("F21", F21) :: ("F22", F22) :: ("F23", F23) ::
+  ("F24", F24) :: ("F25", F25) :: ("F26", F26) :: ("F27", F27) ::
+  ("F28", F28) :: ("F29", F29) :: ("F30", F30) :: ("F31", F31) :: nil.
+
+Definition register_by_name (s: string) : option mreg :=
+  let fix assoc (l: list (string * mreg)) : option mreg :=
+    match l with
+    | nil => None
+    | (s1, r1) :: l' => if string_dec s s1 then Some r1 else assoc l'
+    end
+  in assoc register_names.
+
 (** ** Destroyed registers, preferred registers *)
 
 Definition destroyed_by_op (op: operation): list mreg :=
@@ -119,6 +150,16 @@ Definition destroyed_by_cond (cond: condition): list mreg :=
 Definition destroyed_by_jumptable: list mreg :=
   R12 :: nil.
 
+Fixpoint destroyed_by_clobber (cl: list string): list mreg :=
+  match cl with
+  | nil => nil
+  | c1 :: cl =>
+      match register_by_name c1 with
+      | Some r => r :: destroyed_by_clobber cl
+      | None   => destroyed_by_clobber cl
+      end
+  end.
+
 Definition destroyed_by_builtin (ef: external_function): list mreg :=
   match ef with
   | EF_builtin _ _ => F13 :: nil
@@ -128,6 +169,7 @@ Definition destroyed_by_builtin (ef: external_function): list mreg :=
   | EF_vstore_global Mint64 _ _ => R10 :: R11 :: R12 :: nil
   | EF_vstore_global _ _ _ => R11 :: R12 :: nil
   | EF_memcpy _ _ => R11 :: R12 :: F13 :: nil
+  | EF_inline_asm txt sg clob => destroyed_by_clobber clob
   | _ => nil
   end.
 
diff --git a/powerpc/Machregsaux.ml b/powerpc/Machregsaux.ml
index ba111089..8c3017ff 100644
--- a/powerpc/Machregsaux.ml
+++ b/powerpc/Machregsaux.ml
@@ -12,49 +12,24 @@
 
 (** Auxiliary functions on machine registers *)
 
+open Camlcoq
 open Machregs
 
-let register_names = [
-  ("R3", R3);  ("R4", R4);  ("R5", R5);  ("R6", R6);
-  ("R7", R7);  ("R8", R8);  ("R9", R9);  ("R10", R10);
-  ("R11", R11); ("R12", R12);
-  ("R14", R14); ("R15", R15); ("R16", R16);
-  ("R17", R17); ("R18", R18); ("R19", R19); ("R20", R20);
-  ("R21", R21); ("R22", R22); ("R23", R23); ("R24", R24);
-  ("R25", R25); ("R26", R26); ("R27", R27); ("R28", R28);
-  ("R29", R29); ("R30", R30); ("R31", R31);
-  ("F0", F0); ("F1", F1);  ("F2", F2);  ("F3", F3);  ("F4", F4);
-  ("F5", F5);  ("F6", F6);  ("F7", F7);  ("F8", F8);
-  ("F9", F9);  ("F10", F10); ("F11", F11); ("F12", F12);
-  ("F13", F13); ("F14", F14); ("F15", F15);
-  ("F16", F16); ("F17", F17); ("F18", F18); ("F19", F19);
-  ("F20", F20); ("F21", F21); ("F22", F22); ("F23", F23);
-  ("F24", F24); ("F25", F25); ("F26", F26); ("F27", F27);
-  ("F28", F28); ("F29", F29); ("F30", F30); ("F31", F31)
-]
+let register_names : (mreg, string) Hashtbl.t = Hashtbl.create 31
+
+let _ =
+  List.iter
+    (fun (s, r) -> Hashtbl.add register_names r (camlstring_of_coqstring s))
+    Machregs.register_names
 
 let scratch_register_names = [ "R0" ]
 
 let name_of_register r =
-  let rec rev_assoc = function
-  | [] -> None
-  | (a, b) :: rem -> if b = r then Some a else rev_assoc rem
-  in rev_assoc register_names
+  try Some (Hashtbl.find register_names r) with Not_found -> None
 
 let register_by_name s =
-  try
-    Some(List.assoc (String.uppercase s) register_names)
-  with Not_found ->
-    None
+  Machregs.register_by_name (coqstring_of_camlstring (String.uppercase s))
 
 let can_reserve_register r =
   List.mem r Conventions1.int_callee_save_regs
   || List.mem r Conventions1.float_callee_save_regs
-
-let mregs_of_clobber idl =
-  List.fold_left
-    (fun l c ->
-      match register_by_name (Camlcoq.extern_atom c) with
-      | Some r -> r :: l
-      | None -> l)
-    [] idl
diff --git a/powerpc/Machregsaux.mli b/powerpc/Machregsaux.mli
index f0feec96..d4877a62 100644
--- a/powerpc/Machregsaux.mli
+++ b/powerpc/Machregsaux.mli
@@ -16,4 +16,3 @@ val name_of_register: Machregs.mreg -> string option
 val register_by_name: string -> Machregs.mreg option
 val scratch_register_names: string list
 val can_reserve_register: Machregs.mreg -> bool
-val mregs_of_clobber: Camlcoq.atom list -> Machregs.mreg list
diff --git a/powerpc/PrintOp.ml b/powerpc/PrintOp.ml
index 664280f9..b0213014 100644
--- a/powerpc/PrintOp.ml
+++ b/powerpc/PrintOp.ml
@@ -49,6 +49,7 @@ let print_operation reg pp = function
   | Omove, [r1] -> reg pp r1
   | Ointconst n, [] -> fprintf pp "%ld" (camlint_of_coqint n)
   | Ofloatconst n, [] -> fprintf pp "%F" (camlfloat_of_coqfloat n)
+  | Osingleconst n, [] -> fprintf pp "%Ff" (camlfloat_of_coqfloat32 n)
   | Oaddrsymbol(id, ofs), [] ->
       fprintf pp "\"%s\" + %ld" (extern_atom id) (camlint_of_coqint ofs)
   | Oaddrstack ofs, [] ->
@@ -95,7 +96,14 @@ let print_operation reg pp = function
   | Osubf, [r1;r2] -> fprintf pp "%a -f %a" reg r1 reg r2
   | Omulf, [r1;r2] -> fprintf pp "%a *f %a" reg r1 reg r2
   | Odivf, [r1;r2] -> fprintf pp "%a /f %a" reg r1 reg r2
+  | Onegfs, [r1] -> fprintf pp "negfs(%a)" reg r1
+  | Oabsfs, [r1] -> fprintf pp "absfs(%a)" reg r1
+  | Oaddfs, [r1;r2] -> fprintf pp "%a +fs %a" reg r1 reg r2
+  | Osubfs, [r1;r2] -> fprintf pp "%a -fs %a" reg r1 reg r2
+  | Omulfs, [r1;r2] -> fprintf pp "%a *fs %a" reg r1 reg r2
+  | Odivfs, [r1;r2] -> fprintf pp "%a /fs %a" reg r1 reg r2
   | Osingleoffloat, [r1] -> fprintf pp "singleoffloat(%a)" reg r1
+  | Ofloatofsingle, [r1] -> fprintf pp "floatofsingle(%a)" reg r1
   | Ointoffloat, [r1] -> fprintf pp "intoffloat(%a)" reg r1
   | Ofloatofwords, [r1;r2] -> fprintf pp "floatofwords(%a,%a)" reg r1 reg r2
   | Omakelong, [r1;r2] -> fprintf pp "makelong(%a,%a)" reg r1 reg r2
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index b05b29c0..3789d62e 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -132,7 +132,7 @@ module Linux_System : SYSTEM =
 
 
     let print_file_line oc file line =
-      PrintAnnot.print_file_line oc comment file line
+      print_file_line oc comment file line
     
     (* Emit .cfi directives *)      
     let cfi_startproc = cfi_startproc
@@ -203,7 +203,7 @@ module Diab_System : SYSTEM =
       | Section_debug_abbrev -> ".debug_abbrev,,n"
 
     let print_file_line oc file line =
-      PrintAnnot.print_file_line_d2 oc comment file line
+      print_file_line_d2 oc comment file line
 
     (* Emit .cfi directives *)
     let cfi_startproc oc = ()
@@ -240,10 +240,10 @@ module Diab_System : SYSTEM =
           end_addr := label_end;
           fprintf oc "%a:\n" label label_end;
           fprintf oc "	.text\n";
-          PrintAnnot.StringSet.iter (fun file ->
+          StringSet.iter (fun file ->
             let label = new_label () in
             Hashtbl.add filenum file label;
-            fprintf oc ".L%d:	.d2filenum \"%s\"\n" label file) !PrintAnnot.all_files;
+            fprintf oc ".L%d:	.d2filenum \"%s\"\n" label file) !all_files;
           fprintf oc "	.d2_line_end\n"
         end
 
@@ -331,7 +331,7 @@ module Target (System : SYSTEM):TARGET =
           (int_of_string (Str.matched_group 2 txt))
       end else begin
         fprintf oc "%s annotation: " comment;
-        PrintAnnot.print_annot_stmt preg_annot "R1" oc txt targs args
+        print_annot_stmt preg_annot "R1" oc txt targs args
       end
 
     (* Determine if the displacement of a conditional branch fits the short form *)
@@ -652,7 +652,7 @@ module Target (System : SYSTEM):TARGET =
           begin match ef with
           | EF_inline_asm(txt, sg, clob) ->
               fprintf oc "%s begin inline assembly\n\t" comment;
-              PrintAnnot.print_inline_asm preg oc (extern_atom txt) sg args res;
+              print_inline_asm preg oc (extern_atom txt) sg args res;
               fprintf oc "%s end inline assembly\n" comment
           | _ ->
               assert false
diff --git a/test/regression/extasm.c b/test/regression/extasm.c
index 4925392e..00a1cd57 100644
--- a/test/regression/extasm.c
+++ b/test/regression/extasm.c
@@ -1,7 +1,7 @@
 /* Testing extended asm.
    To run the test, compile with -S and grep "TEST" in the generated .s */
 
-int clobbers(int x)
+int clobbers(int x, int z)
 {
   int y;
   asm("TEST0 out:%0 in:%1" : "=r"(y) : "r"(x) : "cc"
@@ -10,10 +10,10 @@ int clobbers(int x)
 #elif defined(__arm__)
       , "r0", "r1", "r4"
 #elif defined(__PPC__)
-      , "r3", "r4", "r31"
+      , "r0", "r3", "r4", "r31"
 #endif
 );
-  return y;
+  return y + z;
 }
 
 int main()