diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2019-02-12 11:57:16 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2019-02-12 11:57:16 +0100 |
commit | 1f38df638dfd4ae2aa85467cc28f6b4fa1da03b1 (patch) | |
tree | 16ab41df7bc06808ccdf83c867b3a844da61d179 /mppa_k1c/PostpassSchedulingproof.v | |
parent | ede096d051de168bd52b41e1d909e0b017899094 (diff) | |
download | compcert-kvx-1f38df638dfd4ae2aa85467cc28f6b4fa1da03b1.tar.gz compcert-kvx-1f38df638dfd4ae2aa85467cc28f6b4fa1da03b1.zip |
Minor refactorization
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
-rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 19d30354..d0aa89a4 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -36,18 +36,6 @@ Inductive bblock_equiv (ge: Genv.t fundef unit) (f: function) (bb bb': bblock) : exec_bblock ge f bb rs m = exec_bblock ge f bb' rs m) ->
bblock_equiv ge f bb bb'.
-Lemma concat2_zlt_size:
- forall a b bb,
- concat2 a b = OK bb ->
- size a <= Ptrofs.max_unsigned
- /\ size b <= Ptrofs.max_unsigned.
-Proof.
- intros. monadInv H.
- split.
- - unfold check_size in EQ. destruct (zlt Ptrofs.max_unsigned (size a)); monadInv EQ. omega.
- - unfold check_size in EQ1. destruct (zlt Ptrofs.max_unsigned (size b)); monadInv EQ1. omega.
-Qed.
-
(* Axioms that verified_schedule must verify *)
Axiom verified_schedule_correct:
forall ge f bb lbb,
|