diff options
Diffstat (limited to 'aarch64/Archi.v')
| -rw-r--r-- | aarch64/Archi.v | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/aarch64/Archi.v b/aarch64/Archi.v index 42500e70..91e91673 100644 --- a/aarch64/Archi.v +++ b/aarch64/Archi.v @@ -85,6 +85,10 @@ Global Opaque ptr64 big_endian splitlong fma_order fma_invalid_mul_is_nan float_of_single_preserves_sNaN. -(** Whether to generate position-independent code or not *) +(** Which ABI to implement *) -Parameter pic_code: unit -> bool. +Inductive abi_kind: Type := + | AAPCS64 (**r ARM's standard as used in Linux and other ELF platforms *) + | Apple. (**r the variant used in macOS and iOS *) + +Parameter abi: abi_kind. |