diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2018-10-10 15:39:41 +0200 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2018-10-10 15:39:41 +0200 |
commit | 83119fc0b190707cf5025ae2f44ac13dec68b692 (patch) | |
tree | b6c99e58cdb476b84a36efc15911a5fd13186e8d /mppa_k1c/Asmblockgen.v | |
parent | 5ef35384172fe6d3b09148959314fdc13436445b (diff) | |
download | compcert-kvx-83119fc0b190707cf5025ae2f44ac13dec68b692.tar.gz compcert-kvx-83119fc0b190707cf5025ae2f44ac13dec68b692.zip |
Preuve de MBcall et du exit=None dans le step_simu_control
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
-rw-r--r-- | mppa_k1c/Asmblockgen.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 2e13d34b..28941e22 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -850,11 +850,11 @@ 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 := Pnop::c; exit := None |} :: nil + | None => {| header := hd; body := Pnop::(c ++ (extract_basic ctl)); exit := None |} :: nil (* gen_bblock_noctl hd (c ++ (extract_basic ctl)) :: nil *) | Some (PExpand (Pbuiltin ef args res)) => ({| header := hd; body := Pnop::c; exit := None |}) :: ((PExpand (Pbuiltin ef args res)) ::b nil) - | Some (PCtlFlow i) => {| header := hd; body := c ++ (extract_basic ctl); exit := Some (PCtlFlow i) |} :: nil + | Some (PCtlFlow i) => {| header := hd; body := Pnop :: (c ++ (extract_basic ctl)); exit := Some (PCtlFlow i) |} :: nil end . |