1 (* *********************************************************************)
3 (* The Compcert verified compiler *)
5 (* Xavier Leroy, INRIA Paris-Rocquencourt *)
7 (* Copyright Institut National de Recherche en Informatique et en *)
8 (* Automatique. All rights reserved. This file is distributed *)
9 (* under the terms of the GNU General Public License as published by *)
10 (* the Free Software Foundation, either version 2 of the License, or *)
11 (* (at your option) any later version. This file is also distributed *)
12 (* under the terms of the INRIA Non-Commercial License Agreement. *)
14 (* *********************************************************************)
16 (* Machine-dependent aspects *)
27 sizeof_longdouble: int;
28 sizeof_void: int option;
29 sizeof_fun: int option;
32 sizeof_ptrdiff_t: int;
37 alignof_longlong: int;
40 alignof_longdouble: int;
41 alignof_void: int option;
42 alignof_fun: int option
54 sizeof_longdouble = 16;
67 alignof_longdouble = 16;
81 sizeof_longdouble = 16;
94 alignof_longdouble = 16;
108 sizeof_longdouble = 16;
113 sizeof_ptrdiff_t = 8;
118 alignof_longlong = 8;
121 alignof_longdouble = 16;
126 let make_char_signed c = {c with char_signed = true}
128 let gcc_extensions c =
129 { c with sizeof_void = Some 1; sizeof_fun = Some 1;
130 alignof_void = Some 1; alignof_fun = Some 1 }
133 ref (match Sys.word_size with
135 | 64 -> if Sys.os_type = "Win32" then il32pll64 else i32lpll64