From a6b6bf31121d975c915c01f501618d97df7879fb Mon Sep 17 00:00:00 2001 From: Xavier Leroy 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/C2C.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'cfrontend/C2C.ml') 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 *) -- cgit