aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Machine.ml
diff options
context:
space:
mode:
authorXavier Leroy <xavierleroy@users.noreply.github.com>2019-09-11 15:13:12 +0200
committerGitHub <noreply@github.com>2019-09-11 15:13:12 +0200
commit7601fb5e792a5305336e5cda9794c4041d053b95 (patch)
treef0dc0acd7bb5ad6dae80e4389fb165fa93eb3cb8 /cparser/Machine.ml
parentd3eba50731c23546c6e9ccb14230460fc1da592e (diff)
parentc243b565ab0744086e10efcfee16768f6c3cf880 (diff)
downloadcompcert-7601fb5e792a5305336e5cda9794c4041d053b95.tar.gz
compcert-7601fb5e792a5305336e5cda9794c4041d053b95.zip
Merge pull request #313 from AbsInt/aarch64
Support target architecture AArch64 (ARMv8 in 64-bit mode)
Diffstat (limited to 'cparser/Machine.ml')
-rw-r--r--cparser/Machine.ml5
1 files changed, 5 insertions, 0 deletions
diff --git a/cparser/Machine.ml b/cparser/Machine.ml
index 089f2483..97bedb3b 100644
--- a/cparser/Machine.ml
+++ b/cparser/Machine.ml
@@ -237,6 +237,11 @@ let rv64 =
struct_passing_style = SP_ref_callee; (* Wrong *)
struct_return_style = SR_ref } (* to check *)
+let aarch64 =
+ { i32lpll64 with name = "aarch64";
+ struct_passing_style = SP_ref_callee; (* Wrong *)
+ struct_return_style = SR_ref } (* Wrong *)
+
(* Add GCC extensions re: sizeof and alignof *)
let gcc_extensions c =