Revised treatment of builtins

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1283 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

10 files changed, 300 insertions, 244 deletions

diff --git a/cparser/.depend b/cparser/.depend
index d5c86cf7..9f12718f 100644
--- a/cparser/.depend
+++ b/cparser/.depend
@@ -9,6 +9,7 @@ Cutil.cmi: Env.cmi C.cmi
 Elab.cmi: C.cmi 
 Env.cmi: C.cmi 
 Errors.cmi: 
+GCC.cmi: Builtins.cmi 
 Lexer.cmi: Parser.cmi 
 Machine.cmi: 
 Parse_aux.cmi: 
@@ -48,12 +49,14 @@ Env.cmo: C.cmi Env.cmi
 Env.cmx: C.cmi Env.cmi 
 Errors.cmo: Errors.cmi 
 Errors.cmx: Errors.cmi 
+GCC.cmo: Cutil.cmi C.cmi Builtins.cmi GCC.cmi 
+GCC.cmx: Cutil.cmx C.cmi Builtins.cmx GCC.cmi 
 Lexer.cmo: Parser.cmi Parse_aux.cmi Cabshelper.cmo Lexer.cmi 
 Lexer.cmx: Parser.cmx Parse_aux.cmx Cabshelper.cmx Lexer.cmi 
 Machine.cmo: Machine.cmi 
 Machine.cmx: Machine.cmi 
-Main.cmo: Parse.cmi Cprint.cmi 
-Main.cmx: Parse.cmx Cprint.cmx 
+Main.cmo: Parse.cmi GCC.cmi Cprint.cmi Builtins.cmi 
+Main.cmx: Parse.cmx GCC.cmx Cprint.cmx Builtins.cmx 
 Parse_aux.cmo: Errors.cmi Cabshelper.cmo Parse_aux.cmi 
 Parse_aux.cmx: Errors.cmx Cabshelper.cmx Parse_aux.cmi 
 Parse.cmo: Unblock.cmi StructByValue.cmi StructAssign.cmi SimplExpr.cmi \
@@ -64,12 +67,8 @@ Parser.cmo: Parse_aux.cmi Cabshelper.cmo Cabs.cmo Parser.cmi
 Parser.cmx: Parse_aux.cmx Cabshelper.cmx Cabs.cmx Parser.cmi 
 Rename.cmo: Errors.cmi Cutil.cmi C.cmi Builtins.cmi Rename.cmi 
 Rename.cmx: Errors.cmx Cutil.cmx C.cmi Builtins.cmx Rename.cmi 
-Scoping.cmo: 
-Scoping.cmx: 
-SimplExpr.cmo: Transform.cmi Cutil.cmi C.cmi SimplExpr.cmi 
-SimplExpr.cmx: Transform.cmx Cutil.cmx C.cmi SimplExpr.cmi 
-SimplifyStrict.cmo: Env.cmi Cutil.cmi C.cmi 
-SimplifyStrict.cmx: Env.cmx Cutil.cmx C.cmi 
+SimplExpr.cmo: Transform.cmi Errors.cmi Cutil.cmi C.cmi SimplExpr.cmi 
+SimplExpr.cmx: Transform.cmx Errors.cmx Cutil.cmx C.cmi SimplExpr.cmi 
 StructAssign.cmo: Transform.cmi Errors.cmi Env.cmi Cutil.cmi C.cmi \
     StructAssign.cmi 
 StructAssign.cmx: Transform.cmx Errors.cmx Env.cmx Cutil.cmx C.cmi \
diff --git a/cparser/Builtins.ml b/cparser/Builtins.ml
index eb10314d..020452f9 100644
--- a/cparser/Builtins.ml
+++ b/cparser/Builtins.ml
@@ -18,233 +18,33 @@
 open C
 open Cutil
 
