diff options
Diffstat (limited to 'backend/Bounds.v')
-rw-r--r-- | backend/Bounds.v | 2 |
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 |