From 8fbe9863a920f6351a13c5a7f0028b8640b9319d Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 28 Oct 2019 11:20:28 +0100 Subject: 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.) --- exportclight/ExportClight.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'exportclight') 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 "@[(%a,@ @[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 *) -- cgit