@@ -61,6 +61,7 @@ impl Alignment {
61
61
#[ rustc_const_unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
62
62
#[ inline]
63
63
#[ ensures( |result| align. is_power_of_two( ) == result. is_some( ) ) ]
64
+ #[ ensures( |result| result. is_none( ) || result. unwrap( ) . as_usize( ) == align) ]
64
65
pub const fn new ( align : usize ) -> Option < Self > {
65
66
if align. is_power_of_two ( ) {
66
67
// SAFETY: Just checked it only has one bit set
@@ -132,6 +133,7 @@ impl Alignment {
132
133
#[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
133
134
#[ rustc_const_unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
134
135
#[ inline]
136
+ #[ requires( self . as_usize( ) . is_power_of_two( ) ) ]
135
137
#[ ensures( |result| ( * result as usize ) < mem:: size_of:: <usize >( ) * 8 ) ]
136
138
pub const fn log2 ( self ) -> u32 {
137
139
self . as_nonzero ( ) . trailing_zeros ( )
@@ -164,6 +166,7 @@ impl Alignment {
164
166
#[ rustc_const_unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
165
167
#[ inline]
166
168
#[ ensures( |result| * result > 0 ) ]
169
+ #[ ensures( |result| * result == !( self . as_usize( ) -1 ) ) ]
167
170
pub const fn mask ( self ) -> usize {
168
171
// SAFETY: The alignment is always nonzero, and therefore decrementing won't overflow.
169
172
!( unsafe { self . as_usize ( ) . unchecked_sub ( 1 ) } )
0 commit comments