diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v
index 6013a17df67247c1c9ccb8716af5126049131f09..10058907b99e929609ae2604a588e6ca25f18f97 100644
--- a/backend/LTLintyping.v
+++ b/backend/LTLintyping.v
@@ -15,6 +15,7 @@
 Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
+Require Import Integers.
 Require Import Op.
 Require Import RTL.
 Require Import Locations.
@@ -80,6 +81,7 @@ Inductive wt_instr : instruction -> Prop :=
       forall arg tbl,
       Loc.type arg = Tint ->
       loc_acceptable arg ->
+      list_length_z tbl * 4 <= Int.max_signed ->
       wt_instr (Ljumptable arg tbl)
   | wt_Lreturn: 
       forall optres,
diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v
index e62f9287fa129c085bb55ff92998cf82ce36ad5f..9a2322c7803b8734fd026718cc02ff3aca8793bc 100644
--- a/backend/LTLtyping.v
+++ b/backend/LTLtyping.v
@@ -15,6 +15,7 @@
 Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
+Require Import Integers.
 Require Import Op.
 Require Import RTL.
 Require Import Locations.
@@ -99,6 +100,7 @@ Inductive wt_instr : instruction -> Prop :=
       Loc.type arg = Tint ->
       loc_acceptable arg ->
       (forall lbl, In lbl tbl -> valid_successor lbl) ->
+      list_length_z tbl * 4 <= Int.max_signed ->
       wt_instr (Ljumptable arg tbl)
   | wt_Lreturn: 
       forall optres,
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index ba4952bd5a41be59bb384fc9b495a182be5c2768..1fe77378f44ee33b974196a8a209f0c35cce1992 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -15,6 +15,7 @@
 Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
+Require Import Integers.
 Require Import Op.
 Require Import RTL.
 Require Import Locations.
@@ -98,6 +99,7 @@ Inductive wt_instr : instruction -> Prop :=
   | wt_Ljumptable:
       forall arg tbl,
       mreg_type arg = Tint ->
+      list_length_z tbl * 4 <= Int.max_signed ->
       wt_instr (Ljumptable arg tbl)
   | wt_Lreturn: 
       wt_instr (Lreturn).
diff --git a/backend/Machtyping.v b/backend/Machtyping.v
index fe086cb4f3e7aae61663b95a303ec11dfe4a6353..8b40001abbc279ba7edfff14b27f16c568722e8d 100644
--- a/backend/Machtyping.v
+++ b/backend/Machtyping.v
@@ -82,6 +82,7 @@ Inductive wt_instr : instruction -> Prop :=
   | wt_Mjumptable:
       forall arg tbl,
       mreg_type arg = Tint ->
+      list_length_z tbl * 4 <= Int.max_signed ->
       wt_instr (Mjumptable arg tbl)
   | wt_Mreturn: 
       wt_instr Mreturn.
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 86f0eaf10925533e01ec4d634dc0d8598d6bca64..d8e2f212347c9c2a42d9179893314197da746438 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -116,6 +116,7 @@ Inductive wt_instr : instruction -> Prop :=
       forall arg tbl,
       env arg = Tint ->
       (forall s, In s tbl -> valid_successor s) ->
+      list_length_z tbl * 4 <= Int.max_signed ->
       wt_instr (Ijumptable arg tbl)
   | wt_Ireturn: 
       forall optres,
@@ -232,6 +233,7 @@ Definition check_instr (i: instruction) : bool :=
   | Ijumptable arg tbl =>
       check_reg arg Tint
       && List.forallb check_successor tbl
+      && zle (list_length_z tbl * 4) Int.max_signed
   | Ireturn optres =>
       match optres, funct.(fn_sig).(sig_res) with
       | None, None => true
@@ -336,8 +338,8 @@ Proof.
   apply check_successor_correct; auto.
   (* jumptable *)
   constructor. apply check_reg_correct; auto.
-  rewrite List.forallb_forall in H0. intros. apply check_successor_correct; auto.
-  intros. 
+  rewrite List.forallb_forall in H1. intros. apply check_successor_correct; auto.
+  eapply proj_sumbool_true. eauto.  
   (* return *)
   constructor. 
   destruct o; simpl; destruct funct.(fn_sig).(sig_res); try discriminate.
