diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-04-03 16:32:59 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-04-03 16:32:59 +0200 |
| commit | e0fb40f126c980819869bf2a2f32f7332b1b4a5a (patch) | |
| tree | e80686110986df274bb14e1bb167c446ff4dacab /mppa_k1c/Asmblockgenproof.v | |
| parent | 34261e53d0da905307eb3e0a0b711571365b078e (diff) | |
| download | compcert-kvx-e0fb40f126c980819869bf2a2f32f7332b1b4a5a.tar.gz compcert-kvx-e0fb40f126c980819869bf2a2f32f7332b1b4a5a.zip | |
Preuve des load/store registre registre. Reste des modifs mineures dans les preuves de Asmblockdeps
Diffstat (limited to 'mppa_k1c/Asmblockgenproof.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index 81474d30..70f188ec 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -1185,7 +1185,7 @@ Local Transparent destroyed_by_op. exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1.
intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.
exploit Mem.loadv_extends; eauto. intros [v' [C D]].
- exploit transl_load_correct; eauto. admit.
+ exploit transl_load_correct; eauto.
intros [rs2 [P [Q R]]].
eapply exec_straight_body in P.
@@ -1212,7 +1212,7 @@ Local Transparent destroyed_by_op. intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.
assert (Val.lessdef (ms src) (rs1 (preg_of src))). eapply preg_val; eauto.
exploit Mem.storev_extends; eauto. intros [m2' [C D]].
- exploit transl_store_correct; eauto. admit. intros [rs2 [P Q]].
+ exploit transl_store_correct; eauto. intros [rs2 [P Q]].
eapply exec_straight_body in P.
2: eapply code_to_basics_id; eauto.
@@ -1227,7 +1227,7 @@ Local Transparent destroyed_by_op. eapply agree_undef_regs; eauto with asmgen.
simpl; congruence.
-Admitted.
+Qed.
Lemma exec_body_trans:
forall l l' rs0 m0 rs1 m1 rs2 m2,
|