diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-10-12 16:38:46 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-10-12 16:38:46 +0200 |
| commit | e13e255b375774a632fd825d32a3146ed593d11c (patch) | |
| tree | b40522f02d9c93b06b33f99081d92ef64e75771c /kvx | |
| parent | 3a56ef38c7ec2c930312e7f574c66d4e3fd79983 (diff) | |
| download | compcert-kvx-e13e255b375774a632fd825d32a3146ed593d11c.tar.gz compcert-kvx-e13e255b375774a632fd825d32a3146ed593d11c.zip | |
remove the last tiny issue!
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/lib/RTLpathSE_impl_junk.v | 13 |
1 files changed, 3 insertions, 10 deletions
diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v index 4fb69d18..754f0c64 100644 --- a/kvx/lib/RTLpathSE_impl_junk.v +++ b/kvx/lib/RTLpathSE_impl_junk.v @@ -1631,8 +1631,7 @@ Qed. *) Definition hsistate_simu_core dm f (hse1 hse2: hsistate) := - (dm ! (hsi_pc hse2) = Some (hsi_pc hse1)) (* FIXME: issue here ? => see hsistate_simu_check below *) - /\ list_forall2 (hsiexit_simu_core dm f) (hsi_exits hse1) (hsi_exits hse2) + list_forall2 (hsiexit_simu_core dm f) (hsi_exits hse1) (hsi_exits hse2) /\ hsilocal_simu_core None (hsi_local hse1) (hsi_local hse2). Definition hsistate_simu dm f (hst1 hst2: hsistate) (ctx: simu_proof_context f): Prop := forall st1 st2, @@ -1688,10 +1687,8 @@ Theorem hsistate_simu_core_correct dm f hst1 hst2 ctx: hsistate_simu_core dm f hst1 hst2 -> hsistate_simu dm f hst1 hst2 ctx. Proof. - intros SIMUC st1 st2 HREF1 HREF2 DREF1 DREF2 is1 SEMI. - destruct HREF1 as (PCREF1 & EREF1). destruct HREF2 as (PCREF2 & EREF2). + intros (ESIMU & LSIMU) st1 st2 (PCREF1 & EREF1) (PCREF2 & EREF2) DREF1 DREF2 is1 SEMI. destruct DREF1 as (DEREF1 & LREF1 & NESTED). destruct DREF2 as (DEREF2 & LREF2 & _). - destruct SIMUC as (PCSIMU & ESIMU & LSIMU). exploit hsiexits_simu_core_correct; eauto. intro HESIMU. unfold ssem_internal in SEMI. destruct (icontinue _) eqn:ICONT. - destruct SEMI as (SSEML & PCEQ & ALLFU). @@ -2083,11 +2080,7 @@ Qed. Hint Resolve hsiexits_simu_check_correct: wlp. Global Opaque hsiexits_simu_check. -(* FIXME: we got an issue here. - the revmap check may reject any code with a sfval<>None. -*) Definition hsistate_simu_check (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsistate) := - (* revmap_check_single dm (hsi_pc hst1) (hsi_pc hst2);; *) (* FIXME: too strong ? *) hsiexits_simu_check dm f (hsi_exits hst1) (hsi_exits hst2);; hsilocal_simu_check (hsi_local hst1) (hsi_local hst2). @@ -2096,7 +2089,7 @@ Lemma hsistate_simu_check_correct dm f hst1 hst2: hsistate_simu_core dm f hst1 hst2. Proof. unfold hsistate_simu_core; wlp_simplify. -Admitted. (* FIXME *) +Qed. Hint Resolve hsistate_simu_check_correct: wlp. Global Opaque hsistate_simu_check. |