source: Deliverables/D2.2/8051/cparser/Machine.mli

Last change on this file was 486, checked in by ayache, 9 years ago

Deliverable D2.2

File size: 1.7 KB
Line 
1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
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.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16(* Machine-dependent aspects *)
17
18type t = {
19  char_signed: bool;
20  sizeof_ptr: int;
21  sizeof_short: int;
22  sizeof_int: int;
23  sizeof_long: int;
24  sizeof_longlong: int;
25  sizeof_float: int;
26  sizeof_double: int;
27  sizeof_longdouble: int;
28  sizeof_void: int option;
29  sizeof_fun: int option;
30  sizeof_wchar: int;
31  sizeof_size_t: int;
32  sizeof_ptrdiff_t: int;
33  alignof_ptr: int;
34  alignof_short: int;
35  alignof_int: int;
36  alignof_long: int;
37  alignof_longlong: int;
38  alignof_float: int;
39  alignof_double: int;
40  alignof_longdouble: int;
41  alignof_void: int option;
42  alignof_fun: int option
43}
44
45val ilp32ll64 : t
46val i32lpll64 : t
47val il32pll64 : t
48val make_char_signed : t -> t
49val gcc_extensions : t -> t
50
51val config : t ref
Note: See TracBrowser for help on using the repository browser.