diff --git a/backend/Tunnelingtyping.v b/backend/Tunnelingtyping.v
index 8990cb44a3b35cbc15d4e14b277384a30f585119..834e8e18a64595813b5dfd17da817804454e3f45 100644
--- a/backend/Tunnelingtyping.v
+++ b/backend/Tunnelingtyping.v
@@ -76,7 +76,8 @@ Proof.
   intros; inv H0; simpl; econstructor; eauto;
   try (eapply branch_target_valid; eauto).
   intros. exploit list_in_map_inv; eauto. intros [x [A B]]. subst lbl.
-  eapply branch_target_valid; eauto. 
+  eapply branch_target_valid; eauto.
+  rewrite list_length_z_map. auto.
 Qed.
 
 Lemma wt_tunnel_function:
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 7bc4f8bf5f5306aa6ef9b73f00d3370261c3ad5f..02fa7babb92f9977f77a709a7d911818595cd4dc 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -648,6 +648,13 @@ Proof.
   rewrite list_length_z_cons. omega.
 Qed.
 
+Lemma list_length_z_map:
+  forall (A B: Type) (f: A -> B) (l: list A),
+  list_length_z (map f l) = list_length_z l.
+Proof.
+  induction l. reflexivity. simpl. repeat rewrite list_length_z_cons. congruence.
+Qed. 
+
 (** Extract the n-th element of a list, as [List.nth_error] does,
     but the index [n] is of type [Z]. *)
 
diff --git a/lib/Integers.v b/lib/Integers.v
index c54b6fe5dc8a3f92f15e47ac88e9977d17f001c2..625973a0600b6f1ab26872f474a9378aca8475a4 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -871,6 +871,13 @@ Proof.
   apply neg_mul_distr_l. 
 Qed.
 
+Theorem mul_signed:
+  forall x y, mul x y = repr (signed x * signed y).
+Proof.
+  intros; unfold mul. apply eqm_samerepr.
+  apply eqm_mult; apply eqm_sym; apply eqm_signed_unsigned.
+Qed.
+
 (** ** Properties of binary decompositions *)
 
 Lemma Z_shift_add_bin_decomp:
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 18dc93aba87b41b112919108f45f255b62513e3a..1582b414614d1b188ccb7e8bc81ab55229aacea0 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -298,8 +298,7 @@ lbl:    .long   0x43300000, 0x00000000
 - [Pbtbl reg table]: this is a N-way branch, implemented via a jump table
   as follows:
 <<
-        rlwinm  r12, reg, 2, 0, 29
-        addis   r12, r12, ha16(lbl)
+        addis   r12, reg, ha16(lbl)
         lwz     r12, lo16(lbl)(r12)
         mtctr   r12
         bctr    r12
@@ -307,6 +306,7 @@ lbl:    .long   0x43300000, 0x00000000
 lbl:    .long   table[0], table[1], ...
         .text
 >>
+  Note that [reg] contains 4 times the index of the desired table entry.
 *)
 
 Definition code := list instruction.
@@ -624,10 +624,13 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
   | Pbtbl r tbl =>
       match rs#r with
       | Vint n => 
