diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2018-03-23 15:58:21 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-04 16:30:09 +0200 |
commit | 8d196f0f3193758a6371d9eb539af350202e0f4f (patch) | |
tree | 3a434028437588a39c0b6220b85e4732f112dbfc /mppa_k1c/Asmgenproof.v | |
parent | c81c303db03ba732bda8612381e8569db181a541 (diff) | |
download | compcert-kvx-8d196f0f3193758a6371d9eb539af350202e0f4f.tar.gz compcert-kvx-8d196f0f3193758a6371d9eb539af350202e0f4f.zip |
MPPA - Added Mgoto + Pj_l
Diffstat (limited to 'mppa_k1c/Asmgenproof.v')
-rw-r--r-- | mppa_k1c/Asmgenproof.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v index 88e42d1e..068a2731 100644 --- a/mppa_k1c/Asmgenproof.v +++ b/mppa_k1c/Asmgenproof.v @@ -884,7 +884,6 @@ Local Transparent destroyed_by_op. - (* Mgoto *) assert (f0 = f) by congruence. subst f0. inv AT. monadInv H4. -(* exploit find_label_goto_label; eauto. intros [tc' [rs' [GOTO [AT2 INV]]]]. left; exists (State rs' m'); split. apply plus_one. econstructor; eauto. @@ -894,7 +893,6 @@ Local Transparent destroyed_by_op. econstructor; eauto. eapply agree_exten; eauto with asmgen. congruence. -*) - (* Mcond true *) assert (f0 = f) by congruence. subst f0. exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. |