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

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