-          match list_nth_z tbl (Int.signed n) with
-          | None => Error
-          | Some lbl => goto_label c lbl (rs #GPR12 <- Vundef #CTR <- Vundef) m
-          end
+          let pos := Int.signed n in
+          if zeq (Zmod pos 4) 0 then
+            match list_nth_z tbl (pos / 4) with
+            | None => Error
+            | Some lbl => goto_label c lbl (rs #GPR12 <- Vundef #CTR <- Vundef) m
+            end
+          else Error
       | _ => Error
       end
   | Pcmplw r1 r2 =>
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 4beabb1c8d75d4b3eee3783b3af8412785718915..2c65ca4defe87feeaaaaa0b8354afdc4742b87ad 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 ::
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 4e45c8eae9cf59cbb649fc41d3ce08c03bacf699..a2fc6108efc125f9d83508254d2187d3628ef759 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -1146,21 +1146,47 @@ Proof.
   assert (f0 = f) by congruence. subst f0.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
   intro WTI. inv WTI.
-  pose (rs1 := rs0 # GPR12 <- Vundef # CTR <- Vundef).
-  inv AT. simpl in H6.
-  assert (rs1 PC = Vptr fb ofs). rewrite H3. reflexivity.
-  generalize (functions_transl _ _ H1); intro FN.
-  generalize (functions_transl_no_overflow _ _ H1); intro NOOV.
-  exploit find_label_goto_label; eauto. intros [rs2 [A [B C]]].
-  left; exists (State rs2 m); split.
-  apply plus_one. econstructor. symmetry; eauto. eauto.
-  eapply find_instr_tail. eauto. 
-  simpl. rewrite (ireg_val _ _ _ _ AG H4) in H. rewrite H. 
-  change label with Mach.label; rewrite H0. eexact A. 
+  exploit list_nth_z_range; eauto. intro RANGE.
+  assert (SHIFT: Int.signed (Int.rolm n (Int.repr 2) (Int.repr (-4))) = Int.signed n * 4).
+    replace (Int.repr (-4)) with (Int.shl Int.mone (Int.repr 2)).
+    rewrite <- Int.shl_rolm. rewrite Int.shl_mul.
+    rewrite Int.mul_signed.
+    apply Int.signed_repr.
+    split. apply Zle_trans with 0. vm_compute; congruence. omega. 
+    omega.
+    vm_compute. reflexivity.
+    vm_compute. apply Int.mkint_eq. auto.
+  inv AT. simpl in H7. 
+  set (k1 := Pbtbl GPR12 tbl :: transl_code f c).
+  set (rs1 := nextinstr (rs0 # GPR12 <- (Vint (Int.rolm n (Int.repr 2) (Int.repr (-4)))))).
+  generalize (functions_transl _ _ H4); intro FN.
+  generalize (functions_transl_no_overflow _ _ H4); intro NOOV.
+  assert (exec_straight tge (transl_function f)
+            (Prlwinm GPR12 (ireg_of arg) (Int.repr 2) (Int.repr (-4)) :: k1) rs0 m
+            k1 rs1 m).
+   apply exec_straight_one. 
+   simpl. rewrite <- (ireg_val _ _ _ _ AG H5). rewrite H. reflexivity. reflexivity. 
+  exploit exec_straight_steps_2; eauto. 
+  intros [ofs' [PC1 CT1]].
+  set (rs2 := rs1 # GPR12 <- Vundef # CTR <- Vundef).
+  assert (PC2: rs2 PC = Vptr fb ofs'). rewrite <- PC1. reflexivity.
+  generalize (find_label_goto_label f lbl rs2 m _ _ _ FIND PC2 H2).
+  intros [rs3 [GOTO [AT3 INV3]]].
+  left; exists (State rs3 m); split.
+  eapply plus_right'. 
+  eapply exec_straight_steps_1; eauto.
+  econstructor; eauto. 
+  eapply find_instr_tail. unfold k1 in CT1. eauto.
+  unfold exec_instr.
+  change (rs1 GPR12) with (Vint (Int.rolm n (Int.repr 2) (Int.repr (-4)))).
+Opaque Zmod.  Opaque Zdiv.
+  simpl. rewrite SHIFT. rewrite Z_mod_mult. rewrite zeq_true. 
+  rewrite Z_div_mult. 
+  change label with Mach.label; rewrite H0. exact GOTO. omega. traceEq.
   econstructor; eauto. 
   eapply Mach.find_label_incl; eauto.
-  apply agree_exten_2 with rs1; auto.
-  unfold rs1. repeat apply agree_set_other; auto with ppcgen.
+  apply agree_exten_2 with rs2; auto. 
+  unfold rs2, rs1. repeat apply agree_set_other; auto with ppcgen.
 Qed.
 
 Lemma exec_Mreturn_prop:
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index df1b062935e50a8aea3536c3861017221e909e64..d9c6531472afa601a92f50bb5bd7e9856dcd03c3 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -263,8 +263,7 @@ let print_instruction oc labels = function
       fprintf oc "	bt	%a, %a\n" crbit bit label (transl_label lbl)
   | Pbtbl(r, tbl) ->
       let lbl = new_label() in
-      fprintf oc "	rlwinm	%a, %a, 2, 0, 29\n" ireg GPR12 ireg r;
-      fprintf oc "	addis	%a, %a, %a\n" ireg GPR12 ireg GPR12 label_high lbl;
+      fprintf oc "	addis	%a, %a, %a\n" ireg GPR12 ireg r label_high lbl;
       fprintf oc "	lwz	%a, %a(%a)\n" ireg GPR12 label_low lbl ireg GPR12;
       fprintf oc "	mtctr	%a\n" ireg GPR12;
       fprintf oc "	bctr\n";