diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-06-13 18:11:19 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-06-13 18:11:19 +0000 |
commit | a5ffc59246b09a389e5f8cbc2f217e323e76990f (patch) | |
tree | e1bc7cc54518aad7c20645f187cee8110de8cff9 /backend/Reload.v | |
parent | 4daccd62b92b23016d3f343d5691f9c164a8a951 (diff) | |
download | compcert-kvx-a5ffc59246b09a389e5f8cbc2f217e323e76990f.tar.gz compcert-kvx-a5ffc59246b09a389e5f8cbc2f217e323e76990f.zip |
Revised handling of annotation statements, and more generally built-in functions, and more generally external functions
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1672 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Reload.v')
-rw-r--r-- | backend/Reload.v | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/backend/Reload.v b/backend/Reload.v index 81b61998..0ad53e6e 100644 --- a/backend/Reload.v +++ b/backend/Reload.v @@ -236,10 +236,13 @@ Definition transf_instr (Ltailcall sig (inr _ id) :: k) end | LTLin.Lbuiltin ef args dst => - let rargs := regs_for args in - let rdst := reg_for dst in - add_reloads args rargs - (Lbuiltin ef rargs rdst :: add_spill rdst dst k) + if ef_reloads ef then + (let rargs := regs_for args in + let rdst := reg_for dst in + add_reloads args rargs + (Lbuiltin ef rargs rdst :: add_spill rdst dst k)) + else + Lannot ef args :: k | LTLin.Llabel lbl => Llabel lbl :: k | LTLin.Lgoto lbl => |