diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-11-14 16:04:03 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-11-14 16:04:03 +0100 |
| commit | 4c471a5a7852d02c368101205b34418c0f754b91 (patch) | |
| tree | eaa336fa65571e440f183c745d7bc40b591050fe /mppa_k1c/Asmblockdeps.v | |
| parent | 8d1b23070baa3c2db69a066dfc097e08bb811eb3 (diff) | |
| download | compcert-kvx-4c471a5a7852d02c368101205b34418c0f754b91.tar.gz compcert-kvx-4c471a5a7852d02c368101205b34418c0f754b91.zip | |
fixing a potential inconsistency from unsafe_coerce
Now, unsafe_coerce axioms are clearly consistent (for any interpretation of may-return monads).
But, the extraction is still unsafe...
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 c4c1bbf1..8bc1112f 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1636,11 +1636,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. |