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, 36 insertions, 6 deletions

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