diff options
Diffstat (limited to 'aarch64/Archi.v')
| -rw-r--r-- | aarch64/Archi.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/aarch64/Archi.v b/aarch64/Archi.v index 4911db73..378ca0d1 100644 --- a/aarch64/Archi.v +++ b/aarch64/Archi.v @@ -88,6 +88,10 @@ Global Opaque ptr64 big_endian splitlong (** Which ABI to implement *) +Parameter pic_code: unit -> bool. + +Definition has_notrap_loads := false. + 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 *) |