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/PostpassScheduling.v | |
| parent | ede096d051de168bd52b41e1d909e0b017899094 (diff) | |
| download | compcert-kvx-1f38df638dfd4ae2aa85467cc28f6b4fa1da03b1.tar.gz compcert-kvx-1f38df638dfd4ae2aa85467cc28f6b4fa1da03b1.zip | |
Minor refactorization
Diffstat (limited to 'mppa_k1c/PostpassScheduling.v')
| -rw-r--r-- | mppa_k1c/PostpassScheduling.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v index ef455e39..10331f15 100644 --- a/mppa_k1c/PostpassScheduling.v +++ b/mppa_k1c/PostpassScheduling.v @@ -71,6 +71,18 @@ Next Obligation. apply (H ef args res). contradict H1. auto.
Qed.
+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.
+
Lemma concat2_noexit:
forall a b bb,
concat2 a b = OK bb ->
|