1 files changed, 31 insertions, 2 deletions
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index ea4d1918..63f4c136 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -883,11 +883,16 @@ Proof.
   intros until x2. intros Hbuiltin TIC.
   destruct ex.
   - destruct c.
+    (* MBcall *)
     + simpl in TIC. exploreInst; simpl; eauto.
+    (* MBtailcall *)
     + simpl in TIC. exploreInst; simpl; eauto.
+    (* MBbuiltin *)
     + assert (H: Some (MBbuiltin e l b) <>  Some (MBbuiltin e l b)).
         apply Hbuiltin. contradict H; auto.
+    (* MBgoto *)
     + simpl in TIC. exploreInst; simpl; eauto.
+    (* MBcond *)
     + simpl in TIC. unfold transl_cbranch in TIC. exploreInst; simpl; eauto.
       * unfold transl_opt_compuimm. exploreInst; simpl; eauto.
       * unfold transl_opt_compluimm. exploreInst; simpl; eauto.
@@ -895,7 +900,9 @@ Proof.
       * unfold transl_comp_notfloat64. exploreInst; simpl; eauto.
       * unfold transl_comp_float32. exploreInst; simpl; eauto.
       * unfold transl_comp_notfloat32. exploreInst; simpl; eauto.
-    + simpl in TIC. inv TIC.
+    (* MBjumptable *)
+    + simpl in TIC. exploreInst; simpl; eauto.
+    (* MBreturn *)
     + simpl in TIC. monadInv TIC. simpl. eauto.
   - monadInv TIC. simpl; auto.
 Qed.
@@ -1358,7 +1365,29 @@ Proof.
         intros. discriminate.
     + (* MBjumptable *)
       destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
-      inv TBC. inv TIC.
+      inv TBC. inv TIC. inv H0.
+
+      assert (f0 = f) by congruence. subst f0.
+      monadInv H1.
+      generalize (transf_function_no_overflow _ _ TRANSF0); intro NOOV.
+      assert (f1 = f) by congruence. subst f1.
+      exploit find_label_goto_label. 4: eapply H16. 1-2: eauto. instantiate (2 := (nextblock tbb rs2) # GPR62 <- Vundef # GPR63 <- Vundef).
+        unfold nextblock. Simpl. unfold Val.offset_ptr. rewrite PCeq. reflexivity.
+      exploit functions_transl. eapply FIND0. eapply TRANSF0. intros FIND3. assert (fn = tf) by congruence. subst fn.
+
+      intros [tc' [rs' [A [B C]]]].
+      exploit ireg_val; eauto. rewrite H13. intros LD; inv LD.
+      
+      repeat eexists.
+        rewrite H6. simpl extract_basic. simpl. eauto.
+        rewrite H7. simpl extract_ctl. simpl. Simpl. rewrite <- H1. unfold Mach.label in H14. unfold label. rewrite H14. eapply A.
+      econstructor; eauto.
+        eapply agree_undef_regs; eauto. intros. rewrite C; auto with asmgen.
+        { assert (destroyed_by_jumptable = R62 :: R63 :: nil) by auto. rewrite H2 in H0. simpl in H0. inv H0.
+          destruct (preg_eq r' GPR63). subst. contradiction.
+          destruct (preg_eq r' GPR62). subst. contradiction.
+          destruct r'; Simpl. }
+        discriminate.
     + (* MBreturn *)
       destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
       inv TBC. inv TIC. inv H0.