aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/extractionMachdep.v
diff options
context:
space:
mode:
Diffstat (limited to 'aarch64/extractionMachdep.v')
-rw-r--r--aarch64/extractionMachdep.v18
1 files changed, 16 insertions, 2 deletions
diff --git a/aarch64/extractionMachdep.v b/aarch64/extractionMachdep.v
index 5f26dc28..ee0e3631 100644
--- a/aarch64/extractionMachdep.v
+++ b/aarch64/extractionMachdep.v
@@ -15,13 +15,27 @@
(* Additional extraction directives specific to the AArch64 port *)
-Require Archi Asm.
+Require Archi Asm Asmgen SelectOp.
(* Archi *)
-Extract Constant Archi.pic_code => "fun () -> false". (* for the time being *)
+Extract Constant Archi.abi =>
+ "match Configuration.abi with
+ | ""apple"" -> Apple
+ | _ -> AAPCS64".
+
+(* SelectOp *)
+
+Extract Constant SelectOp.symbol_is_relocatable =>
+ "match Configuration.system with
+ | ""macosx"" -> C2C.atom_is_extern
+ | _ -> (fun _ -> false)".
(* Asm *)
+
Extract Constant Asm.symbol_low => "fun _ _ _ -> assert false".
Extract Constant Asm.symbol_high => "fun _ _ _ -> assert false".
+
+(* Asmgen *)
+
Extract Constant Asmgen.symbol_is_aligned => "C2C.atom_is_aligned".