diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-10-25 15:04:51 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-10-25 15:04:51 +0200 |
| commit | 38c3e762876ec66efaab289394d200d12b19af6d (patch) | |
| tree | eaf6be9363c1837991b910a20573e608bac181cd /mppa_k1c/Asmblockgen.v | |
| parent | f5435aa72f5e2c79927b2ee26f36afacd82ddfea (diff) | |
| download | compcert-kvx-38c3e762876ec66efaab289394d200d12b19af6d.tar.gz compcert-kvx-38c3e762876ec66efaab289394d200d12b19af6d.zip | |
Adding "proof irrelevance" to bblocks
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index a4c94e9b..634ba20c 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -860,7 +860,7 @@ Definition transl_basic_code' (f: Machblock.function) (il: list Machblock.basic_ otherwise the offset part of the [PC] code pointer could wrap around, leading to incorrect executions. *) -Local Obligation Tactic := bblock_auto_correct. +(* Local Obligation Tactic := bblock_auto_correct. *) (* Program Definition gen_bblock_noctl (hd: list label) (c: list basic) := match c with @@ -884,10 +884,11 @@ Program Definition gen_bblocks (hd: list label) (c: list basic) (ctl: list instr end . Next Obligation. - intros. constructor. intro. apply app_eq_nil in H. destruct H. discriminate. -Qed. (* Next Obligation. - intros. constructor. intro. apply app_eq_nil in H. destruct H. discriminate. -Qed. *) + bblock_auto_correct. intros. constructor. intro. apply app_eq_nil in H. destruct H. discriminate. +Qed. +Next Obligation. + bblock_auto_correct. +Qed. Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool) : res (list bblock) := do c <- transl_basic_code f fb.(Machblock.body) ep; |