diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-04-01 13:07:02 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-04-01 13:07:02 +0200 |
| commit | 27d53418eff4e246a842a46b0883edda6860e3c2 (patch) | |
| tree | 2b285fb2d26e212f48e5dc954ac9ec6092dddab8 /mppa_k1c/Asmblockdeps.v | |
| parent | 2cbb81b2679a6d2b25bf490528060b321117294c (diff) | |
| download | compcert-kvx-27d53418eff4e246a842a46b0883edda6860e3c2.tar.gz compcert-kvx-27d53418eff4e246a842a46b0883edda6860e3c2.zip | |
cleaning Asmvliw semantics
Diffstat (limited to 'mppa_k1c/Asmblockdeps.v')
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index dd876485..6d98ab9b 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -2158,15 +2158,13 @@ Proof. constructor; auto. Qed. -Lemma bblock_para_check_correct: - forall ge fn bb rs m rs' m' o, +Lemma bblock_para_check_correct ge fn bb rs m rs' m': Ge = Genv ge fn -> exec_bblock ge fn bb rs m = Next rs' m' -> bblock_para_check bb = true -> - parexec_bblock ge fn bb rs m o -> - o = Next rs' m'. + det_parexec ge fn bb rs m rs' m'. Proof. - intros. unfold bblock_para_check in H1. + intros H H0 H1 o H2. unfold bblock_para_check in H1. exploit forward_simu; eauto. eapply trans_state_match. intros (s2' & EXEC & MS). exploit forward_simu_par_alt. 2: apply (trans_state_match (State rs m)). all: eauto. |