Skip to content

Commit

Permalink
Update non_null.rs
Browse files Browse the repository at this point in the history
  • Loading branch information
Dhvani-Kapadia authored Nov 16, 2024
1 parent 065eb9f commit 5f0538c
Showing 1 changed file with 7 additions and 7 deletions.
14 changes: 7 additions & 7 deletions library/core/src/ptr/non_null.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1818,7 +1818,7 @@ mod verify {
let non_null_ptr: *mut i32 = kani::any::<usize>() as *mut i32;
if let Some(ptr) = NonNull::new(non_null_ptr){
// Call as_ptr
let raw_ptr = ptr.as_ptr();}
let raw_ptr = ptr.as_ptr();}

}
#[kani::proof_for_contract(NonNull::<[T]>::as_mut_ptr)]
Expand All @@ -1829,17 +1829,17 @@ mod verify {
let mut values: [i32; ARR_LEN] = [0; ARR_LEN];
let raw_ptr: *mut i32 = generator.any_in_bounds().ptr;
if let Some(ptr) = NonNull::new(raw_ptr){
let slice_ptr = NonNull::slice_from_raw_parts(ptr, values.len());
// Call as_mut_ptr
let raw_ptr = slice_ptr.as_mut_ptr();
let slice_ptr = NonNull::slice_from_raw_parts(ptr, values.len());
// Call as_mut_ptr
let raw_ptr = slice_ptr.as_mut_ptr();
}}
#[kani::proof_for_contract(NonNull::<T>::cast)]
pub fn non_null_check_cast() {
// Create a non-null pointer to a random value
let non_null_ptr: *mut i32 = kani::any::<usize>() as *mut i32;
if let Some(ptr) = NonNull::new(non_null_ptr){
// Perform the cast
let casted_ptr: NonNull<u8> = ptr.cast();
let casted_ptr: NonNull<u8> = ptr.cast();
}}
#[kani::proof_for_contract(NonNull::<[T]>::as_non_null_ptr)]
pub fn non_null_check_as_non_null_ptr() {
Expand All @@ -1848,8 +1848,8 @@ mod verify {
let mut values: [i32; ARR_LEN] = [0; ARR_LEN];
let raw_ptr: *mut i32 = generator.any_in_bounds().ptr;
if let Some(ptr) = NonNull::new(raw_ptr){
let slice_ptr = NonNull::slice_from_raw_parts(ptr, values.len());
let result = slice_ptr.as_non_null_ptr();
let slice_ptr = NonNull::slice_from_raw_parts(ptr, values.len());
let result = slice_ptr.as_non_null_ptr();
}}

}
Expand Down

0 comments on commit 5f0538c

Please sign in to comment.