@@ -373,7 +373,6 @@ impl<T: ?Sized> NonNull<T> {
373
373
#[ rustc_const_stable( feature = "const_nonnull_as_ref" , since = "1.73.0" ) ]
374
374
#[ must_use]
375
375
#[ inline( always) ]
376
- #[ requires( ub_checks:: can_dereference( self ) == true ) ] // Ensure pointer is valid for shared reference
377
376
#[ ensures( |result: &&T | core:: ptr:: eq( * result, self . as_ptr( ) ) ) ] // Ensure returned reference matches pointer
378
377
pub const unsafe fn as_ref < ' a > ( & self ) -> & ' a T {
379
378
// SAFETY: the caller must guarantee that `self` meets all the
@@ -413,8 +412,6 @@ impl<T: ?Sized> NonNull<T> {
413
412
#[ rustc_const_unstable( feature = "const_ptr_as_ref" , issue = "91822" ) ]
414
413
#[ must_use]
415
414
#[ inline( always) ]
416
- // verify that `self` meets all the requirements for a mutable reference
417
- #[ requires( ub_checks:: can_dereference( self ) ) ]
418
415
// verify result (a mutable reference) is still associated with the same memory address as the raw pointer stored in self
419
416
#[ ensures( |result: &&mut T | core:: ptr:: eq( * result, self . as_ptr( ) ) ) ]
420
417
pub const unsafe fn as_mut < ' a > ( & mut self ) -> & ' a mut T {
@@ -1829,20 +1826,22 @@ mod verify {
1829
1826
#[ kani:: proof_for_contract( NonNull :: as_mut) ]
1830
1827
pub fn non_null_check_as_mut ( ) {
1831
1828
let mut x: i32 = kani:: any ( ) ;
1832
- let mut ptr = NonNull :: new ( x as * mut i32 ) . unwrap ( ) ;
1833
-
1834
- unsafe {
1835
- let result = ptr. as_mut ( ) ;
1829
+ if let Some ( mut ptr) = NonNull :: new ( & mut x as * mut i32 ) {
1830
+ kani:: assume ( ptr. as_ptr ( ) . align_offset ( core:: mem:: align_of :: < i32 > ( ) ) == 0 ) ;
1831
+ unsafe {
1832
+ let result = ptr. as_mut ( ) ;
1833
+ }
1836
1834
}
1837
1835
}
1838
1836
1839
1837
#[ kani:: proof_for_contract( NonNull :: as_ref) ]
1840
1838
pub fn non_null_check_as_ref ( ) {
1841
1839
let mut x: i32 = kani:: any ( ) ;
1842
- let ptr = NonNull :: new ( x as * mut i32 ) . unwrap ( ) ;
1843
-
1844
- unsafe {
1845
- let _ = ptr. as_ref ( ) ;
1840
+ if let Some ( ptr) = NonNull :: new ( & mut x as * mut i32 ) {
1841
+ kani:: assume ( ptr. as_ptr ( ) . align_offset ( core:: mem:: align_of :: < i32 > ( ) ) == 0 ) ;
1842
+ unsafe {
1843
+ let _ = ptr. as_ref ( ) ;
1844
+ }
1846
1845
}
1847
1846
}
1848
1847
0 commit comments