diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-08-27 18:58:38 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-08-27 18:58:38 +0200 |
| commit | ca64d933691ee3cb9f0992b73c75eccea0808193 (patch) | |
| tree | 1d255d6e4c1d43818c397be998e1e3dd8cd0750f /kvx/lib | |
| parent | 1b196baa866aceb569df4f9f6803c7d3ea18f3d9 (diff) | |
| download | compcert-kvx-ca64d933691ee3cb9f0992b73c75eccea0808193.tar.gz compcert-kvx-ca64d933691ee3cb9f0992b73c75eccea0808193.zip | |
more realistic ok_allexit.
Diffstat (limited to 'kvx/lib')
| -rw-r--r-- | kvx/lib/RTLpathSE_impl.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/kvx/lib/RTLpathSE_impl.v b/kvx/lib/RTLpathSE_impl.v index 96854123..a99765aa 100644 --- a/kvx/lib/RTLpathSE_impl.v +++ b/kvx/lib/RTLpathSE_impl.v @@ -416,9 +416,9 @@ Proof. Qed. -Lemma ok_allexit ge sp st rs m is1: - ssem_internal ge sp st rs m is1 -> - forall se, In se (si_exits st) -> sok_local ge sp rs m (si_elocal se). +Lemma ok_allexit ge sp hst st rs m: + hsiexits_refines_dyn ge sp rs m hst st -> + forall se, In se st -> sok_local ge sp rs m (si_elocal se). Admitted. (* TODO !! *) @@ -427,10 +427,10 @@ Theorem hsistate_simu_core_correct dm f hst1 hst2 ctx: hsistate_simu dm f hst1 hst2 ctx. Proof. intros SIMUC st1 st2 HREF1 HREF2 DREF1 DREF2 is1 SEMI. - generalize (ok_allexit _ _ _ _ _ _ SEMI). - intros EXOK. destruct HREF1 as (PCREF1 & EREF1). destruct HREF2 as (PCREF2 & EREF2). destruct DREF1 as (DEREF1 & LREF1). destruct DREF2 as (DEREF2 & LREF2). + generalize (ok_allexit _ _ _ _ _ _ DEREF1). + intros EXOK. destruct SIMUC as (PCSIMU & ESIMU & LSIMU). exploit hsiexits_simu_core_correct; eauto. intro HESIMU. unfold ssem_internal in SEMI. destruct (icontinue _) eqn:ICONT. |