diff options
Diffstat (limited to 'backend/PPCgen.v')
| -rw-r--r-- | backend/PPCgen.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/backend/PPCgen.v b/backend/PPCgen.v index 1789fb13..f6d1fec0 100644 --- a/backend/PPCgen.v +++ b/backend/PPCgen.v @@ -362,6 +362,8 @@ Definition transl_op Pfrsp (freg_of r) (freg_of a1) :: k | Ointoffloat, a1 :: nil => Pfcti (ireg_of r) (freg_of a1) :: k + | Ointuoffloat, a1 :: nil => + Pfctiu (ireg_of r) (freg_of a1) :: k | Ofloatofint, a1 :: nil => Pictf (freg_of r) (ireg_of a1) :: k | Ofloatofintu, a1 :: nil => |