From a6b6bf31121d975c915c01f501618d97df7879fb Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Sat, 9 May 2015 09:00:51 +0200
Subject: 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
---
 cfrontend/PrintCsyntax.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'cfrontend/PrintCsyntax.ml')

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;
-- 
cgit