Merge branch 'master' into dwarf

Conflicts:
	Makefile
	driver/Driver.ml

1 files changed, 21 insertions, 9 deletions

diff --git a/cparser/Machine.ml b/cparser/Machine.ml
index b215505b..bd6489fd 100644
--- a/cparser/Machine.ml
+++ b/cparser/Machine.ml
@@ -44,7 +44,7 @@ type t = {
   alignof_fun: int option;
   bigendian: bool;
   bitfields_msb_first: bool;
-  struct_return_as_int: int
+  supports_unaligned_accesses: bool
 }
 
 let ilp32ll64 = {
@@ -76,7 +76,7 @@ let ilp32ll64 = {
   alignof_fun = None;
   bigendian = false;
   bitfields_msb_first = false;
-  struct_return_as_int = 0
+  supports_unaligned_accesses = false
 }
 
 let i32lpll64 = {
@@ -108,7 +108,7 @@ let i32lpll64 = {
   alignof_fun = None;
   bigendian = false;
   bitfields_msb_first = false;
-  struct_return_as_int = 0
+  supports_unaligned_accesses = false
 }
 
 let il32pll64 = {
@@ -140,7 +140,7 @@ let il32pll64 = {
   alignof_fun = None;
   bigendian = false;
   bitfields_msb_first = false;
-  struct_return_as_int = 0
+  supports_unaligned_accesses = false
 }
 
 (* Canned configurations for some ABIs *)
@@ -149,9 +149,15 @@ let x86_32 =
   { ilp32ll64 with name = "x86_32";
                    char_signed = true;
                    alignof_longlong = 4; alignof_double = 4;
-                   sizeof_longdouble = 12; alignof_longdouble = 4 }
+                   sizeof_longdouble = 12; alignof_longdouble = 4;
+                   supports_unaligned_accesses = true }
+
+let x86_32_macosx =
+  { x86_32 with sizeof_longdouble = 16; alignof_longdouble = 16 }
+
 let x86_64 =
   { i32lpll64 with name = "x86_64"; char_signed = true }
+
 let win32 =
   { ilp32ll64 with name = "win32"; char_signed = true;
                    sizeof_wchar = 2; wchar_signed = false }
@@ -162,10 +168,10 @@ let ppc_32_bigendian =
   { ilp32ll64 with name = "powerpc";
                    bigendian = true;
                    bitfields_msb_first = true;
-                   struct_return_as_int = 8 }
+                   supports_unaligned_accesses = true }
+
 let arm_littleendian =
-  { ilp32ll64 with name = "arm";
-                   struct_return_as_int = 4 }
+  { ilp32ll64 with name = "arm" }
 
 (* Add GCC extensions re: sizeof and alignof *)
 
@@ -173,6 +179,12 @@ let gcc_extensions c =
   { c with sizeof_void = Some 1; sizeof_fun = Some 1;
            alignof_void = Some 1; alignof_fun = Some 1 }
 
+(* Normalize configuration for use with the CompCert reference interpreter *)
+
+let compcert_interpreter c =
+  { c with sizeof_longdouble = 8; alignof_longdouble = 8;
+           supports_unaligned_accesses = false }
+
 (* Undefined configuration *)
 
 let undef = {
@@ -204,7 +216,7 @@ let undef = {
   alignof_fun = None;
   bigendian = false;
   bitfields_msb_first = false;
-  struct_return_as_int = 0
+  supports_unaligned_accesses = false
 }
 
 (* The current configuration.  Must be initialized before use. *)