diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-06-16 18:55:17 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-08-07 10:40:26 +0200 |
| commit | eb85803875c5a4e90be60d870f01fac380ca18b0 (patch) | |
| tree | 5fb9ac38ace0b8c6caec6b5438610258b321185c | |
| parent | b839084a1731b09542eedff0cfac8e1a7b072c69 (diff) | |
| download | compcert-eb85803875c5a4e90be60d870f01fac380ca18b0.tar.gz compcert-eb85803875c5a4e90be60d870f01fac380ca18b0.zip | |
Relax lemma Val.zero_ext_and and add Val.zero_ext_andl
| -rw-r--r-- | common/Values.v | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/common/Values.v b/common/Values.v index 52474f99..de317734 100644 --- a/common/Values.v +++ b/common/Values.v @@ -1910,10 +1910,18 @@ Qed. Lemma zero_ext_and: forall n v, - 0 < n < Int.zwordsize -> + 0 <= n -> Val.zero_ext n v = Val.and v (Vint (Int.repr (two_p n - 1))). Proof. - intros. destruct v; simpl; auto. decEq. apply Int.zero_ext_and; auto. omega. + intros. destruct v; simpl; auto. decEq. apply Int.zero_ext_and; auto. +Qed. + +Lemma zero_ext_andl: + forall n v, + 0 <= n -> + Val.zero_ext_l n v = Val.andl v (Vlong (Int64.repr (two_p n - 1))). +Proof. + intros. destruct v; simpl; auto. decEq. apply Int64.zero_ext_and; auto. Qed. Lemma rolm_lt_zero: |