diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-11-10 14:58:33 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-11-10 14:58:33 +0000 |
| commit | 8ccc7f2f597aff2c8590c4e62552fb53406ad0f8 (patch) | |
| tree | a553844ce1b6960ae5240f65593c085be733e3b2 /powerpc/Asmgen.v | |
| parent | 74487f079dd56663f97f9731cea328931857495c (diff) | |
More realistic treatment of jump tables: show the absence of overflow when accessing the table
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1172 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc/Asmgen.v')
| -rw-r--r-- | powerpc/Asmgen.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 4beabb1..2c65ca4 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -503,7 +503,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := transl_cond cond args (if (snd p) then Pbt (fst p) lbl :: k else Pbf (fst p) lbl :: k) | Mjumptable arg tbl => - Pbtbl (ireg_of arg) tbl :: k + Prlwinm GPR12 (ireg_of arg) (Int.repr 2) (Int.repr (-4)) :: + Pbtbl GPR12 tbl :: k | Mreturn => Plwz GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 :: Pmtlr GPR12 :: |