diff --git a/cparser/.depend b/cparser/.depend
index d5c86cf7d776bb5376377b497328c35f326ba2ed..9f12718f3b3d0d9e6a127771fccc262a52aff574 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 eb10314d0fd5eb3a99f27e261bfed23e88e3def9..020452f99b85add16c58274e41587ae409b692de 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 853bae93b096f6373d694833f839b57b37e64019..be0d941fdddadf4f3d9f90168247c355a1e22072 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 3c01230ecce793d92772021546798739ff79e3e8..5971d4d433a9c15551281e83c79fd93858d0d092 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 0000000000000000000000000000000000000000..9f864dcd9555eb447baa2fcab58f35dc47007b56
--- /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 0000000000000000000000000000000000000000..76f40372b3b2458acf7fdc2460167a2a2cfae4a7
--- /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 de286b05db1bade54fd7fff3da9ba2d0ae38c0f6..3b93d6668ec2867daae6e8a18b0ac576791218ac 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 0ecd8f7b24c7bfee933c16a706aebf4981e460a6..df1d604767cc7470eefb75a2ccd1c04bf3297eb5 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 fc91b6a9674bae9bf28b3e11e1b8fa869bf4bf68..4b2f350726d204f5fe8b373f06d8601e5e24e253 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 780e38e025a62b4a860ebd63f398df54378b089a..637e9a8e797182a562399287a0c2ed63ab879ca2 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