diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-10-18 17:09:17 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-10-18 17:09:17 +0200 |
| commit | d6ac402cfec2443ecb1a73a92838701236889afe (patch) | |
| tree | a1364917ae05903e1b8013142114912b0dded0e8 /mppa_k1c/Asmblockgenproof1.v | |
| parent | 7048a1fe04f45695aa6f7c4a35a6f9dcb5456c2b (diff) | |
| download | compcert-kvx-d6ac402cfec2443ecb1a73a92838701236889afe.tar.gz compcert-kvx-d6ac402cfec2443ecb1a73a92838701236889afe.zip | |
Avancement dans le cas MBgetstack du step_simu_basic
Diffstat (limited to 'mppa_k1c/Asmblockgenproof1.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 81123c9b..08be374a 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1324,18 +1324,18 @@ Proof. Qed. -(* + Lemma loadind_correct: forall (base: ireg) ofs ty dst k c (rs: regset) m v, loadind base ofs ty dst k = OK c -> Mem.loadv (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) = Some v -> base <> GPR31 -> exists rs', - exec_straight ge fn c rs m k rs' m + exec_straight ge c rs m k rs' m /\ rs'#(preg_of dst) = v /\ forall r, r <> PC -> r <> GPR31 -> r <> preg_of dst -> rs'#r = rs#r. -Proof. - intros until v; intros TR LOAD NOT31. +Proof. Admitted. +(* intros until v; intros TR LOAD NOT31. assert (A: exists mk_instr, c = indexed_memory_access mk_instr base ofs k /\ forall base' ofs' rs', @@ -1345,8 +1345,9 @@ Proof. destruct ty, (preg_of dst); inv TR; econstructor; split; eauto. } destruct A as (mk_instr & B & C). subst c. eapply indexed_load_access_correct; eauto with asmgen. -Qed. +Qed. *) +(* Lemma storeind_correct: forall (base: ireg) ofs ty src k c (rs: regset) m m', storeind src base ofs ty k = OK c -> |