@@ -43,6 +43,10 @@ impl Alignment {
4343 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
4444 #[ inline]
4545 #[ must_use]
46+ #[ cfg_attr( not( bootstrap) , core:: contracts:: requires(
47+ mem:: align_of:: <T >( ) . is_power_of_two( ) ) ) ]
48+ #[ cfg_attr( not( bootstrap) , core:: contracts:: ensures(
49+ |result| result. as_usize( ) . is_power_of_two( ) ) ) ]
4650 pub const fn of < T > ( ) -> Self {
4751 // This can't actually panic since type alignment is always a power of two.
4852 const { Alignment :: new ( mem:: align_of :: < T > ( ) ) . unwrap ( ) }
@@ -54,6 +58,9 @@ impl Alignment {
5458 /// Note that `0` is not a power of two, nor a valid alignment.
5559 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
5660 #[ inline]
61+ #[ cfg_attr( not( bootstrap) , core:: contracts:: ensures(
62+ |result| align. is_power_of_two( ) == result. is_some( ) &&
63+ ( result. is_none( ) || result. unwrap( ) . as_usize( ) == align) ) ) ]
5764 pub const fn new ( align : usize ) -> Option < Self > {
5865 if align. is_power_of_two ( ) {
5966 // SAFETY: Just checked it only has one bit set
@@ -73,6 +80,9 @@ impl Alignment {
7380 /// It must *not* be zero.
7481 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
7582 #[ inline]
83+ #[ cfg_attr( not( bootstrap) , core:: contracts:: requires( align > 0 && ( align & ( align - 1 ) ) == 0 ) ) ]
84+ #[ cfg_attr( not( bootstrap) , core:: contracts:: ensures(
85+ |result| result. as_usize( ) == align && result. as_usize( ) . is_power_of_two( ) ) ) ]
7686 pub const unsafe fn new_unchecked ( align : usize ) -> Self {
7787 assert_unsafe_precondition ! (
7888 check_language_ub,
@@ -88,13 +98,16 @@ impl Alignment {
8898 /// Returns the alignment as a [`usize`].
8999 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
90100 #[ inline]
101+ #[ cfg_attr( not( bootstrap) , core:: contracts:: ensures( |result| result. is_power_of_two( ) ) ) ]
91102 pub const fn as_usize ( self ) -> usize {
92103 self . 0 as usize
93104 }
94105
95106 /// Returns the alignment as a <code>[NonZero]<[usize]></code>.
96107 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
97108 #[ inline]
109+ #[ cfg_attr( not( bootstrap) , core:: contracts:: ensures(
110+ |result| result. get( ) . is_power_of_two( ) && result. get( ) == self . as_usize( ) ) ) ]
98111 pub const fn as_nonzero ( self ) -> NonZero < usize > {
99112 // This transmutes directly to avoid the UbCheck in `NonZero::new_unchecked`
100113 // since there's no way for the user to trip that check anyway -- the
@@ -120,6 +133,10 @@ impl Alignment {
120133 /// ```
121134 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
122135 #[ inline]
136+ #[ cfg_attr( not( bootstrap) , core:: contracts:: requires( self . as_usize( ) . is_power_of_two( ) ) ) ]
137+ #[ cfg_attr( not( bootstrap) , core:: contracts:: ensures(
138+ |result| ( * result as usize ) < mem:: size_of:: <usize >( ) * 8 &&
139+ ( 1usize << * result) == self . as_usize( ) ) ) ]
123140 pub const fn log2 ( self ) -> u32 {
124141 self . as_nonzero ( ) . trailing_zeros ( )
125142 }
@@ -149,6 +166,10 @@ impl Alignment {
149166 /// ```
150167 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
151168 #[ inline]
169+ #[ cfg_attr( not( bootstrap) , core:: contracts:: ensures(
170+ |result| * result > 0 &&
171+ * result == !( self . as_usize( ) -1 ) &&
172+ self . as_usize( ) & * result == self . as_usize( ) ) ) ]
152173 pub const fn mask ( self ) -> usize {
153174 // SAFETY: The alignment is always nonzero, and therefore decrementing won't overflow.
154175 !( unsafe { self . as_usize ( ) . unchecked_sub ( 1 ) } )
0 commit comments