diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-05 11:51:49 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-05 11:51:49 +0100 |
| commit | 264637042f4e648888307af28392aea21e2f28b8 (patch) | |
| tree | 83ab317e47f2f390d336809f1c06b5f1e83f9ddc /mppa_k1c/Asmblockdeps.v | |
| parent | 50092ae8d8937cb5771c890dd608ac961ce32440 (diff) | |
| download | compcert-kvx-264637042f4e648888307af28392aea21e2f28b8.tar.gz compcert-kvx-264637042f4e648888307af28392aea21e2f28b8.zip | |
No more axioms remaining (scheduling completely proven), however error at extraction
Diffstat (limited to 'mppa_k1c/Asmblockdeps.v')
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 24 |
1 files changed, 3 insertions, 21 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 4912a96f..63ccdeac 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1375,27 +1375,8 @@ Theorem bblock_eq_test_correct verb p1 p2 : Proof. wlp_simplify. Qed. -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) -> - bblock_equiv' bb bb'. - -Lemma bblock_equiv'_refl: forall tbb, bblock_equiv' tbb tbb. -Proof. - repeat constructor. -Qed. - -Axiom bblock_equivb: L.bblock -> L.bblock -> bool. - -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. @@ -1410,7 +1391,8 @@ Proof. apply unsafe_coerce_not_really_correct; eauto. Qed. +Definition bblock_equivb: Asmblock.bblock -> Asmblock.bblock -> bool := pure_bblock_eq_test true. -End SECT. +Definition bblock_equiv_eq := pure_bblock_eq_test_correct true. -Extract Constant bblock_equivb => "PostpassSchedulingOracle.bblock_equivb'". +End SECT. |