aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--cfrontend/C2C.ml4
-rw-r--r--cparser/Ceval.ml2
-rw-r--r--cparser/Cutil.ml32
-rw-r--r--cparser/Cutil.mli12
-rw-r--r--cparser/Elab.ml16
-rw-r--r--cparser/GCC.ml46
-rw-r--r--cparser/Machine.ml42
-rw-r--r--cparser/PackedStructs.ml2
8 files changed, 88 insertions, 68 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 584c265a..fddbfd30 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -137,8 +137,8 @@ let builtins_generic = {
(TVoid [],
[TPtr(TVoid [], []);
TPtr(TVoid [AConst], []);
- TInt(Cutil.size_t_ikind, []);
- TInt(Cutil.size_t_ikind, [])],
+ TInt(IUInt, []);
+ TInt(IUInt, [])],
false);
(* Annotations *)
"__builtin_annot",
diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml
index 39cda58c..ba7cdabc 100644
--- a/cparser/Ceval.ml
+++ b/cparser/Ceval.ml
@@ -102,7 +102,7 @@ let cast env ty_to ty_from v =
then v
else raise Notconst
| TPtr(ty, _), I n ->
- I (normalize_int n ptr_t_ikind)
+ I (normalize_int n (ptr_t_ikind ()))
| TPtr(ty, _), (S _ | WS _) ->
v
| TEnum(_, _), I n ->
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 9093b230..9e7f102e 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -707,41 +707,34 @@ let type_of_member env fld =
(** Special types *)
let find_matching_unsigned_ikind sz =
+ assert (sz > 0);
if sz = !config.sizeof_int then IUInt
else if sz = !config.sizeof_long then IULong
else if sz = !config.sizeof_longlong then IULongLong
else assert false
let find_matching_signed_ikind sz =
+ assert (sz > 0);
if sz = !config.sizeof_int then IInt
else if sz = !config.sizeof_long then ILong
else if sz = !config.sizeof_longlong then ILongLong
else assert false
-let wchar_ikind =
+let wchar_ikind () =
if !config.wchar_signed
then find_matching_signed_ikind !config.sizeof_wchar
else find_matching_unsigned_ikind !config.sizeof_wchar
-let size_t_ikind = find_matching_unsigned_ikind !config.sizeof_size_t
-let ptr_t_ikind = find_matching_unsigned_ikind !config.sizeof_ptr
-let ptrdiff_t_ikind = find_matching_signed_ikind !config.sizeof_ptrdiff_t
-
-(** The wchar_t type. Try to get it from a typedef in the environment,
- otherwise use the integer type described in !config. *)
-
-let wchar_type env =
- try
- let (id, def) = Env.lookup_typedef env "wchar_t" in TNamed(id, [])
- with Env.Error _ ->
- TInt(wchar_ikind, [])
+let size_t_ikind () = find_matching_unsigned_ikind !config.sizeof_size_t
+let ptr_t_ikind () = find_matching_unsigned_ikind !config.sizeof_ptr
+let ptrdiff_t_ikind () = find_matching_signed_ikind !config.sizeof_ptrdiff_t
(** The type of a constant *)
-let type_of_constant env = function
+let type_of_constant = function
| CInt(_, ik, _) -> TInt(ik, [])
| CFloat(_, fk) -> TFloat(fk, [])
| CStr _ -> TPtr(TInt(IChar, []), [])
- | CWStr _ -> TPtr(wchar_type env, [])
+ | CWStr _ -> TPtr(TInt(wchar_ikind(), []), [])
| CEnum(_, _) -> TInt(IInt, [])
(* Check that a C expression is a lvalue *)
@@ -829,15 +822,14 @@ let floatconst0 =
{ edesc = EConst(CFloat({hex=false; intPart="0"; fracPart="0"; exp="0"}, FDouble));
etyp = TFloat(FDouble, []) }
-(* Construct the literal "0" with void * type *)
-
-let nullconst =
- { edesc = EConst(CInt(0L, ptr_t_ikind, "0")); etyp = TPtr(TVoid [], []) }
-
(* Construct a cast expression *)
let ecast ty e = { edesc = ECast(ty, e); etyp = ty }
+(* Construct the literal "0" with void * type *)
+
+let nullconst = ecast (TPtr(TVoid [], [])) (intconst 0L IInt)
+
(* Construct an assignment expression *)
let eassign e1 e2 = { edesc = EBinop(Oassign, e1, e2, e1.etyp); etyp = e1.etyp }
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index 53bcfcea..bd52badf 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -156,20 +156,20 @@ val default_argument_conversion : Env.t -> typ -> typ
(* Special types *)
val enum_ikind : ikind
(* Integer kind for enum values. Always [IInt]. *)
-val wchar_ikind : ikind
- (* Integer kind for wchar_t type. Unsigned. *)
-val size_t_ikind : ikind
+val wchar_ikind : unit -> ikind
+ (* Integer kind for wchar_t type. *)
+val size_t_ikind : unit -> ikind
(* Integer kind for size_t type. Unsigned. *)
-val ptr_t_ikind : ikind
+val ptr_t_ikind : unit -> ikind
(* Integer kind for ptr_t type. Smallest unsigned kind large enough
to contain a pointer without information loss. *)
-val ptrdiff_t_ikind : ikind
+val ptrdiff_t_ikind : unit -> ikind
(* Integer kind for ptrdiff_t type. Smallest signed kind large enough
to contain the difference between two pointers. *)
(* Helpers for type-checking *)
-val type_of_constant : Env.t -> constant -> typ
+val type_of_constant : constant -> typ
(* Return the type of the given constant. *)
val type_of_member : Env.t -> field -> typ
(* Return the type of accessing the given field [fld].
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index faffc36f..bad92cf6 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1198,7 +1198,7 @@ let elab_expr loc env a =
| CONSTANT cst ->
let cst' = elab_constant loc cst in
- { edesc = EConst cst'; etyp = type_of_constant env cst' }
+ { edesc = EConst cst'; etyp = type_of_constant cst' }
(* 6.5.2 Postfix expressions *)
@@ -1339,31 +1339,31 @@ let elab_expr loc env a =
match b1.edesc with
| EConst(CStr s) ->
let sz = String.length s + 1 in
- EConst(CInt(Int64.of_int sz, size_t_ikind, ""))
+ EConst(CInt(Int64.of_int sz, size_t_ikind(), ""))
| EConst(CWStr s) ->
let sz = (!config).sizeof_wchar * (List.length s + 1) in
- EConst(CInt(Int64.of_int sz, size_t_ikind, ""))
+ EConst(CInt(Int64.of_int sz, size_t_ikind(), ""))
| _ ->
ESizeof b1.etyp in
- { edesc = bdesc; etyp = TInt(size_t_ikind, []) }
+ { edesc = bdesc; etyp = TInt(size_t_ikind(), []) }
| TYPE_SIZEOF (spec, dcl) ->
let (ty, env') = elab_type loc env spec dcl in
if wrap incomplete_type loc env' ty then
err "incomplete type %a" Cprint.typ ty;
- { edesc = ESizeof ty; etyp = TInt(size_t_ikind, []) }
+ { edesc = ESizeof ty; etyp = TInt(size_t_ikind(), []) }
| EXPR_ALIGNOF a1 ->
let b1 = elab a1 in
if wrap incomplete_type loc env b1.etyp then
err "incomplete type %a" Cprint.typ b1.etyp;
- { edesc = EAlignof b1.etyp; etyp = TInt(size_t_ikind, []) }
+ { edesc = EAlignof b1.etyp; etyp = TInt(size_t_ikind(), []) }
| TYPE_ALIGNOF (spec, dcl) ->
let (ty, env') = elab_type loc env spec dcl in
if wrap incomplete_type loc env' ty then
err "incomplete type %a" Cprint.typ ty;
- { edesc = EAlignof ty; etyp = TInt(size_t_ikind, []) }
+ { edesc = EAlignof ty; etyp = TInt(size_t_ikind(), []) }
| UNARY(PLUS, a1) ->
let b1 = elab a1 in
@@ -1465,7 +1465,7 @@ let elab_expr loc env a =
err "illegal pointer arithmetic in binary '-'";
if wrap sizeof loc env ty1 = Some 0 then
err "subtraction between two pointers to zero-sized objects";
- (TPtr(ty1, []), TInt(ptrdiff_t_ikind, []))
+ (TPtr(ty1, []), TInt(ptrdiff_t_ikind(), []))
| _, _ -> error "type error in binary '-'"
end in
{ edesc = EBinop(Osub, b1, b2, tyop); etyp = tyres }
diff --git a/cparser/GCC.ml b/cparser/GCC.ml
index 1bcbbbc8..030f300b 100644
--- a/cparser/GCC.ml
+++ b/cparser/GCC.ml
@@ -35,7 +35,7 @@ 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 sizeType() = TInt(size_t_ikind(), [])
let builtins = {
Builtins.typedefs = [
@@ -43,22 +43,22 @@ let builtins = {
];
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___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___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___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);
@@ -124,8 +124,8 @@ let builtins = {
"__builtin_inf", (doubleType, [], false);
"__builtin_inff", (floatType, [], false);
"__builtin_infl", (longDoubleType, [], false);
- "__builtin_memcpy", (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType ], false);
- "__builtin_mempcpy", (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType ], false);
+ "__builtin_memcpy", (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType() ], false);
+ "__builtin_mempcpy", (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType() ], false);
"__builtin_fmod", (doubleType, [ doubleType ], false);
"__builtin_fmodf", (floatType, [ floatType ], false);
@@ -162,7 +162,7 @@ let builtins = {
"__builtin_nansf", (floatType, [ charConstPtrType ], false);
"__builtin_nansl", (longDoubleType, [ charConstPtrType ], false);
"__builtin_next_arg", (voidPtrType, [], false);
- "__builtin_object_size", (sizeType, [ voidPtrType; intType ], false);
+ "__builtin_object_size", (sizeType(), [ voidPtrType; intType ], false);
"__builtin_parity", (intType, [ uintType ], false);
"__builtin_parityl", (intType, [ ulongType ], false);
@@ -196,9 +196,9 @@ let builtins = {
"__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_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);
"__builtin_tan", (doubleType, [ doubleType ], false);
@@ -217,9 +217,7 @@ let builtins = {
"__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)
+ "__builtin_va_arg", (voidType, [ voidPtrType; sizeType() ], false);
+ "__builtin_va_copy", (voidType, [ voidPtrType; voidPtrType ], false)
]
}
diff --git a/cparser/Machine.ml b/cparser/Machine.ml
index 6a7f5054..b215505b 100644
--- a/cparser/Machine.ml
+++ b/cparser/Machine.ml
@@ -173,10 +173,40 @@ let gcc_extensions c =
{ c with sizeof_void = Some 1; sizeof_fun = Some 1;
alignof_void = Some 1; alignof_fun = Some 1 }
-(* Default configuration *)
+(* Undefined configuration *)
-let config =
- ref (match Sys.word_size with
- | 32 -> if Sys.os_type = "Win32" then win32 else ilp32ll64
- | 64 -> if Sys.os_type = "Win32" then win64 else i32lpll64
- | _ -> assert false)
+let undef = {
+ name = "UNDEFINED";
+ char_signed = false;
+ sizeof_ptr = 0;
+ sizeof_short = 0;
+ sizeof_int = 0;
+ sizeof_long = 0;
+ sizeof_longlong = 0;
+ sizeof_float = 0;
+ sizeof_double = 0;
+ sizeof_longdouble = 0;
+ sizeof_void = None;
+ sizeof_fun = None;
+ sizeof_wchar = 0;
+ wchar_signed = true;
+ sizeof_size_t = 0;
+ sizeof_ptrdiff_t = 0;
+ alignof_ptr = 0;
+ alignof_short = 0;
+ alignof_int = 0;
+ alignof_long = 0;
+ alignof_longlong = 0;
+ alignof_float = 0;
+ alignof_double = 0;
+ alignof_longdouble = 0;
+ alignof_void = None;
+ alignof_fun = None;
+ bigendian = false;
+ bitfields_msb_first = false;
+ struct_return_as_int = 0
+}
+
+(* The current configuration. Must be initialized before use. *)
+
+let config = ref undef
diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml
index 686a7d39..1f602fc1 100644
--- a/cparser/PackedStructs.ml
+++ b/cparser/PackedStructs.ml
@@ -138,7 +138,7 @@ let accessor_type loc env ty =
match unroll env ty with
| TInt(ik,_) -> (8 * sizeof_ikind ik, TInt(unsigned_ikind_of ik,[]))
| TEnum(_,_) -> (8 * sizeof_ikind enum_ikind, TInt(unsigned_ikind_of enum_ikind,[]))
- | TPtr _ -> (8 * !config.sizeof_ptr, TInt(ptr_t_ikind,[]))
+ | TPtr _ -> (8 * !config.sizeof_ptr, TInt(ptr_t_ikind(),[]))
| _ ->
error "%a: unsupported type for byte-swapped field access" formatloc loc;
(32, TVoid [])
generated by cgit (git 2.34.1) at 2024-06-02 16:57:49 +0000