diff options
Diffstat (limited to 'mppa_k1c/Machregs.v')
| -rw-r--r-- | mppa_k1c/Machregs.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index 2b3fb1aa..f494c67d 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -152,8 +152,7 @@ Definition destroyed_by_store (chunk: memory_chunk) (addr: addressing): list mre Definition destroyed_by_cond (cond: condition): list mreg := nil. -(* Definition destroyed_by_jumptable: list mreg := R5 :: nil. *) -Definition destroyed_by_jumptable: list mreg := nil. +Definition destroyed_by_jumptable: list mreg := R62 :: R63 :: nil. Fixpoint destroyed_by_clobber (cl: list string): list mreg := match cl with |