diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-19 15:50:22 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-19 15:50:22 +0100 |
| commit | f321f75979d18ab99f226b2c5d6bbb59bffb5cac (patch) | |
| tree | 54dfd0c7ce3a0569549120c786026b6b33431254 /mppa_k1c/Asmblockgen.v | |
| parent | b169a1c8b88feee186d96c107562aff847caf235 (diff) | |
| download | compcert-kvx-f321f75979d18ab99f226b2c5d6bbb59bffb5cac.tar.gz compcert-kvx-f321f75979d18ab99f226b2c5d6bbb59bffb5cac.zip | |
Pseudo instruction for 32 bits division, no code generation yet
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 4b168eec..c54394eb 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -960,7 +960,7 @@ Program Definition gen_bblocks (hd: list label) (c: list basic) (ctl: list instr | _ => {| header := hd; body := c; exit := None |} :: {| header := nil; body := nil; exit := Some (PExpand (Pbuiltin ef args res)) |} :: nil end - | Some (PCtlFlow i) => {| header := hd; body := (c ++ extract_basic ctl); exit := Some (PCtlFlow i) |} :: nil + | Some ex => {| header := hd; body := (c ++ extract_basic ctl); exit := Some ex |} :: nil end . Next Obligation. @@ -970,7 +970,7 @@ Next Obligation. Qed. Next Obligation. apply wf_bblock_refl. constructor. right. discriminate. - discriminate. + unfold builtin_alone. intros. pose (H ef args res). rewrite H0 in n. contradiction. Qed. Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool) : res (list bblock) := |