diff options
Diffstat (limited to 'aarch64/Machregs.v')
| -rw-r--r-- | aarch64/Machregs.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/aarch64/Machregs.v b/aarch64/Machregs.v index 704c392e..f9b9fd79 100644 --- a/aarch64/Machregs.v +++ b/aarch64/Machregs.v @@ -156,18 +156,18 @@ Fixpoint destroyed_by_clobber (cl: list string): list mreg := Definition destroyed_by_builtin (ef: external_function): list mreg := match ef with - | EF_memcpy sz al => R15 :: R17 :: R29 :: nil + | EF_memcpy sz al => R14 :: R15 :: R17 :: nil | EF_inline_asm txt sg clob => destroyed_by_clobber clob | _ => nil end. Definition destroyed_by_setstack (ty: typ): list mreg := nil. -Definition destroyed_at_function_entry: list mreg := R29 :: nil. +Definition destroyed_at_function_entry: list mreg := R15 :: nil. Definition destroyed_at_indirect_call: list mreg := nil. -Definition temp_for_parent_frame: mreg := R29. +Definition temp_for_parent_frame: mreg := R15. Definition mregs_for_operation (op: operation): list (option mreg) * option mreg := (nil, None). |