Delay reads from !Machine.config before it is properly initialized.

Several definitions in Cutil and elsewhere were accessing the default
value of !Machine.config, before it is properly initialized in Driver.
Delay evaluation of these definitions, and initialize Machine.config
to nonsensical values so that lack of initialization is caught early
(e.g. in Cutil.find_matching_*_kind).

Also, following up on commit [3b8a094], don't use "wchar_t" typedef
to type wide string literals, even if this typedef is in scope.
The risk here is to hide an inconsistency between "wchar_t"'s definition
in standard headers and CompCert's built-in definition.

1 files changed, 12 insertions, 20 deletions

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 }