diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-01-23 13:33:33 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-01-23 13:33:33 +0100 |
commit | b5b681b7b55abb18165eaa907b04aefb9b0fddde (patch) | |
tree | 9c0a7df4b20ede85b54fe5c4e5d326fbf30a0013 /cparser/Machine.ml | |
parent | 12803784f2753863985d1030999469c18e01e0f1 (diff) | |
parent | f00b70b6a17fdfb4e8606df891f6becc8102ef12 (diff) | |
download | compcert-kvx-b5b681b7b55abb18165eaa907b04aefb9b0fddde.tar.gz compcert-kvx-b5b681b7b55abb18165eaa907b04aefb9b0fddde.zip |
Merge branch 'master' into dwarf
Diffstat (limited to 'cparser/Machine.ml')
-rw-r--r-- | cparser/Machine.ml | 42 |
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 |