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, 1 insertions, 1 deletions

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 *)