aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Machine.ml
diff options
context:
space:
mode:
authorxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-12-20 13:13:29 +0000
committerxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-12-20 13:13:29 +0000
commit1c768ee3ff91e826f52cf08e1aaa8c4d637240f5 (patch)
tree2e3b505567304d8795b06ff9b2485e230214d923 /cparser/Machine.ml
parent7698300cfe2d3f944ce2e1d4a60a263620487718 (diff)
downloadcompcert-kvx-1c768ee3ff91e826f52cf08e1aaa8c4d637240f5.tar.gz
compcert-kvx-1c768ee3ff91e826f52cf08e1aaa8c4d637240f5.zip
Hack StructReturn to better adhere to PowerPC and ARM calling conventions.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2382 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cparser/Machine.ml')
-rw-r--r--cparser/Machine.ml27
1 files changed, 18 insertions, 9 deletions
diff --git a/cparser/Machine.ml b/cparser/Machine.ml
index 7696444c..374e1bb9 100644
--- a/cparser/Machine.ml
+++ b/cparser/Machine.ml
@@ -42,7 +42,8 @@ type t = {
alignof_void: int option;
alignof_fun: int option;
bigendian: bool;
- bitfields_msb_first: bool
+ bitfields_msb_first: bool;
+ struct_return_as_int: int
}
let ilp32ll64 = {
@@ -72,7 +73,8 @@ let ilp32ll64 = {
alignof_void = None;
alignof_fun = None;
bigendian = false;
- bitfields_msb_first = false
+ bitfields_msb_first = false;
+ struct_return_as_int = 0
}
let i32lpll64 = {
@@ -102,7 +104,8 @@ let i32lpll64 = {
alignof_void = None;
alignof_fun = None;
bigendian = false;
- bitfields_msb_first = false
+ bitfields_msb_first = false;
+ struct_return_as_int = 0
}
let il32pll64 = {
@@ -132,20 +135,26 @@ let il32pll64 = {
alignof_void = None;
alignof_fun = None;
bigendian = false;
- bitfields_msb_first = false
+ bitfields_msb_first = false;
+ struct_return_as_int = 0
}
(* Canned configurations for some ABIs *)
let x86_32 =
- { ilp32ll64 with char_signed = true; name = "x86_32" }
+ { ilp32ll64 with name = "x86_32"; char_signed = true }
let x86_64 =
- { i32lpll64 with char_signed = true; name = "x86_64" }
+ { i32lpll64 with name = "x86_64"; char_signed = true }
let win64 =
- { il32pll64 with char_signed = true; name = "x86_64" }
+ { il32pll64 with name = "x86_64"; char_signed = true }
let ppc_32_bigendian =
- { ilp32ll64 with bigendian = true; bitfields_msb_first = true; name = "powerpc" }
-let arm_littleendian = { ilp32ll64 with name = "arm" }
+ { ilp32ll64 with name = "powerpc";
+ bigendian = true;
+ bitfields_msb_first = true;
+ struct_return_as_int = 8 }
+let arm_littleendian =
+ { ilp32ll64 with name = "arm";
+ struct_return_as_int = 4 }
(* Add GCC extensions re: sizeof and alignof *)