diff --git a/cfrontend/C2Clight.ml b/cfrontend/C2Clight.ml
index 2ad2ac5e735128bac12752a07891f88ec1627a1d..57ee8fd5771b2b4df30eadb7e26e29bb520c6b33 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 0388c2eb1e70a7e4b0903fcb3e06cfb28c3f4bb7..ebeda7cc3291fa597bd7092ae3e180e613341992 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 *)
diff --git a/cparser/Builtins.ml b/cparser/Builtins.ml
index 020452f99b85add16c58274e41587ae409b692de..8eb1abfd7b8a8a493eeb9344ac3074365da41008 100644
--- a/cparser/Builtins.ml
+++ b/cparser/Builtins.ml
@@ -20,14 +20,17 @@ open Cutil
let env = ref Env.empty
let idents = ref []
+let decls = ref []
let environment () = !env
let identifiers () = !idents
+let declarations () = List.rev !decls
let add_typedef (s, ty) =
let (id, env') = Env.enter_typedef !env s ty in
env := env';
- idents := id :: !idents
+ idents := id :: !idents;
+ decls := {gdesc = Gtypedef(id, ty); gloc = no_loc} :: !decls
let add_function (s, (res, args, va)) =
let ty =
@@ -36,7 +39,8 @@ let add_function (s, (res, args, va)) =
va, []) in
let (id, env') = Env.enter_ident !env s Storage_extern ty in
env := env';
- idents := id :: !idents
+ idents := id :: !idents;
+ decls := {gdesc = Gdecl(Storage_extern, id, ty, None); gloc = no_loc} :: !decls
type t = {
typedefs: (string * C.typ) list;
diff --git a/cparser/Builtins.mli b/cparser/Builtins.mli
index be0d941fdddadf4f3d9f90168247c355a1e22072..7f9d78a95f1c88a48357f51319a18e858f45fafb 100644
--- a/cparser/Builtins.mli
+++ b/cparser/Builtins.mli
@@ -15,6 +15,7 @@
val environment: unit -> Env.t
val identifiers: unit -> C.ident list
+val declarations: unit -> C.globdecl list
type t = {
typedefs: (string * C.typ) list;
diff --git a/cparser/Makefile b/cparser/Makefile
index df1d604767cc7470eefb75a2ccd1c04bf3297eb5..837bda87e49ff36e56efe578985a5cdf45313554 100644
--- a/cparser/Makefile
+++ b/cparser/Makefile
@@ -11,9 +11,9 @@ INTFS=C.mli
SRCS=Errors.ml Cabs.ml Cabshelper.ml Parse_aux.ml Parser.ml Lexer.ml \
Machine.ml \
- Env.ml Cprint.ml Cutil.ml Ceval.ml Cleanup.ml \
+ Env.ml Cprint.ml Cutil.ml Ceval.ml \
Builtins.ml GCC.ml \
- Elab.ml Rename.ml \
+ Cleanup.ml Elab.ml Rename.ml \
Transform.ml \
Unblock.ml SimplExpr.ml AddCasts.ml StructByValue.ml StructAssign.ml \
Bitfields.ml \
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 2d8b0266febff4bea65c6e36cb45a2c644a48c6f..2cc409f5de5994dcd08dcccd31f5bd6f2bcb6ae4 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -63,7 +63,7 @@ let preprocess ifile ofile =
let compile_c_file sourcename ifile ofile =
(* Simplification options *)
let simplifs =
- "bec" (* blocks, impure exprs, implicit casts: mandatory *)
+ "bec" (* blocks, impure exprs, implicit casts: mandatory *)
^ (if !option_fstruct_passing then "s" else "")
^ (if !option_fstruct_assign then "S" else "")
^ (if !option_fbitfields then "f" else "") in
@@ -325,6 +325,7 @@ let cmdline_actions =
let _ =
Cparser.Machine.config := Cparser.Machine.ilp32ll64;
+ Cparser.Builtins.set C2Clight.builtins;
CPragmas.initialize();
parse_cmdline cmdline_actions usage_string;
if !linker_options <> []
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index a1e5afe36ca27afddf71c1d28c3f74b68ce3abb7..d69d0aff3738e9098051975c5dc383bcd11cee10 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -684,25 +684,12 @@ let print_init oc = function
fprintf oc " .long %a\n"
symbol_offset (symb, camlint_of_coqint ofs)
-let print_init_char oc = 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 output_char oc (Char.chr c)
- else fprintf oc "\\%03o" c
- | _ ->
- assert false
-
-let re_string_literal = Str.regexp "__stringlit_[0-9]+"
-
let print_init_data oc name id =
- if Str.string_match re_string_literal (extern_atom name) 0
+ if Str.string_match PrintCsyntax.re_string_literal (extern_atom name) 0
&& List.for_all (function Init_int8 _ -> true | _ -> false) id
- then begin
- fprintf oc " .ascii \"";
- List.iter (print_init_char oc) id;
- fprintf oc "\"\n"
- end else
+ then
+ fprintf oc " .ascii \"%s\"\n" (PrintCsyntax.string_of_init id)
+ else
List.iter (print_init oc) id
let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) =