diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-12-02 19:49:30 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-12-02 19:49:30 +0100 |
| commit | f0c1cc8327ecf2b1e3021bce66f2d6bb0265f6c0 (patch) | |
| tree | 6d5c6988ad68cfe7052dc6dac267c4de53f0202b /mppa_k1c/Asmblockdeps.v | |
| parent | be3d241a0c2247f48dab2988f49e9c651417328b (diff) | |
| parent | eaea751c200213e0f86cf51c1fe93b7ba09c4227 (diff) | |
| download | compcert-kvx-f0c1cc8327ecf2b1e3021bce66f2d6bb0265f6c0.tar.gz compcert-kvx-f0c1cc8327ecf2b1e3021bce66f2d6bb0265f6c0.zip | |
Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-load
Diffstat (limited to 'mppa_k1c/Asmblockdeps.v')
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 65792d13..c7cfe43c 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1665,11 +1665,17 @@ Hint Resolve bblock_simu_test_correct: wlp. Import UnsafeImpure. -Definition pure_bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock): bool := unsafe_coerce (bblock_simu_test verb p1 p2). +Definition pure_bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock): bool := + match unsafe_coerce (bblock_simu_test verb p1 p2) with + | Some b => b + | None => false + end. Theorem pure_bblock_simu_test_correct verb p1 p2 ge fn: pure_bblock_simu_test verb p1 p2 = true -> Asmblockgenproof0.bblock_simu ge fn p1 p2. Proof. - intros; unfold pure_bblock_simu_test. intros; eapply bblock_simu_test_correct; eauto. + unfold pure_bblock_simu_test. + destruct (unsafe_coerce (bblock_simu_test verb p1 p2)) eqn: UNSAFE; try discriminate. + intros; subst. eapply bblock_simu_test_correct; eauto. apply unsafe_coerce_not_really_correct; eauto. Qed. |