diff options
Diffstat (limited to 'common/Values.v')
| -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: |