diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-07 17:49:18 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-07 17:49:18 +0000 |
commit | c24a652789e15b33153c1d90c6869eb6e6e28040 (patch) | |
tree | e5e5aa2767fe098e3b23f82091ff6d60b0c6d8f2 /cfrontend | |
parent | 6a8503115a9952dc793d15d0ea9033b68b30aae6 (diff) | |
download | compcert-c24a652789e15b33153c1d90c6869eb6e6e28040.tar.gz compcert-c24a652789e15b33153c1d90c6869eb6e6e28040.zip |
Handling of builtins, continued.
PrintCsyntax, PrintAsm: improve printing of float literals.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1284 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/C2Clight.ml | 14 | ||||
-rw-r--r-- | cfrontend/PrintCsyntax.ml | 57 |
2 files changed, 42 insertions, 29 deletions
diff --git a/cfrontend/C2Clight.ml b/cfrontend/C2Clight.ml index 2ad2ac5e..57ee8fd5 100644 --- a/cfrontend/C2Clight.ml +++ b/cfrontend/C2Clight.ml @@ -704,6 +704,7 @@ let convertProgram p = Hashtbl.clear decl_atom; Hashtbl.clear stringTable; Hashtbl.clear stub_function_table; + let p = Builtins.declarations() @ p in try let (funs1, vars1) = convertGlobdecls (translEnv Env.empty p) [] [] (cleanupGlobals p) in @@ -743,3 +744,16 @@ let atom_is_readonly a = type_is_readonly env ty with Not_found -> false + +(** ** The builtin environment *) + +let builtins = { + Builtins.typedefs = [ + (* keeps GCC-specific headers happy, harmless for others *) + "__builtin_va_list", C.TPtr(C.TVoid [], []) + ]; + Builtins.functions = [ + ] +} + + diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 0388c2eb..ebeda7cc 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -344,32 +344,21 @@ let print_fundef p (Coq_pair(id, fd)) = print_function p id f let string_of_init id = - try - let s = String.create (List.length id) in - let i = ref 0 in - List.iter - (function - | Init_int8 n -> - s.[!i] <- Char.chr(Int32.to_int(camlint_of_coqint n)); - incr i - | _ -> raise Not_found) - id; - Some s - with Not_found -> None - -let print_escaped_string p s = - fprintf p "\""; - for i = 0 to String.length s - 1 do - match s.[i] with - | ('\"' | '\\') as c -> fprintf p "\\%c" c - | '\n' -> fprintf p "\\n" - | '\t' -> fprintf p "\\t" - | '\r' -> fprintf p "\\r" - | c -> if c >= ' ' && c <= '~' - then fprintf p "%c" c - else fprintf p "\\x%02x" (Char.code c) - done; - fprintf p "\"" + let b = Buffer.create (List.length id) in + let add_init = function + | Init_int8 n -> + let c = Int32.to_int (camlint_of_coqint n) in + if c >= 32 && c <= 126 && c <> Char.code '\"' && c <> Char.code '\\' + then Buffer.add_char b (Char.chr c) + else Buffer.add_string b (Printf.sprintf "\\%03o" c) + | _ -> + assert false + in List.iter add_init id; Buffer.contents b + +let chop_last_nul id = + match List.rev id with + | Init_int8 BinInt.Z0 :: tl -> List.rev tl + | _ -> id let print_init p = function | Init_int8 n -> fprintf p "%ld,@ " (camlint_of_coqint n) @@ -384,6 +373,8 @@ let print_init p = function then fprintf p "&%s,@ " (extern_atom symb) else fprintf p "(void *)((char *)&%s + %ld),@ " (extern_atom symb) ofs +let re_string_literal = Str.regexp "__stringlit_[0-9]+" + let print_globvar p (Coq_pair(Coq_pair(id, init), ty)) = match init with | [] -> @@ -393,10 +384,18 @@ let print_globvar p (Coq_pair(Coq_pair(id, init), ty)) = fprintf p "%s;@ @ " (name_cdecl (extern_atom id) ty) | _ -> - fprintf p "@[<hov 2>%s = {@ " + fprintf p "@[<hov 2>%s = " (name_cdecl (extern_atom id) ty); - List.iter (print_init p) init; - fprintf p "};@]@ @ " + if Str.string_match re_string_literal (extern_atom id) 0 + && List.for_all (function Init_int8 _ -> true | _ -> false) init + then + fprintf p "\"%s\"" (string_of_init (chop_last_nul init)) + else begin + fprintf p "{@ "; + List.iter (print_init p) init; + fprintf p "}" + end; + fprintf p ";@]@ @ " (* Collect struct and union types *) |