diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-10-24 17:33:04 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-10-24 17:33:04 +0200 |
| commit | f5435aa72f5e2c79927b2ee26f36afacd82ddfea (patch) | |
| tree | 00d10653e3d02a8c3cf8c51a3d54b4424173df85 /mppa_k1c/Asmblockgenproof1.v | |
| parent | ba4b3ba3ebf01c202cdd847796eccd00f20f63b0 (diff) | |
| download | compcert-kvx-f5435aa72f5e2c79927b2ee26f36afacd82ddfea.tar.gz compcert-kvx-f5435aa72f5e2c79927b2ee26f36afacd82ddfea.zip | |
MBgetparam done!
Diffstat (limited to 'mppa_k1c/Asmblockgenproof1.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 4abf1d52..74b8f8b5 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1394,22 +1394,20 @@ Proof. intros. rewrite H. Simpl. Qed. +*) + Lemma loadind_ptr_correct: forall (base: ireg) ofs (dst: ireg) k (rs: regset) m v, Mem.loadv Mptr m (Val.offset_ptr rs#base ofs) = Some v -> base <> GPR31 -> exists rs', - exec_straight ge fn (loadind_ptr base ofs dst k) rs m k rs' m + exec_straight ge (loadind_ptr base ofs dst :: k) rs m k rs' m /\ rs'#dst = v /\ forall r, r <> PC -> r <> GPR31 -> r <> dst -> rs'#r = rs#r. Proof. intros. eapply indexed_load_access_correct; eauto with asmgen. intros. unfold Mptr. assert (Archi.ptr64 = true). auto. rewrite H1. auto. Qed. -*) - - -Definition nosroll := 0. Lemma storeind_ptr_correct: forall (base: ireg) ofs (src: ireg) k (rs: regset) m m', |