diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-05-18 09:58:14 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-05-18 09:58:14 +0200 |
commit | 4663ad4b31e351e29a4d8d034ad4a961a48263f1 (patch) | |
tree | d21554c60ed607bf8fdd1476431f9707bf882604 /cfrontend | |
parent | 10def48b639b8e83ae6cc8bf9c14da8c12e98370 (diff) | |
parent | 5d017f110f6c23c29a182465ab7832a944c0ba26 (diff) | |
download | compcert-4663ad4b31e351e29a4d8d034ad4a961a48263f1.tar.gz compcert-4663ad4b31e351e29a4d8d034ad4a961a48263f1.zip |
Merge branch 'master' into json_export
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/C2C.ml | 2 | ||||
-rw-r--r-- | cfrontend/PrintCsyntax.ml | 4 |
2 files changed, 3 insertions, 3 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 *) 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; |