| Rev | Line | |
|---|
| [486] | 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 | |
|---|
| 18 | type 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 | |
|---|
| 45 | let ilp32ll64 = { |
|---|
| 46 | char_signed = false; |
|---|
| 47 | sizeof_ptr = 4; |
|---|
| 48 | sizeof_short = 2; |
|---|
| 49 | sizeof_int = 4; |
|---|
| 50 | sizeof_long = 4; |
|---|
| 51 | sizeof_longlong = 8; |
|---|
| 52 | sizeof_float = 4; |
|---|
| 53 | sizeof_double = 8; |
|---|
| 54 | sizeof_longdouble = 16; |
|---|
| 55 | sizeof_void = None; |
|---|
| 56 | sizeof_fun = None; |
|---|
| 57 | sizeof_wchar = 4; |
|---|
| 58 | sizeof_size_t = 4; |
|---|
| 59 | sizeof_ptrdiff_t = 4; |
|---|
| 60 | alignof_ptr = 4; |
|---|
| 61 | alignof_short = 2; |
|---|
| 62 | alignof_int = 4; |
|---|
| 63 | alignof_long = 4; |
|---|
| 64 | alignof_longlong = 8; |
|---|
| 65 | alignof_float = 4; |
|---|
| 66 | alignof_double = 8; |
|---|
| 67 | alignof_longdouble = 16; |
|---|
| 68 | alignof_void = None; |
|---|
| 69 | alignof_fun = None |
|---|
| 70 | } |
|---|
| 71 | |
|---|
| 72 | let i32lpll64 = { |
|---|
| 73 | char_signed = false; |
|---|
| 74 | sizeof_ptr = 8; |
|---|
| 75 | sizeof_short = 2; |
|---|
| 76 | sizeof_int = 4; |
|---|
| 77 | sizeof_long = 8; |
|---|
| 78 | sizeof_longlong = 8; |
|---|
| 79 | sizeof_float = 4; |
|---|
| 80 | sizeof_double = 8; |
|---|
| 81 | sizeof_longdouble = 16; |
|---|
| 82 | sizeof_void = None; |
|---|
| 83 | sizeof_fun = None; |
|---|
| 84 | sizeof_wchar = 4; |
|---|
| 85 | sizeof_size_t = 8; |
|---|
| 86 | sizeof_ptrdiff_t = 8; |
|---|
| 87 | alignof_ptr = 8; |
|---|
| 88 | alignof_short = 2; |
|---|
| 89 | alignof_int = 4; |
|---|
| 90 | alignof_long = 8; |
|---|
| 91 | alignof_longlong = 8; |
|---|
| 92 | alignof_float = 4; |
|---|
| 93 | alignof_double = 8; |
|---|
| 94 | alignof_longdouble = 16; |
|---|
| 95 | alignof_void = None; |
|---|
| 96 | alignof_fun = None |
|---|
| 97 | } |
|---|
| 98 | |
|---|
| 99 | let il32pll64 = { |
|---|
| 100 | char_signed = false; |
|---|
| 101 | sizeof_ptr = 8; |
|---|
| 102 | sizeof_short = 2; |
|---|
| 103 | sizeof_int = 4; |
|---|
| 104 | sizeof_long = 4; |
|---|
| 105 | sizeof_longlong = 8; |
|---|
| 106 | sizeof_float = 4; |
|---|
| 107 | sizeof_double = 8; |
|---|
| 108 | sizeof_longdouble = 16; |
|---|
| 109 | sizeof_void = None; |
|---|
| 110 | sizeof_fun = None; |
|---|
| 111 | sizeof_wchar = 4; |
|---|
| 112 | sizeof_size_t = 8; |
|---|
| 113 | sizeof_ptrdiff_t = 8; |
|---|
| 114 | alignof_ptr = 8; |
|---|
| 115 | alignof_short = 2; |
|---|
| 116 | alignof_int = 4; |
|---|
| 117 | alignof_long = 4; |
|---|
| 118 | alignof_longlong = 8; |
|---|
| 119 | alignof_float = 4; |
|---|
| 120 | alignof_double = 8; |
|---|
| 121 | alignof_longdouble = 16; |
|---|
| 122 | alignof_void = None; |
|---|
| 123 | alignof_fun = None |
|---|
| 124 | } |
|---|
| 125 | |
|---|
| 126 | let make_char_signed c = {c with char_signed = true} |
|---|
| 127 | |
|---|
| 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 } |
|---|
| 131 | |
|---|
| 132 | let config = |
|---|
| 133 | ref (match Sys.word_size with |
|---|
| 134 | | 32 -> ilp32ll64 |
|---|
| 135 | | 64 -> if Sys.os_type = "Win32" then il32pll64 else i32lpll64 |
|---|
| 136 | | _ -> assert false) |
|---|
Note: See
TracBrowser
for help on using the repository browser.
