@@ -43,6 +43,8 @@ impl Alignment {
4343 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
4444 #[ inline]
4545 #[ must_use]
46+ #[ cfg_attr( not( bootstrap) , core:: contracts:: ensures(
47+ |result: & Alignment | result. as_usize( ) . is_power_of_two( ) ) ) ]
4648 pub const fn of < T > ( ) -> Self {
4749 // This can't actually panic since type alignment is always a power of two.
4850 const { Alignment :: new ( mem:: align_of :: < T > ( ) ) . unwrap ( ) }
@@ -54,6 +56,9 @@ impl Alignment {
5456 /// Note that `0` is not a power of two, nor a valid alignment.
5557 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
5658 #[ inline]
59+ #[ cfg_attr( not( bootstrap) , core:: contracts:: ensures(
60+ |result: & Option <Alignment >| align. is_power_of_two( ) == result. is_some( ) &&
61+ ( result. is_none( ) || result. unwrap( ) . as_usize( ) == align) ) ) ]
5762 pub const fn new ( align : usize ) -> Option < Self > {
5863 if align. is_power_of_two ( ) {
5964 // SAFETY: Just checked it only has one bit set
@@ -73,6 +78,10 @@ impl Alignment {
7378 /// It must *not* be zero.
7479 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
7580 #[ inline]
81+ #[ cfg_attr( not( bootstrap) , core:: contracts:: requires( align > 0 && ( align & ( align - 1 ) ) == 0 ) ) ]
82+ #[ cfg_attr( not( bootstrap) , core:: contracts:: ensures(
83+ |result: & Alignment | result. as_usize( ) == align &&
84+ result. as_usize( ) . is_power_of_two( ) ) ) ]
7685 pub const unsafe fn new_unchecked ( align : usize ) -> Self {
7786 assert_unsafe_precondition ! (
7887 check_language_ub,
@@ -88,13 +97,18 @@ impl Alignment {
8897 /// Returns the alignment as a [`usize`].
8998 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
9099 #[ inline]
100+ #[ cfg_attr( not( bootstrap) , core:: contracts:: ensures(
101+ |result: & usize | 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: & NonZero <usize >| result. get( ) . is_power_of_two( ) &&
111+ result. get( ) == self . as_usize( ) ) ) ]
98112 pub const fn as_nonzero ( self ) -> NonZero < usize > {
99113 // This transmutes directly to avoid the UbCheck in `NonZero::new_unchecked`
100114 // since there's no way for the user to trip that check anyway -- the
@@ -120,6 +134,10 @@ impl Alignment {
120134 /// ```
121135 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
122136 #[ inline]
137+ #[ cfg_attr( not( bootstrap) , core:: contracts:: requires( self . as_usize( ) . is_power_of_two( ) ) ) ]
138+ #[ cfg_attr( not( bootstrap) , core:: contracts:: ensures(
139+ |result: & u32 | * result < usize :: BITS &&
140+ ( 1usize << * result) == self . as_usize( ) ) ) ]
123141 pub const fn log2 ( self ) -> u32 {
124142 self . as_nonzero ( ) . trailing_zeros ( )
125143 }
@@ -149,6 +167,10 @@ impl Alignment {
149167 /// ```
150168 #[ unstable( feature = "ptr_alignment_type" , issue = "102070" ) ]
151169 #[ inline]
170+ #[ cfg_attr( not( bootstrap) , core:: contracts:: ensures(
171+ |result: & usize | * result > 0 &&
172+ * result == !( self . as_usize( ) -1 ) &&
173+ self . as_usize( ) & * result == self . as_usize( ) ) ) ]
152174 pub const fn mask ( self ) -> usize {
153175 // SAFETY: The alignment is always nonzero, and therefore decrementing won't overflow.
154176 !( unsafe { self . as_usize ( ) . unchecked_sub ( 1 ) } )
0 commit comments