diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-10-31 17:08:31 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-10-31 17:08:31 +0000 |
| commit | 636e45004c6fc3530f47ae237802bec732c32b30 (patch) | |
| tree | 75c3f6abb2263fffcea3835adb873db1ebc2eb9d /backend/PPCgen.v | |
| parent | 5d742d80bf5ff7520b88160b2e435fcedf6fb15b (diff) | |
| download | compcert-636e45004c6fc3530f47ae237802bec732c32b30.tar.gz compcert-636e45004c6fc3530f47ae237802bec732c32b30.zip | |
Simplification des Cconst_symbol: seules les versions 'signed' sont conservees
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@442 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/PPCgen.v')
| -rw-r--r-- | backend/PPCgen.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/backend/PPCgen.v b/backend/PPCgen.v index d7a83b0b..171945de 100644 --- a/backend/PPCgen.v +++ b/backend/PPCgen.v @@ -265,8 +265,8 @@ Definition transl_op | Ofloatconst f, nil => Plfi (freg_of r) f :: k | Oaddrsymbol s ofs, nil => - Paddis (ireg_of r) GPR0 (Csymbol_high_unsigned s ofs) :: - Pori (ireg_of r) (ireg_of r) (Csymbol_low_unsigned s ofs) :: k + Paddis GPR2 GPR0 (Csymbol_high s ofs) :: + Paddi (ireg_of r) GPR2 (Csymbol_low s ofs) :: k | Oaddrstack n, nil => addimm (ireg_of r) GPR1 n k | Ocast8signed, a1 :: nil => @@ -385,16 +385,16 @@ Definition transl_load_store | Aindexed2, a1 :: a2 :: nil => mk2 (ireg_of a1) (ireg_of a2) :: k | Aglobal symb ofs, nil => - Paddis GPR2 GPR0 (Csymbol_high_signed symb ofs) :: - mk1 (Csymbol_low_signed symb ofs) GPR2 :: k + Paddis GPR2 GPR0 (Csymbol_high symb ofs) :: + mk1 (Csymbol_low symb ofs) GPR2 :: k | Abased symb ofs, a1 :: nil => if ireg_eq (ireg_of a1) GPR0 then Pmr GPR2 (ireg_of a1) :: - Paddis GPR2 GPR2 (Csymbol_high_signed symb ofs) :: - mk1 (Csymbol_low_signed symb ofs) GPR2 :: k + Paddis GPR2 GPR2 (Csymbol_high symb ofs) :: + mk1 (Csymbol_low symb ofs) GPR2 :: k else - Paddis GPR2 (ireg_of a1) (Csymbol_high_signed symb ofs) :: - mk1 (Csymbol_low_signed symb ofs) GPR2 :: k + Paddis GPR2 (ireg_of a1) (Csymbol_high symb ofs) :: + mk1 (Csymbol_low symb ofs) GPR2 :: k | Ainstack ofs, nil => if Int.eq (high_s ofs) Int.zero then mk1 (Cint ofs) GPR1 :: k |