1 files changed, 5 insertions, 0 deletions
diff --git a/backend/Reload.v b/backend/Reload.v
index 5728a628..81b61998 100644
--- a/backend/Reload.v
+++ b/backend/Reload.v
@@ -235,6 +235,11 @@ Definition transf_instr
           parallel_move args largs
             (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)
   | LTLin.Llabel lbl =>
       Llabel lbl :: k
   | LTLin.Lgoto lbl =>