diff options
Diffstat (limited to 'aarch64/Asmgen.v')
| -rw-r--r-- | aarch64/Asmgen.v | 13 |
1 files changed, 4 insertions, 9 deletions
diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index 024c9a17..683530d4 100644 --- a/aarch64/Asmgen.v +++ b/aarch64/Asmgen.v @@ -969,8 +969,8 @@ Definition transl_addressing (sz: Z) (addr: Op.addressing) (args: list mreg) (** Translation of loads and stores *) Definition transl_load (trap: trapping_mode) - (chunk: memory_chunk) (addr: Op.addressing) - (args: list mreg) (dst: mreg) (k: code) : res code := + (chunk: memory_chunk) (addr: Op.addressing) + (args: list mreg) (dst: mreg) (k: code) : res code := match trap with | NOTRAP => Error (msg "Asmgen.transl_load non-trapping loads unsupported on aarch64") | TRAP => @@ -1061,13 +1061,8 @@ Definition storeptr (src: ireg) (base: iregsp) (ofs: ptrofs) (k: code) := (** Function epilogue *) Definition make_epilogue (f: Mach.function) (k: code) := - (* FIXME - Cannot be used because memcpy destroys X30; - issue being discussed with X. Leroy *) - (* if is_leaf_function f - then Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k - else*) loadptr XSP f.(fn_retaddr_ofs) RA - (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k). + loadptr XSP f.(fn_retaddr_ofs) RA + (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k). (** Translation of a Mach instruction. *) |