diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2018-10-15 17:53:10 +0200 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2018-10-15 17:53:10 +0200 |
commit | 3fb302f11ccb8e7196d01ec51104060be7c01055 (patch) | |
tree | bfa6f620290bcf038d4e5454fae79cc75cdf1d3e /mppa_k1c/Asmblockgen.v | |
parent | 9ba6ffd3346136feef33d400596a3ca89f9e7260 (diff) | |
download | compcert-kvx-3fb302f11ccb8e7196d01ec51104060be7c01055.tar.gz compcert-kvx-3fb302f11ccb8e7196d01ec51104060be7c01055.zip |
Réintroduction du Pnop, que si pas de body et d'exit. Réécriture du transl_bblocks_distrib
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
-rw-r--r-- | mppa_k1c/Asmblockgen.v | 12 |
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; |