From f321f75979d18ab99f226b2c5d6bbb59bffb5cac Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 19 Mar 2019 15:50:22 +0100 Subject: Pseudo instruction for 32 bits division, no code generation yet --- mppa_k1c/Asmblockgen.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'mppa_k1c/Asmblockgen.v') 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) := -- cgit