diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-02 09:22:37 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-02 09:22:37 +0100 |
| commit | 55d62972391310a71e7bc0eff362fc339455b23b (patch) | |
| tree | 84dfc04b6b25c92ad6e0090310d34db14a37966c /mppa_k1c/Asmblockdeps.v | |
| parent | 59948b3348964f4b16f408ffe690f2c78ca80959 (diff) | |
| download | compcert-kvx-55d62972391310a71e7bc0eff362fc339455b23b.tar.gz compcert-kvx-55d62972391310a71e7bc0eff362fc339455b23b.zip | |
(Unsafe) coercion of ??bool into bool
Diffstat (limited to 'mppa_k1c/Asmblockdeps.v')
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index c2477e66..80383c2f 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1313,6 +1313,7 @@ Admitted. (* FIXME - à voir avec Sylvain *) Global Opaque bblock_eq_test. Hint Resolve bblock_eq_test_correct: wlp. + Inductive bblock_equiv' (bb bb': L.bblock) := | bblock_equiv_intro': (forall s, exec Ge bb s = exec Ge bb' s) -> @@ -1329,6 +1330,22 @@ Axiom bblock_equiv'_eq: forall b1 b2, bblock_equivb b1 b2 = true <-> bblock_equiv' b1 b2. (* FIXME - à voir avec Sylvain *) + +(* Coerce bblock_eq_test into a pure function (this is a little unsafe like all oracles in CompCert). *) + +Import UnsafeImpure. + +Definition pure_bblock_eq_test (verb: bool) (p1 p2: Asmblock.bblock): bool := unsafe_coerce (bblock_eq_test verb p1 p2). + +Theorem pure_bblock_eq_test_correct verb p1 p2: + forall ge fn, Ge = Genv ge fn -> + pure_bblock_eq_test verb p1 p2 = true -> Asmblockgenproof0.bblock_equiv ge fn p1 p2. +Proof. + intros; unfold pure_bblock_eq_test. intros; eapply bblock_eq_test_correct; eauto. + apply unsafe_coerce_not_really_correct; eauto. +Qed. + + End SECT. Extract Constant bblock_equivb => "PostpassSchedulingOracle.bblock_equivb'". |