diff options
Diffstat (limited to 'exportclight/ExportClight.ml')
| -rw-r--r-- | exportclight/ExportClight.ml | 35 |
1 files changed, 21 insertions, 14 deletions
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index c9d6fced..87956b58 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -81,8 +81,12 @@ let define_idents p = string_of_atom (fun (id, name) -> try - fprintf p "Definition _%s : ident := %ld%%positive.@ " - (sanitize name) (P.to_int32 id) + if id = pos_of_string name then + fprintf p "Definition _%s : ident := $\"%s\".@ " + (sanitize name) name + else + fprintf p "Definition _%s : ident := %ld%%positive.@ " + (sanitize name) (P.to_int32 id) with Not_an_identifier -> ()); iter_hashtbl_sorted @@ -93,9 +97,11 @@ let define_idents p = fprintf p "@ " let name_temporary t = - let t1 = P.to_int t and t0 = P.to_int (first_unused_ident ()) in - if t1 >= t0 && not (Hashtbl.mem temp_names t) - then Hashtbl.add temp_names t (sprintf "_t'%d" (t1 - t0 + 1)) + if not (Hashtbl.mem string_of_atom t) && not (Hashtbl.mem temp_names t) + then begin + let t1 = P.to_int t and t0 = P.to_int (first_unused_ident ()) in + Hashtbl.add temp_names t (sprintf "_t'%d" (t1 - t0 + 1)) + end let name_opt_temporary = function | None -> () @@ -468,7 +474,7 @@ let print_assertion p (txt, targs) = | Text _ -> () | Param n -> max_param := max n !max_param) frags; - fprintf p " | \"%s\"%%string, " txt; + fprintf p " | \"%s\", " txt; list_iteri (fun i targ -> fprintf p "_x%d :: " (i + 1)) targs; @@ -495,7 +501,8 @@ let print_assertions p = let prologue = "\ From Coq Require Import String List ZArith.\n\ From compcert Require Import Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs.\n\ -Local Open Scope Z_scope.\n" +Local Open Scope Z_scope.\n\ +Local Open Scope string_scope.\n" (* Naming the compiler-generated temporaries occurring in the program *) @@ -554,15 +561,15 @@ let name_program p = let print_clightgen_info p sourcefile normalized = fprintf p "@[<v 2>Module Info."; - fprintf p "@ Definition version := %S%%string." Version.version; - fprintf p "@ Definition build_number := %S%%string." Version.buildnr; - fprintf p "@ Definition build_tag := %S%%string." Version.tag; - fprintf p "@ Definition arch := %S%%string." Configuration.arch; - fprintf p "@ Definition model := %S%%string." Configuration.model; - fprintf p "@ Definition abi := %S%%string." Configuration.abi; + fprintf p "@ Definition version := %S." Version.version; + fprintf p "@ Definition build_number := %S." Version.buildnr; + fprintf p "@ Definition build_tag := %S." Version.tag; + fprintf p "@ Definition arch := %S." Configuration.arch; + fprintf p "@ Definition model := %S." Configuration.model; + fprintf p "@ Definition abi := %S." Configuration.abi; fprintf p "@ Definition bitsize := %d." (if Archi.ptr64 then 64 else 32); fprintf p "@ Definition big_endian := %B." Archi.big_endian; - fprintf p "@ Definition source_file := %S%%string." sourcefile; + fprintf p "@ Definition source_file := %S." sourcefile; fprintf p "@ Definition normalized := %B." normalized; fprintf p "@]@ End Info.@ @ " |