Réintroduction du Pnop, que si pas de body et d'exit. Réécriture du transl_bblocks_distrib

1 files changed, 8 insertions, 4 deletions

diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index fce2cb47..ad5bbe97 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -850,18 +850,22 @@ Local Obligation Tactic := bblock_auto_correct.
 (** Can generate two bblocks if the ctl is a PExpand (since the PExpand must be alone in its block) *)
 Program Definition gen_bblocks (hd: list label) (c: list basic) (ctl: list instruction) :=
   match (extract_ctl ctl) with
-  | None => {| header := hd; body := (c ++ (Pnop :: extract_basic ctl)); exit := None |} :: nil
+  | None => 
+      match c with
+      | nil => {| header := hd; body := Pnop::nil; exit := None |} :: nil
+      | i::c => {| header := hd; body := ((i::c) ++ extract_basic ctl); exit := None |} :: nil
+      end
 (* gen_bblock_noctl hd (c ++ (extract_basic ctl)) :: nil *)
   | Some (PExpand (Pbuiltin ef args res)) => ({| header := hd; body := c++(Pnop::nil); exit := None |}) :: 
                                             ((PExpand (Pbuiltin ef args res)) ::b nil)
-  | Some (PCtlFlow i) => {| header := hd; body := (c ++ (Pnop :: extract_basic ctl)); exit := Some (PCtlFlow i) |} :: nil
+  | Some (PCtlFlow i) => {| header := hd; body := (c ++ extract_basic ctl); exit := Some (PCtlFlow i) |} :: nil
   end
 .
 Next Obligation.
   intros. constructor. intro. apply app_eq_nil in H. destruct H. discriminate.
-Qed. Next Obligation.
+Qed. (*  Next Obligation.
   intros. constructor. intro. apply app_eq_nil in H. destruct H. discriminate.
-Qed.
+Qed. *)
 
 Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) : res (list bblock) :=
   do c <- transl_basic_code' f fb.(Machblock.body) true;