clightgen: sanitize names of functions and global variables

A "dollar" sign in a function name or a global variable name was producing
incorrect Coq identifiers.  (Issue #319.)

1 files changed, 4 insertions, 4 deletions

diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index b124586a..d86e137a 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -381,7 +381,7 @@ and lblstmts p = function
               (print_option coqZ) lbl stmt s lblstmts ls
 
 let print_function p (id, f) =
-  fprintf p "Definition f_%s := {|@ " (extern_atom id);
+  fprintf p "Definition f_%s := {|@ " (sanitize (extern_atom id));
   fprintf p "  fn_return := %a;@ " typ f.fn_return;
   fprintf p "  fn_callconv := %a;@ " callconv f.fn_callconv;
   fprintf p "  fn_params := %a;@ " (print_list (print_pair ident typ)) f.fn_params;
@@ -402,7 +402,7 @@ let init_data p = function
   | Init_addrof(id,ofs) -> fprintf p "Init_addrof %a %a" ident id coqptrofs ofs
 
 let print_variable p (id, v) =
-  fprintf p "Definition v_%s := {|@ " (extern_atom id);
+  fprintf p "Definition v_%s := {|@ " (sanitize (extern_atom id));
   fprintf p "  gvar_info := %a;@ " typ v.gvar_info;
   fprintf p "  gvar_init := %a;@ " (print_list init_data) v.gvar_init;
   fprintf p "  gvar_readonly := %B;@ " v.gvar_readonly;
@@ -417,12 +417,12 @@ let print_globdef p (id, gd) =
 
 let print_ident_globdef p = function
   | (id, Gfun(Ctypes.Internal f)) ->
-      fprintf p "(%a, Gfun(Internal f_%s))" ident id (extern_atom id)
+      fprintf p "(%a, Gfun(Internal f_%s))" ident id (sanitize (extern_atom id))
   | (id, Gfun(Ctypes.External(ef, targs, tres, cc))) ->
       fprintf p "@[<hov 2>(%a,@ @[<hov 2>Gfun(External %a@ %a@ %a@ %a))@]@]"
         ident id external_function ef typlist targs typ tres callconv cc
   | (id, Gvar v) ->
-      fprintf p "(%a, Gvar v_%s)" ident id (extern_atom id)
+      fprintf p "(%a, Gvar v_%s)" ident id (sanitize (extern_atom id))
 
 (* Composite definitions *)