-(* Code adapted from CIL *)
-
-let voidType = TVoid []
-let charType = TInt(IChar, [])
-let intType = TInt(IInt, [])
-let uintType = TInt(IUInt, [])
-let longType = TInt(ILong, [])
-let ulongType = TInt(IULong, [])
-let ulongLongType = TInt(IULongLong, [])
-let floatType = TFloat(FFloat, [])
-let doubleType = TFloat(FDouble, [])
-let longDoubleType = TFloat (FLongDouble, [])
-let voidPtrType = TPtr(TVoid [], [])
-let voidConstPtrType = TPtr(TVoid [AConst], [])
-let charPtrType = TPtr(TInt(IChar, []), [])
-let charConstPtrType = TPtr(TInt(IChar, [AConst]), [])
-let intPtrType = TPtr(TInt(IInt, []), [])
-let sizeType = TInt(size_t_ikind, [])
-
-let gcc_builtin_types = [
-  "__builtin_va_list", voidPtrType
-]
-
-let gcc_builtin_values = [
-  "__builtin___fprintf_chk",  (intType, [ voidPtrType; intType; charConstPtrType ], true) (* first argument is really FILE*, not void*, but we don't want to build in the definition for FILE *);
-  "__builtin___memcpy_chk",  (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType; sizeType ], false);
-  "__builtin___memmove_chk",  (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType; sizeType ], false);
-  "__builtin___mempcpy_chk",  (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType; sizeType ], false);
-  "__builtin___memset_chk",  (voidPtrType, [ voidPtrType; intType; sizeType; sizeType ], false);
-  "__builtin___printf_chk",  (intType, [ intType; charConstPtrType ], true);
-  "__builtin___snprintf_chk",  (intType, [ charPtrType; sizeType; intType; sizeType; charConstPtrType ], true);
-  "__builtin___sprintf_chk",  (intType, [ charPtrType; intType; sizeType; charConstPtrType ], true);
-  "__builtin___stpcpy_chk",  (charPtrType, [ charPtrType; charConstPtrType; sizeType ], false);
-  "__builtin___strcat_chk",  (charPtrType, [ charPtrType; charConstPtrType; sizeType ], false);
-  "__builtin___strcpy_chk",  (charPtrType, [ charPtrType; charConstPtrType; sizeType ], false);
-  "__builtin___strncat_chk",  (charPtrType, [ charPtrType; charConstPtrType; sizeType; sizeType ], false);
-  "__builtin___strncpy_chk",  (charPtrType, [ charPtrType; charConstPtrType; sizeType; sizeType ], false);
-  "__builtin___vfprintf_chk",  (intType, [ voidPtrType; intType; charConstPtrType; voidPtrType ], false) (* first argument is really FILE*, not void*, but we don't want to build in the definition for FILE *);
-  "__builtin___vprintf_chk",  (intType, [ intType; charConstPtrType; voidPtrType ], false);
-  "__builtin___vsnprintf_chk",  (intType, [ charPtrType; sizeType; intType; sizeType; charConstPtrType; voidPtrType ], false);
-  "__builtin___vsprintf_chk",  (intType, [ charPtrType; intType; sizeType; charConstPtrType; voidPtrType ], false);
-
-  "__builtin_acos",  (doubleType, [ doubleType ], false);
-  "__builtin_acosf",  (floatType, [ floatType ], false);
-  "__builtin_acosl",  (longDoubleType, [ longDoubleType ], false);
-
-  "__builtin_alloca",  (voidPtrType, [ uintType ], false);
-  
-  "__builtin_asin",  (doubleType, [ doubleType ], false);
-  "__builtin_asinf",  (floatType, [ floatType ], false);
-  "__builtin_asinl",  (longDoubleType, [ longDoubleType ], false);
-
-  "__builtin_atan",  (doubleType, [ doubleType ], false);
-  "__builtin_atanf",  (floatType, [ floatType ], false);
-  "__builtin_atanl",  (longDoubleType, [ longDoubleType ], false);
-
-  "__builtin_atan2",  (doubleType, [ doubleType; doubleType ], false);
-  "__builtin_atan2f",  (floatType, [ floatType; floatType ], false);
-  "__builtin_atan2l",  (longDoubleType, [ longDoubleType; 
-                                                longDoubleType ], false);
-
-  "__builtin_ceil",  (doubleType, [ doubleType ], false);
-  "__builtin_ceilf",  (floatType, [ floatType ], false);
-  "__builtin_ceill",  (longDoubleType, [ longDoubleType ], false);
-
-  "__builtin_cos",  (doubleType, [ doubleType ], false);
-  "__builtin_cosf",  (floatType, [ floatType ], false);
-  "__builtin_cosl",  (longDoubleType, [ longDoubleType ], false);
-
-  "__builtin_cosh",  (doubleType, [ doubleType ], false);
-  "__builtin_coshf",  (floatType, [ floatType ], false);
-  "__builtin_coshl",  (longDoubleType, [ longDoubleType ], false);
-
-  "__builtin_clz",  (intType, [ uintType ], false);
-  "__builtin_clzl",  (intType, [ ulongType ], false);
-  "__builtin_clzll",  (intType, [ ulongLongType ], false);
-  "__builtin_constant_p",  (intType, [ intType ], false);
-  "__builtin_ctz",  (intType, [ uintType ], false);
-  "__builtin_ctzl",  (intType, [ ulongType ], false);
-  "__builtin_ctzll",  (intType, [ ulongLongType ], false);
-
-  "__builtin_exp",  (doubleType, [ doubleType ], false);
-  "__builtin_expf",  (floatType, [ floatType ], false);
-  "__builtin_expl",  (longDoubleType, [ longDoubleType ], false);
-
-  "__builtin_expect",  (longType, [ longType; longType ], false);
-
-  "__builtin_fabs",  (doubleType, [ doubleType ], false);
-  "__builtin_fabsf",  (floatType, [ floatType ], false);
-  "__builtin_fabsl",  (longDoubleType, [ longDoubleType ], false);
-
-  "__builtin_ffs",  (intType, [ uintType ], false);
-  "__builtin_ffsl",  (intType, [ ulongType ], false);
-  "__builtin_ffsll",  (intType, [ ulongLongType ], false);
-  "__builtin_frame_address",  (voidPtrType, [ uintType ], false);
-
-  "__builtin_floor",  (doubleType, [ doubleType ], false);
-  "__builtin_floorf",  (floatType, [ floatType ], false);
-  "__builtin_floorl",  (longDoubleType, [ longDoubleType ], false);
-
-  "__builtin_huge_val",  (doubleType, [], false);
-  "__builtin_huge_valf",  (floatType, [], false);
-  "__builtin_huge_vall",  (longDoubleType, [], false);
-  "__builtin_inf",  (doubleType, [], false);
-  "__builtin_inff",  (floatType, [], false);
-  "__builtin_infl",  (longDoubleType, [], false);
-  "__builtin_memcpy",  (voidPtrType, [ voidPtrType; voidConstPtrType; uintType ], false);
-  "__builtin_mempcpy",  (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType ], false);
-
-  "__builtin_fmod",  (doubleType, [ doubleType ], false);
-  "__builtin_fmodf",  (floatType, [ floatType ], false);
-  "__builtin_fmodl",  (longDoubleType, [ longDoubleType ], false);
-
-  "__builtin_frexp",  (doubleType, [ doubleType; intPtrType ], false);
-  "__builtin_frexpf",  (floatType, [ floatType; intPtrType  ], false);
-  "__builtin_frexpl",  (longDoubleType, [ longDoubleType; 
-                                                intPtrType  ], false);
-
-  "__builtin_ldexp",  (doubleType, [ doubleType; intType ], false);
-  "__builtin_ldexpf",  (floatType, [ floatType; intType  ], false);
-  "__builtin_ldexpl",  (longDoubleType, [ longDoubleType; 
-                                                intType  ], false);
-
-  "__builtin_log",  (doubleType, [ doubleType ], false);
-  "__builtin_logf",  (floatType, [ floatType ], false);
-  "__builtin_logl",  (longDoubleType, [ longDoubleType ], false);
-
-  "__builtin_log10",  (doubleType, [ doubleType ], false);
-  "__builtin_log10f",  (floatType, [ floatType ], false);
-  "__builtin_log10l",  (longDoubleType, [ longDoubleType ], false);
-
-  "__builtin_modff",  (floatType, [ floatType; 
-                                          TPtr(floatType,[]) ], false);
-  "__builtin_modfl",  (longDoubleType, [ longDoubleType; 
-                                               TPtr(longDoubleType, []) ], 
-                             false);
-
-  "__builtin_nan",  (doubleType, [ charConstPtrType ], false);
-  "__builtin_nanf",  (floatType, [ charConstPtrType ], false);
-  "__builtin_nanl",  (longDoubleType, [ charConstPtrType ], false);
-  "__builtin_nans",  (doubleType, [ charConstPtrType ], false);
-  "__builtin_nansf",  (floatType, [ charConstPtrType ], false);
-  "__builtin_nansl",  (longDoubleType, [ charConstPtrType ], false);
-  "__builtin_next_arg",  (voidPtrType, [], false);
-  "__builtin_object_size",  (sizeType, [ voidPtrType; intType ], false);
-
-  "__builtin_parity",  (intType, [ uintType ], false);
-  "__builtin_parityl",  (intType, [ ulongType ], false);
-  "__builtin_parityll",  (intType, [ ulongLongType ], false);
-
-  "__builtin_popcount",  (intType, [ uintType ], false);
-  "__builtin_popcountl",  (intType, [ ulongType ], false);
-  "__builtin_popcountll",  (intType, [ ulongLongType ], false);
-
-  "__builtin_powi",  (doubleType, [ doubleType; intType ], false);
-  "__builtin_powif",  (floatType, [ floatType; intType ], false);
-  "__builtin_powil",  (longDoubleType, [ longDoubleType; intType ], false);
-  "__builtin_prefetch",  (voidType, [ voidConstPtrType ], true);
-  "__builtin_return",  (voidType, [ voidConstPtrType ], false);
-  "__builtin_return_address",  (voidPtrType, [ uintType ], false);
-
-  "__builtin_sin",  (doubleType, [ doubleType ], false);
-  "__builtin_sinf",  (floatType, [ floatType ], false);
-  "__builtin_sinl",  (longDoubleType, [ longDoubleType ], false);
-
-  "__builtin_sinh",  (doubleType, [ doubleType ], false);
-  "__builtin_sinhf",  (floatType, [ floatType ], false);
-  "__builtin_sinhl",  (longDoubleType, [ longDoubleType ], false);
-
-  "__builtin_sqrt",  (doubleType, [ doubleType ], false);
-  "__builtin_sqrtf",  (floatType, [ floatType ], false);
-  "__builtin_sqrtl",  (longDoubleType, [ longDoubleType ], false);
-
-  "__builtin_stpcpy",  (charPtrType, [ charPtrType; charConstPtrType ], false);
-  "__builtin_strchr",  (charPtrType, [ charPtrType; charType ], false);
-  "__builtin_strcmp",  (intType, [ charConstPtrType; charConstPtrType ], false);
-  "__builtin_strcpy",  (charPtrType, [ charPtrType; charConstPtrType ], false);
-  "__builtin_strcspn",  (uintType, [ charConstPtrType; charConstPtrType ], false);
-  "__builtin_strncat",  (charPtrType, [ charPtrType; charConstPtrType; sizeType ], false);
-  "__builtin_strncmp",  (intType, [ charConstPtrType; charConstPtrType; sizeType ], false);
-  "__builtin_strncpy",  (charPtrType, [ charPtrType; charConstPtrType; sizeType ], false);
-  "__builtin_strspn",  (intType, [ charConstPtrType; charConstPtrType ], false);
-  "__builtin_strpbrk",  (charPtrType, [ charConstPtrType; charConstPtrType ], false);
-  (* When we parse builtin_types_compatible_p, we change its interface *)
-  "__builtin_types_compatible_p", 
-                              (intType, [ uintType; (* Sizeof the type *)
-                                          uintType  (* Sizeof the type *) ],
-                               false);
-  "__builtin_tan",  (doubleType, [ doubleType ], false);
-  "__builtin_tanf",  (floatType, [ floatType ], false);
-  "__builtin_tanl",  (longDoubleType, [ longDoubleType ], false);
-
-  "__builtin_tanh",  (doubleType, [ doubleType ], false);
-  "__builtin_tanhf",  (floatType, [ floatType ], false);
-  "__builtin_tanhl",  (longDoubleType, [ longDoubleType ], false);
-
-  "__builtin_va_end",  (voidType, [ voidPtrType ], false);
-  "__builtin_varargs_start",  
-    (voidType, [ voidPtrType ], false);
-  (* When we elaborate builtin_stdarg_start/builtin_va_start,
-     second argument is passed by address *)
-  "__builtin_va_start",  (voidType, [ voidPtrType; voidPtrType ], false);
-  "__builtin_stdarg_start",  (voidType, [ voidPtrType ], false);
-  (* When we parse builtin_va_arg, type argument becomes sizeof type *)
-  "__builtin_va_arg",  (voidType, [ voidPtrType; sizeType ], false);
-  "__builtin_va_copy",  (voidType, [ voidPtrType;
-                                           voidPtrType ],
-                              false)
-]
-
-let (builtin_env, builtin_idents) =
-  let env = ref Env.empty
-  and ids = ref [] in
-  List.iter
-    (fun (s, ty) ->
-      let (id, env') = Env.enter_typedef !env s ty in
-      env := env';
-      ids := id :: !ids)
-    gcc_builtin_types;
-  List.iter
-    (fun (s, (res, args, va)) ->
-      let ty =
-        TFun(res,
-             Some (List.map (fun ty -> (Env.fresh_ident "", ty)) args),
-             va, []) in
-      let (id, env') = Env.enter_ident !env s Storage_extern ty in
-      env := env';
-      ids := id :: !ids)
-    gcc_builtin_values;
-  (!env, List.rev !ids)
+let env = ref Env.empty
+let idents = ref []
+
+let environment () = !env
+let identifiers () = !idents
+
+let add_typedef (s, ty) =
+  let (id, env') = Env.enter_typedef !env s ty in
+  env := env';
+  idents := id :: !idents
+
+let add_function (s, (res, args, va)) =
+  let ty =
+    TFun(res,
+         Some (List.map (fun ty -> (Env.fresh_ident "", ty)) args),
+         va, []) in
+  let (id, env') = Env.enter_ident !env s Storage_extern ty in
+  env := env';
+  idents := id :: !idents
+
+type t = {
+  typedefs: (string * C.typ) list;
+  functions: (string * (C.typ * C.typ list * bool)) list
+}
+
+let set blt =
+  env := Env.empty;
+  idents := [];
+  List.iter add_typedef blt.typedefs;
+  List.iter add_function blt.functions
diff --git a/cparser/Builtins.mli b/cparser/Builtins.mli
index 853bae93..be0d941f 100644
--- a/cparser/Builtins.mli
+++ b/cparser/Builtins.mli
@@ -13,5 +13,12 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-val builtin_env : Env.t
-val builtin_idents: C.ident list
+val environment: unit -> Env.t
+val identifiers: unit -> C.ident list
+
+type t = {
+  typedefs: (string * C.typ) list;
+  functions: (string * (C.typ * C.typ list * bool)) list
+}
+
+val set: t -> unit
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 3c01230e..5971d4d4 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1755,7 +1755,7 @@ let _ = elab_block_f := elab_block
 let elab_preprocessed_file name ic =
   let lb = Lexer.init name ic in
   reset();
-  ignore (elab_definitions false Builtins.builtin_env
+  ignore (elab_definitions false (Builtins.environment())
                                  (Parser.file Lexer.initial lb));
   Lexer.finish();
   elaborated_program()
diff --git a/cparser/GCC.ml b/cparser/GCC.ml
new file mode 100644
index 00000000..9f864dcd
--- /dev/null
+++ b/cparser/GCC.ml
@@ -0,0 +1,230 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* GCC built-ins *)
+
+open C
+open Cutil
+
+(* Code adapted from CIL *)
+
+let voidType = TVoid []
+let charType = TInt(IChar, [])
+let intType = TInt(IInt, [])
+let uintType = TInt(IUInt, [])
+let longType = TInt(ILong, [])
+let ulongType = TInt(IULong, [])
+let ulongLongType = TInt(IULongLong, [])
+let floatType = TFloat(FFloat, [])
+let doubleType = TFloat(FDouble, [])
+let longDoubleType = TFloat (FLongDouble, [])
+let voidPtrType = TPtr(TVoid [], [])
+let voidConstPtrType = TPtr(TVoid [AConst], [])
+let charPtrType = TPtr(TInt(IChar, []), [])
+let charConstPtrType = TPtr(TInt(IChar, [AConst]), [])
+let intPtrType = TPtr(TInt(IInt, []), [])
+let sizeType = TInt(size_t_ikind, [])
+
+let builtins = {
+  Builtins.typedefs = [
+  "__builtin_va_list", voidPtrType
+];
+  Builtins.functions = [
+  "__builtin___fprintf_chk",  (intType, [ voidPtrType; intType; charConstPtrType ], true) (* first argument is really FILE*, not void*, but we don't want to build in the definition for FILE *);
+  "__builtin___memcpy_chk",  (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType; sizeType ], false);
+  "__builtin___memmove_chk",  (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType; sizeType ], false);
+  "__builtin___mempcpy_chk",  (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType; sizeType ], false);
+  "__builtin___memset_chk",  (voidPtrType, [ voidPtrType; intType; sizeType; sizeType ], false);
+  "__builtin___printf_chk",  (intType, [ intType; charConstPtrType ], true);
+  "__builtin___snprintf_chk",  (intType, [ charPtrType; sizeType; intType; sizeType; charConstPtrType ], true);
+  "__builtin___sprintf_chk",  (intType, [ charPtrType; intType; sizeType; charConstPtrType ], true);
+  "__builtin___stpcpy_chk",  (charPtrType, [ charPtrType; charConstPtrType; sizeType ], false);
+  "__builtin___strcat_chk",  (charPtrType, [ charPtrType; charConstPtrType; sizeType ], false);
+  "__builtin___strcpy_chk",  (charPtrType, [ charPtrType; charConstPtrType; sizeType ], false);
+  "__builtin___strncat_chk",  (charPtrType, [ charPtrType; charConstPtrType; sizeType; sizeType ], false);
+  "__builtin___strncpy_chk",  (charPtrType, [ charPtrType; charConstPtrType; sizeType; sizeType ], false);
+  "__builtin___vfprintf_chk",  (intType, [ voidPtrType; intType; charConstPtrType; voidPtrType ], false) (* first argument is really FILE*, not void*, but we don't want to build in the definition for FILE *);
+  "__builtin___vprintf_chk",  (intType, [ intType; charConstPtrType; voidPtrType ], false);
+  "__builtin___vsnprintf_chk",  (intType, [ charPtrType; sizeType; intType; sizeType; charConstPtrType; voidPtrType ], false);
+  "__builtin___vsprintf_chk",  (intType, [ charPtrType; intType; sizeType; charConstPtrType; voidPtrType ], false);
+
+  "__builtin_acos",  (doubleType, [ doubleType ], false);
+  "__builtin_acosf",  (floatType, [ floatType ], false);
+  "__builtin_acosl",  (longDoubleType, [ longDoubleType ], false);
+
+  "__builtin_alloca",  (voidPtrType, [ uintType ], false);
+  
+  "__builtin_asin",  (doubleType, [ doubleType ], false);
+  "__builtin_asinf",  (floatType, [ floatType ], false);
+  "__builtin_asinl",  (longDoubleType, [ longDoubleType ], false);
+
+  "__builtin_atan",  (doubleType, [ doubleType ], false);
+  "__builtin_atanf",  (floatType, [ floatType ], false);
+  "__builtin_atanl",  (longDoubleType, [ longDoubleType ], false);
+
+  "__builtin_atan2",  (doubleType, [ doubleType; doubleType ], false);
+  "__builtin_atan2f",  (floatType, [ floatType; floatType ], false);
+  "__builtin_atan2l",  (longDoubleType, [ longDoubleType; 
+                                                longDoubleType ], false);
+
+  "__builtin_ceil",  (doubleType, [ doubleType ], false);
+  "__builtin_ceilf",  (floatType, [ floatType ], false);
+  "__builtin_ceill",  (longDoubleType, [ longDoubleType ], false);
+
+  "__builtin_cos",  (doubleType, [ doubleType ], false);
+  "__builtin_cosf",  (floatType, [ floatType ], false);
+  "__builtin_cosl",  (longDoubleType, [ longDoubleType ], false);
+
+  "__builtin_cosh",  (doubleType, [ doubleType ], false);
+  "__builtin_coshf",  (floatType, [ floatType ], false);
+  "__builtin_coshl",  (longDoubleType, [ longDoubleType ], false);
+
+  "__builtin_clz",  (intType, [ uintType ], false);
+  "__builtin_clzl",  (intType, [ ulongType ], false);
+  "__builtin_clzll",  (intType, [ ulongLongType ], false);
+  "__builtin_constant_p",  (intType, [ intType ], false);
+  "__builtin_ctz",  (intType, [ uintType ], false);
+  "__builtin_ctzl",  (intType, [ ulongType ], false);
+  "__builtin_ctzll",  (intType, [ ulongLongType ], false);
+
+  "__builtin_exp",  (doubleType, [ doubleType ], false);
+  "__builtin_expf",  (floatType, [ floatType ], false);
+  "__builtin_expl",  (longDoubleType, [ longDoubleType ], false);
+
+  "__builtin_expect",  (longType, [ longType; longType ], false);
+
+  "__builtin_fabs",  (doubleType, [ doubleType ], false);
+  "__builtin_fabsf",  (floatType, [ floatType ], false);
+  "__builtin_fabsl",  (longDoubleType, [ longDoubleType ], false);
+
+  "__builtin_ffs",  (intType, [ uintType ], false);
+  "__builtin_ffsl",  (intType, [ ulongType ], false);
+  "__builtin_ffsll",  (intType, [ ulongLongType ], false);
+  "__builtin_frame_address",  (voidPtrType, [ uintType ], false);
+
+  "__builtin_floor",  (doubleType, [ doubleType ], false);
+  "__builtin_floorf",  (floatType, [ floatType ], false);
+  "__builtin_floorl",  (longDoubleType, [ longDoubleType ], false);
+
+  "__builtin_huge_val",  (doubleType, [], false);
+  "__builtin_huge_valf",  (floatType, [], false);
+  "__builtin_huge_vall",  (longDoubleType, [], false);
+  "__builtin_inf",  (doubleType, [], false);
+  "__builtin_inff",  (floatType, [], false);
+  "__builtin_infl",  (longDoubleType, [], false);
+  "__builtin_memcpy",  (voidPtrType, [ voidPtrType; voidConstPtrType; uintType ], false);
+  "__builtin_mempcpy",  (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType ], false);
+
+  "__builtin_fmod",  (doubleType, [ doubleType ], false);
+  "__builtin_fmodf",  (floatType, [ floatType ], false);
+  "__builtin_fmodl",  (longDoubleType, [ longDoubleType ], false);
+
+  "__builtin_frexp",  (doubleType, [ doubleType; intPtrType ], false);
+  "__builtin_frexpf",  (floatType, [ floatType; intPtrType  ], false);
+  "__builtin_frexpl",  (longDoubleType, [ longDoubleType; 
+                                                intPtrType  ], false);
+
+  "__builtin_ldexp",  (doubleType, [ doubleType; intType ], false);
+  "__builtin_ldexpf",  (floatType, [ floatType; intType  ], false);
+  "__builtin_ldexpl",  (longDoubleType, [ longDoubleType; 
+                                                intType  ], false);
+
+  "__builtin_log",  (doubleType, [ doubleType ], false);
+  "__builtin_logf",  (floatType, [ floatType ], false);
+  "__builtin_logl",  (longDoubleType, [ longDoubleType ], false);
+
+  "__builtin_log10",  (doubleType, [ doubleType ], false);
+  "__builtin_log10f",  (floatType, [ floatType ], false);
+  "__builtin_log10l",  (longDoubleType, [ longDoubleType ], false);
+
+  "__builtin_modff",  (floatType, [ floatType; 
+                                          TPtr(floatType,[]) ], false);
+  "__builtin_modfl",  (longDoubleType, [ longDoubleType; 
+                                               TPtr(longDoubleType, []) ], 
+                             false);
+
+  "__builtin_nan",  (doubleType, [ charConstPtrType ], false);
+  "__builtin_nanf",  (floatType, [ charConstPtrType ], false);
+  "__builtin_nanl",  (longDoubleType, [ charConstPtrType ], false);
+  "__builtin_nans",  (doubleType, [ charConstPtrType ], false);
+  "__builtin_nansf",  (floatType, [ charConstPtrType ], false);
+  "__builtin_nansl",  (longDoubleType, [ charConstPtrType ], false);
+  "__builtin_next_arg",  (voidPtrType, [], false);
+  "__builtin_object_size",  (sizeType, [ voidPtrType; intType ], false);
+
+  "__builtin_parity",  (intType, [ uintType ], false);
+  "__builtin_parityl",  (intType, [ ulongType ], false);
+  "__builtin_parityll",  (intType, [ ulongLongType ], false);
+
+  "__builtin_popcount",  (intType, [ uintType ], false);
+  "__builtin_popcountl",  (intType, [ ulongType ], false);
+  "__builtin_popcountll",  (intType, [ ulongLongType ], false);
+
+  "__builtin_powi",  (doubleType, [ doubleType; intType ], false);
+  "__builtin_powif",  (floatType, [ floatType; intType ], false);
+  "__builtin_powil",  (longDoubleType, [ longDoubleType; intType ], false);
+  "__builtin_prefetch",  (voidType, [ voidConstPtrType ], true);
+  "__builtin_return",  (voidType, [ voidConstPtrType ], false);
+  "__builtin_return_address",  (voidPtrType, [ uintType ], false);
+
+  "__builtin_sin",  (doubleType, [ doubleType ], false);
+  "__builtin_sinf",  (floatType, [ floatType ], false);
+  "__builtin_sinl",  (longDoubleType, [ longDoubleType ], false);
+
+  "__builtin_sinh",  (doubleType, [ doubleType ], false);
+  "__builtin_sinhf",  (floatType, [ floatType ], false);
+  "__builtin_sinhl",  (longDoubleType, [ longDoubleType ], false);
+
+  "__builtin_sqrt",  (doubleType, [ doubleType ], false);
+  "__builtin_sqrtf",  (floatType, [ floatType ], false);
+  "__builtin_sqrtl",  (longDoubleType, [ longDoubleType ], false);
+
+  "__builtin_stpcpy",  (charPtrType, [ charPtrType; charConstPtrType ], false);
+  "__builtin_strchr",  (charPtrType, [ charPtrType; charType ], false);
+  "__builtin_strcmp",  (intType, [ charConstPtrType; charConstPtrType ], false);
+  "__builtin_strcpy",  (charPtrType, [ charPtrType; charConstPtrType ], false);
+  "__builtin_strcspn",  (uintType, [ charConstPtrType; charConstPtrType ], false);
+  "__builtin_strncat",  (charPtrType, [ charPtrType; charConstPtrType; sizeType ], false);
+  "__builtin_strncmp",  (intType, [ charConstPtrType; charConstPtrType; sizeType ], false);
+  "__builtin_strncpy",  (charPtrType, [ charPtrType; charConstPtrType; sizeType ], false);
+  "__builtin_strspn",  (intType, [ charConstPtrType; charConstPtrType ], false);
+  "__builtin_strpbrk",  (charPtrType, [ charConstPtrType; charConstPtrType ], false);
+  (* When we parse builtin_types_compatible_p, we change its interface *)
+  "__builtin_types_compatible_p", 
+                              (intType, [ uintType; (* Sizeof the type *)
+                                          uintType  (* Sizeof the type *) ],
+                               false);
+  "__builtin_tan",  (doubleType, [ doubleType ], false);
+  "__builtin_tanf",  (floatType, [ floatType ], false);
+  "__builtin_tanl",  (longDoubleType, [ longDoubleType ], false);
+
+  "__builtin_tanh",  (doubleType, [ doubleType ], false);
+  "__builtin_tanhf",  (floatType, [ floatType ], false);
+  "__builtin_tanhl",  (longDoubleType, [ longDoubleType ], false);
+
+  "__builtin_va_end",  (voidType, [ voidPtrType ], false);
+  "__builtin_varargs_start",  
+    (voidType, [ voidPtrType ], false);
+  (* When we elaborate builtin_stdarg_start/builtin_va_start,
+     second argument is passed by address *)
+  "__builtin_va_start",  (voidType, [ voidPtrType; voidPtrType ], false);
+  "__builtin_stdarg_start",  (voidType, [ voidPtrType ], false);
+  (* When we parse builtin_va_arg, type argument becomes sizeof type *)
+  "__builtin_va_arg",  (voidType, [ voidPtrType; sizeType ], false);
+  "__builtin_va_copy",  (voidType, [ voidPtrType;
+                                           voidPtrType ],
+                              false)
+]
+}
diff --git a/cparser/GCC.mli b/cparser/GCC.mli
new file mode 100644
index 00000000..76f40372
--- /dev/null
+++ b/cparser/GCC.mli
@@ -0,0 +1,18 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* GCC built-ins *)
+
+val builtins: Builtins.t
diff --git a/cparser/Main.ml b/cparser/Main.ml
index de286b05..3b93d666 100644
--- a/cparser/Main.ml
+++ b/cparser/Main.ml
@@ -76,6 +76,7 @@ let rec parse_cmdline prepro args i =
   end
 
 let _ =
+  Builtins.set GCC.builtins;
   let args = parse_cmdline [] [] 1 in
   let cmd = "gcc " ^ String.concat " " (List.map Filename.quote args) in
   let rc = Sys.command cmd in
diff --git a/cparser/Makefile b/cparser/Makefile
index 0ecd8f7b..df1d6047 100644
--- a/cparser/Makefile
+++ b/cparser/Makefile
@@ -12,7 +12,8 @@ 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 \
-  Builtins.ml Elab.ml Rename.ml \
+  Builtins.ml GCC.ml \
+  Elab.ml Rename.ml \
   Transform.ml \
   Unblock.ml SimplExpr.ml AddCasts.ml StructByValue.ml StructAssign.ml \
   Bitfields.ml \
diff --git a/cparser/Rename.ml b/cparser/Rename.ml
index fc91b6a9..4b2f3507 100644
--- a/cparser/Rename.ml
+++ b/cparser/Rename.ml
@@ -221,7 +221,7 @@ let rec globdecls env accu = function
 (* Reserve names of builtins *)
 
 let reserve_builtins () =
-  List.fold_left enter_global empty_env Builtins.builtin_idents
+  List.fold_left enter_global empty_env (Builtins.identifiers())
 
 (* Reserve global declarations with public visibility *)
 
diff --git a/cparser/Transform.ml b/cparser/Transform.ml
index 780e38e0..637e9a8e 100644
--- a/cparser/Transform.ml
+++ b/cparser/Transform.ml
@@ -77,4 +77,4 @@ let program
       in
         transf_globdecls env' ({g with gdesc = desc'} :: accu) gl
 
-  in transf_globdecls Builtins.builtin_env [] p
+  in transf_globdecls (Builtins.environment()) [] p