From fbdff974fe7d2040c25dee1d35781f7e70d87d6c Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 29 Apr 2013 07:51:00 +0000 Subject: Revert suppression of __builtin_{read,write}_reversed for x86 and ARM, for compatibility with earlier CompCert versions. But don't use them in PackedStructs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2216 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cparser/Machine.ml | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) (limited to 'cparser/Machine.ml') diff --git a/cparser/Machine.ml b/cparser/Machine.ml index 0300582..7696444 100644 --- a/cparser/Machine.ml +++ b/cparser/Machine.ml @@ -16,6 +16,7 @@ (* Machine-dependent aspects *) type t = { + name: string; char_signed: bool; sizeof_ptr: int; sizeof_short: int; @@ -45,6 +46,7 @@ type t = { } let ilp32ll64 = { + name = "ilp32ll64"; char_signed = false; sizeof_ptr = 4; sizeof_short = 2; @@ -74,6 +76,7 @@ let ilp32ll64 = { } let i32lpll64 = { + name = "i32lpll64"; char_signed = false; sizeof_ptr = 8; sizeof_short = 2; @@ -103,6 +106,7 @@ let i32lpll64 = { } let il32pll64 = { + name = "il32pll64"; char_signed = false; sizeof_ptr = 8; sizeof_short = 2; @@ -133,11 +137,15 @@ let il32pll64 = { (* Canned configurations for some ABIs *) -let x86_32 = { ilp32ll64 with char_signed = true } -let x86_64 = { i32lpll64 with char_signed = true } -let win64 = { il32pll64 with char_signed = true } -let ppc_32_bigendian = { ilp32ll64 with bigendian = true; bitfields_msb_first = true } -let arm_littleendian = ilp32ll64 +let x86_32 = + { ilp32ll64 with char_signed = true; name = "x86_32" } +let x86_64 = + { i32lpll64 with char_signed = true; name = "x86_64" } +let win64 = + { il32pll64 with char_signed = true; name = "x86_64" } +let ppc_32_bigendian = + { ilp32ll64 with bigendian = true; bitfields_msb_first = true; name = "powerpc" } +let arm_littleendian = { ilp32ll64 with name = "arm" } (* Add GCC extensions re: sizeof and alignof *) -- cgit v1.2.3