Extended inline asm: revised treatment of clobbered registers.

- Treat clobbered registers as being destroyed by EF_inline_asm builtins
  (which is the truth, semantically).
- To enable the above, represent clobbers as Coq strings rather than idents
  and move register_by_name from Machregsaux.ml to Machregs.v.
- Side benefit: more efficient implementation of Machregsaux.name_of_register.

-# Please enter the commit message for your changes. Lines starting

1 files changed, 4 insertions, 3 deletions

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)