diff options
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 => |