diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-01-23 16:04:00 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-01-23 16:04:00 +0100 |
| commit | afe2e1ebb808fb2e281a09b76f29c64467fbb1e1 (patch) | |
| tree | 0a68e69708105de9cb39aaf484adfbaac04e686a /mppa_k1c/Asmblockgen.v | |
| parent | 742f66c3f48e898ccd2435159a2fdb211289064a (diff) | |
| download | compcert-kvx-afe2e1ebb808fb2e281a09b76f29c64467fbb1e1.tar.gz compcert-kvx-afe2e1ebb808fb2e281a09b76f29c64467fbb1e1.zip | |
Adding a predicate that a builtin must be alone in its basicblock
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 0d1dd49c..e32748f8 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -891,9 +891,13 @@ Program Definition gen_bblocks (hd: list label) (c: list basic) (ctl: list instr end . Next Obligation. - bblock_auto_correct. intros. constructor. apply not_eq_sym. auto. + apply wf_bblock_refl. constructor. + left. auto. + discriminate. Qed. Next Obligation. - bblock_auto_correct. + apply wf_bblock_refl. constructor. + right. discriminate. + discriminate. Qed. Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool) : res (list bblock) := |