diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-27 16:19:03 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-27 16:19:03 +0100 |
| commit | b1cd0ff83ec434b09195fe16eebaa8e73fb9c39b (patch) | |
| tree | 44a66f0d3f31e97ebc6365f8e973d61d7a1b2e4b /aarch64/Asmgen.v | |
| parent | 4dabb8cd9b292bb873155e02e430f79cb43dc629 (diff) | |
| parent | e991d17839bf1c4736bdb5d8cbbd956be6fb2a1e (diff) | |
| download | compcert-kvx-b1cd0ff83ec434b09195fe16eebaa8e73fb9c39b.tar.gz compcert-kvx-b1cd0ff83ec434b09195fe16eebaa8e73fb9c39b.zip | |
Merge branch 'dm-leaf' of https://github.com/monniaux/CompCert into mppa-work
Diffstat (limited to 'aarch64/Asmgen.v')
| -rw-r--r-- | aarch64/Asmgen.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index 46dd875d..f4446696 100644 --- a/aarch64/Asmgen.v +++ b/aarch64/Asmgen.v @@ -1061,8 +1061,10 @@ Definition storeptr (src: ireg) (base: iregsp) (ofs: ptrofs) (k: code) := (** Function epilogue *) Definition make_epilogue (f: Mach.function) (k: code) := - loadptr XSP f.(fn_retaddr_ofs) RA - (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k). + 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). (** Translation of a Mach instruction. *) |