summaryrefslogtreecommitdiff
path: root/cparser/Machine.ml
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-03-03 10:22:27 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-03-03 10:22:27 +0000
commit891377ce1962cdb31357d6580d6546ec22df2b4f (patch)
tree4ff7c38749cc7a4c1af411c5aa3eb7225c4ae6a1 /cparser/Machine.ml
parent018edf2d81bf94197892cf1df221f7eeac1f96f6 (diff)
Switching to the new C parser/elaborator/simplifier
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cparser/Machine.ml')
-rw-r--r--cparser/Machine.ml136
1 files changed, 136 insertions, 0 deletions
diff --git a/cparser/Machine.ml b/cparser/Machine.ml
new file mode 100644
index 0000000..21b3daa
--- /dev/null
+++ b/cparser/Machine.ml
@@ -0,0 +1,136 @@
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Xavier Leroy, INRIA Paris-Rocquencourt *)
+(* *)
+(* Copyright Institut National de Recherche en Informatique et en *)
+(* Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the GNU General Public License as published by *)
+(* the Free Software Foundation, either version 2 of the License, or *)
+(* (at your option) any later version. This file is also distributed *)
+(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(* *)
+(* *********************************************************************)
+
+(* Machine-dependent aspects *)
+
+type t = {
+ char_signed: bool;
+ sizeof_ptr: int;
+ sizeof_short: int;
+ sizeof_int: int;
+ sizeof_long: int;
+ sizeof_longlong: int;
+ sizeof_float: int;
+ sizeof_double: int;
+ sizeof_longdouble: int;
+ sizeof_void: int option;
+ sizeof_fun: int option;
+ sizeof_wchar: int;
+ sizeof_size_t: int;
+ sizeof_ptrdiff_t: int;
+ alignof_ptr: int;
+ alignof_short: int;
+ alignof_int: int;
+ alignof_long: int;
+ alignof_longlong: int;
+ alignof_float: int;
+ alignof_double: int;
+ alignof_longdouble: int;
+ alignof_void: int option;
+ alignof_fun: int option
+}
+
+let ilp32ll64 = {
+ char_signed = false;
+ sizeof_ptr = 4;
+ sizeof_short = 2;
+ sizeof_int = 4;
+ sizeof_long = 4;
+ sizeof_longlong = 8;
+ sizeof_float = 4;
+ sizeof_double = 8;
+ sizeof_longdouble = 16;
+ sizeof_void = None;
+ sizeof_fun = None;
+ sizeof_wchar = 4;
+ sizeof_size_t = 4;
+ sizeof_ptrdiff_t = 4;
+ alignof_ptr = 4;
+ alignof_short = 2;
+ alignof_int = 4;
+ alignof_long = 4;
+ alignof_longlong = 8;
+ alignof_float = 4;
+ alignof_double = 8;
+ alignof_longdouble = 16;
+ alignof_void = None;
+ alignof_fun = None
+}
+
+let i32lpll64 = {
+ char_signed = false;
+ sizeof_ptr = 8;
+ sizeof_short = 2;
+ sizeof_int = 4;
+ sizeof_long = 8;
+ sizeof_longlong = 8;
+ sizeof_float = 4;
+ sizeof_double = 8;
+ sizeof_longdouble = 16;
+ sizeof_void = None;
+ sizeof_fun = None;
+ sizeof_wchar = 4;
+ sizeof_size_t = 8;
+ sizeof_ptrdiff_t = 8;
+ alignof_ptr = 8;
+ alignof_short = 2;
+ alignof_int = 4;
+ alignof_long = 8;
+ alignof_longlong = 8;
+ alignof_float = 4;
+ alignof_double = 8;
+ alignof_longdouble = 16;
+ alignof_void = None;
+ alignof_fun = None
+}
+
+let il32pll64 = {
+ char_signed = false;
+ sizeof_ptr = 8;
+ sizeof_short = 2;
+ sizeof_int = 4;
+ sizeof_long = 4;
+ sizeof_longlong = 8;
+ sizeof_float = 4;
+ sizeof_double = 8;
+ sizeof_longdouble = 16;
+ sizeof_void = None;
+ sizeof_fun = None;
+ sizeof_wchar = 4;
+ sizeof_size_t = 8;
+ sizeof_ptrdiff_t = 8;
+ alignof_ptr = 8;
+ alignof_short = 2;
+ alignof_int = 4;
+ alignof_long = 4;
+ alignof_longlong = 8;
+ alignof_float = 4;
+ alignof_double = 8;
+ alignof_longdouble = 16;
+ alignof_void = None;
+ alignof_fun = None
+}
+
+let make_char_signed c = {c with char_signed = true}
+
+let gcc_extensions c =
+ { c with sizeof_void = Some 1; sizeof_fun = Some 1;
+ alignof_void = Some 1; alignof_fun = Some 1 }
+
+let config =
+ ref (match Sys.word_size with
+ | 32 -> ilp32ll64
+ | 64 -> if Sys.os_type = "Win32" then il32pll64 else i32lpll64
+ | _ -> assert false)