diff options
Diffstat (limited to 'powerpc/Machregs.v')
| -rw-r--r-- | powerpc/Machregs.v | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index 53d99e2f..e7c8758b 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -159,11 +159,7 @@ Definition register_by_name (s: string) : option mreg := (** ** Destroyed registers, preferred registers *) -Definition destroyed_by_cond (cond: condition): list mreg := - match cond with - | Ccomplimm _ _ | Ccompluimm _ _ => R12 :: nil - | _ => nil - end. +Definition destroyed_by_cond (cond: condition): list mreg := nil. Definition destroyed_by_op (op: operation): list mreg := match op with |