diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-04-11 10:53:48 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-11 10:53:48 +0200 |
| commit | 89a54eee40305a61d1c1c0b9c5e6ba039592507b (patch) | |
| tree | 83cf2236e0cc161551cc025af531803547654270 /mppa_k1c/Asmgenproof.v | |
| parent | 8bdfa912a9ba8cee569cb40bf2ec4c584095e402 (diff) | |
| download | compcert-kvx-89a54eee40305a61d1c1c0b9c5e6ba039592507b.tar.gz compcert-kvx-89a54eee40305a61d1c1c0b9c5e6ba039592507b.zip | |
MPPA - Onegf
Diffstat (limited to 'mppa_k1c/Asmgenproof.v')
| -rw-r--r-- | mppa_k1c/Asmgenproof.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v index d8080257..4809afcb 100644 --- a/mppa_k1c/Asmgenproof.v +++ b/mppa_k1c/Asmgenproof.v @@ -405,6 +405,8 @@ Proof. - eapply transl_op_label; eauto. (* transl_load *) - destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I. +(* transl store *) +- destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I. - destruct s0; monadInv H; TailNoLabel. - destruct s0; monadInv H; eapply tail_nolabel_trans ; [eapply make_epilogue_label|TailNoLabel]. @@ -797,11 +799,11 @@ Local Transparent destroyed_by_op. left; eapply exec_straight_steps; eauto. intros. simpl in TR. inversion TR. -(*exploit transl_store_correct; eauto. intros [rs2 [P Q]]. + exploit transl_store_correct; eauto. intros [rs2 [P Q]]. exists rs2; split. eauto. split. eapply agree_undef_regs; eauto with asmgen. simpl; congruence. -*) + - (* Mcall *) assert (f0 = f) by congruence. subst f0. inv AT. |