1 files changed, 2 insertions, 0 deletions
diff --git a/backend/Bounds.v b/backend/Bounds.v
index 15468c57..514895be 100644
--- a/backend/Bounds.v
+++ b/backend/Bounds.v
@@ -72,6 +72,7 @@ Definition instr_within_bounds (i: instruction) :=
   | Lop op args res => mreg_within_bounds res
   | Lload chunk addr args dst => mreg_within_bounds dst
   | Lcall sig ros => size_arguments sig <= bound_outgoing b
+  | Lbuiltin ef args res => mreg_within_bounds res
   | _ => True
   end.
 
@@ -103,6 +104,7 @@ Definition regs_of_instr (i: instruction) : list mreg :=
   | Lstore chunk addr args src => nil
   | Lcall sig ros => nil
   | Ltailcall sig ros => nil
+  | Lbuiltin ef args res => res :: nil
   | Llabel lbl => nil
   | Lgoto lbl => nil
   | Lcond cond args lbl => nil