From 16ecdb98088f2d12979fe257b187c391887c5814 Mon Sep 17 00:00:00 2001 From: Dhvani-Kapadia <159494547+Dhvani-Kapadia@users.noreply.github.com> Date: Sat, 2 Nov 2024 12:23:21 -0700 Subject: [PATCH 01/14] adding contracts for 4 memory operations --- library/core/src/ptr/non_null.rs | 141 ++++++++++++++++++++++++++++++- 1 file changed, 138 insertions(+), 3 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 4d6e484915dbf..57ee0ae1b846e 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -9,7 +9,7 @@ use crate::slice::{self, SliceIndex}; use crate::ub_checks::assert_unsafe_precondition; use crate::{fmt, hash, intrinsics, ptr}; use safety::{ensures, requires}; - +use crate::{ub_checks}; #[cfg(kani)] use crate::kani; @@ -934,6 +934,12 @@ impl NonNull { #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_unstable(feature = "const_intrinsic_copy", issue = "80697")] + #[kani::requires(count * core::mem::size_of::() <= isize::MAX as usize)] + #[requires(ub_checks::can_dereference(self.as_ptr()))] //The pointer is valid + #[requires(ub_checks::can_dereference(dest.as_ptr()))] + #[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr() as *const T))] + #[ensures(|result: &()| ub_checks::can_dereference(dest.as_ptr() as *const T))] + #[kani::modifies(dest.as_ptr())] pub const unsafe fn copy_to(self, dest: NonNull, count: usize) where T: Sized, @@ -954,6 +960,14 @@ impl NonNull { #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_unstable(feature = "const_intrinsic_copy", issue = "80697")] + #[kani::requires(count * core::mem::size_of::() <= isize::MAX as usize)] + #[requires(ub_checks::can_dereference(self.as_ptr()))] + #[requires(ub_checks::can_dereference(dest.as_ptr()))] + #[requires((self.as_ptr() as usize).abs_diff(dest.as_ptr() as usize) >= count * core::mem::size_of::())] + #[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr()))] + #[ensures(|result: &()| ub_checks::can_dereference(dest.as_ptr()))] + #[kani::modifies(dest.as_ptr())] + #[kani::modifies(self.as_ptr())] pub const unsafe fn copy_to_nonoverlapping(self, dest: NonNull, count: usize) where T: Sized, @@ -974,6 +988,13 @@ impl NonNull { #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_unstable(feature = "const_intrinsic_copy", issue = "80697")] + #[kani::requires(count * core::mem::size_of::() <= isize::MAX as usize)] + #[requires(ub_checks::can_dereference(src.as_ptr()) )]//The pointer is valid + #[requires( ub_checks::can_dereference(self.as_ptr()))]//The pointer is valid + #[requires((src.as_ptr() as usize).abs_diff(self.as_ptr() as usize) >= count * core::mem::size_of::())] + #[ensures(|result: &()| ub_checks::can_dereference(src.as_ptr()))] + #[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr()))] + #[kani::modifies(self.as_ptr())] pub const unsafe fn copy_from(self, src: NonNull, count: usize) where T: Sized, @@ -994,6 +1015,14 @@ impl NonNull { #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_unstable(feature = "const_intrinsic_copy", issue = "80697")] + #[kani::requires(count * core::mem::size_of::() <= isize::MAX as usize)]//count check + #[requires(ub_checks::can_dereference(self.as_ptr()))] + #[requires(ub_checks::can_dereference(src.as_ptr()))] + #[requires((self.as_ptr() as usize).abs_diff(src.as_ptr() as usize) >= count * core::mem::size_of::())]//The source and destination regions do not overlap. + #[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr()))] + #[ensures(|result: &()| ub_checks::can_dereference(src.as_ptr()))] + #[kani::modifies(self.as_ptr())] + #[kani::modifies(src.as_ptr())] pub const unsafe fn copy_from_nonoverlapping(self, src: NonNull, count: usize) where T: Sized, @@ -1781,7 +1810,7 @@ impl From<&T> for NonNull { } #[cfg(kani)] -#[unstable(feature="kani", issue="none")] +#[unstable(feature = "kani", issue = "none")] mod verify { use super::*; use crate::ptr::null_mut; @@ -1800,7 +1829,113 @@ mod verify { pub fn non_null_check_new() { let mut x: i32 = kani::any(); let xptr = &mut x; - let maybe_null_ptr = if kani::any() { xptr as *mut i32 } else { null_mut() }; + let maybe_null_ptr = if kani::any() { + xptr as *mut i32 + } else { + null_mut() + }; let _ = NonNull::new(maybe_null_ptr); } + + #[kani::proof_for_contract(NonNull::::copy_to)] + pub fn non_null_check_copy_to() { + // Create source and destination values + let mut src_value: i32 = kani::any(); + let mut dest_value: i32 = 0; + + // Create NonNull pointers + let src = NonNull::new(&mut src_value as *mut i32).unwrap(); + let dest = NonNull::new(&mut dest_value as *mut i32).unwrap(); + //casting the pointer + let src_u8 = src.as_ptr() as *const u8; + let dest_u8 = dest.as_ptr() as *mut u8; + //count is 1 as working with single i32 value + let count = 1; + unsafe { + kani::assume(kani::mem::can_dereference(src_u8)); + kani::assume(kani::mem::can_dereference( + src_u8.add(core::mem::size_of::() - 1), + )); + kani::assume(kani::mem::can_dereference(dest_u8)); + kani::assume(kani::mem::can_dereference( + dest_u8.add(core::mem::size_of::() - 1), + )); + src.copy_to(dest, count); + } + } + #[kani::proof_for_contract(NonNull::::copy_from)] + pub fn non_null_check_copy_from() { + // Create source and destination values + let mut src_value: i32 = kani::any(); + let mut dest_value: i32 = 0; + + // Create NonNull pointers + let src = NonNull::new(&mut src_value as *mut i32).unwrap(); + let dest = NonNull::new(&mut dest_value as *mut i32).unwrap(); + //casting the pointer + let src_u8 = src.as_ptr() as *const u8; + let dest_u8 = dest.as_ptr() as *mut u8; + //count is 1 as working with single i32 value + let count = 1; + unsafe { + kani::assume(kani::mem::can_dereference(src_u8)); + kani::assume(kani::mem::can_dereference( + src_u8.add(core::mem::size_of::() - 1), + )); + kani::assume(kani::mem::can_dereference(dest_u8)); + kani::assume(kani::mem::can_dereference( + dest_u8.add(core::mem::size_of::() - 1), + )); + src.copy_from(dest, count); + } + } + #[kani::proof_for_contract(NonNull::::copy_to_nonoverlapping)] + pub fn non_null_check_copy_to_nonoverlapping() { + let mut src_value: i32 = kani::any(); + let mut dest_value: i32 = 0; + + let src = NonNull::new(&mut src_value as *mut i32).unwrap(); + let dest = NonNull::new(&mut dest_value as *mut i32).unwrap(); + //casting the pointer + let src_u8 = src.as_ptr() as *const u8; + let dest_u8 = dest.as_ptr() as *mut u8; + //count represents no of elements to copy + let count = 1; + unsafe { + kani::assume(kani::mem::can_dereference(src_u8)); + kani::assume(kani::mem::can_dereference( + src_u8.add(core::mem::size_of::() - 1), + )); + kani::assume(kani::mem::can_dereference(dest_u8)); + kani::assume(kani::mem::can_dereference( + dest_u8.add(core::mem::size_of::() - 1), + )); + src.copy_to_nonoverlapping(dest, count); + } + } + #[kani::proof_for_contract(NonNull::::copy_from_nonoverlapping)] + pub fn non_null_check_copy_from_nonoverlapping() { + let mut src_value: i32 = kani::any(); + let mut dest_value: i32 = 0; + + let src = NonNull::new(&mut src_value as *mut i32).unwrap(); + let dest = NonNull::new(&mut dest_value as *mut i32).unwrap(); + //casting the pointer + let src_u8 = src.as_ptr() as *const u8; + let dest_u8 = dest.as_ptr() as *mut u8; + //count represents no of elements to copy + let count = 1; + + unsafe { + kani::assume(kani::mem::can_dereference(src_u8)); + kani::assume(kani::mem::can_dereference( + src_u8.add(core::mem::size_of::() - 1), + )); + kani::assume(kani::mem::can_dereference(dest_u8)); + kani::assume(kani::mem::can_dereference( + dest_u8.add(core::mem::size_of::() - 1), + )); + dest.copy_from_nonoverlapping(src, count); + } + } } From 50521ab49db08481540712a283959ee1f5632d6e Mon Sep 17 00:00:00 2001 From: Dhvani-Kapadia <159494547+Dhvani-Kapadia@users.noreply.github.com> Date: Sat, 2 Nov 2024 12:27:45 -0700 Subject: [PATCH 02/14] Update non_null.rs --- library/core/src/ptr/non_null.rs | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 57ee0ae1b846e..fd8a70fd65381 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1810,7 +1810,7 @@ impl From<&T> for NonNull { } #[cfg(kani)] -#[unstable(feature = "kani", issue = "none")] +#[unstable(feature="kani", issue="none")] mod verify { use super::*; use crate::ptr::null_mut; @@ -1829,11 +1829,7 @@ mod verify { pub fn non_null_check_new() { let mut x: i32 = kani::any(); let xptr = &mut x; - let maybe_null_ptr = if kani::any() { - xptr as *mut i32 - } else { - null_mut() - }; + let maybe_null_ptr = if kani::any() { xptr as *mut i32 } else { null_mut() }; let _ = NonNull::new(maybe_null_ptr); } From 5e7ba89e7138f71e7b1f1e14f7684d659f02b43b Mon Sep 17 00:00:00 2001 From: Dhvani-Kapadia <159494547+Dhvani-Kapadia@users.noreply.github.com> Date: Sat, 2 Nov 2024 12:29:21 -0700 Subject: [PATCH 03/14] Update non_null.rs --- library/core/src/ptr/non_null.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index fd8a70fd65381..cdef6152a458c 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1829,7 +1829,7 @@ mod verify { pub fn non_null_check_new() { let mut x: i32 = kani::any(); let xptr = &mut x; - let maybe_null_ptr = if kani::any() { xptr as *mut i32 } else { null_mut() }; + let maybe_null_ptr = if kani::any() { xptr as *mut i32 } else { null_mut() }; let _ = NonNull::new(maybe_null_ptr); } From dac703d541bd1df127ec5b840cd40e97386d6391 Mon Sep 17 00:00:00 2001 From: Dhvani-Kapadia <159494547+Dhvani-Kapadia@users.noreply.github.com> Date: Fri, 8 Nov 2024 11:31:41 -0800 Subject: [PATCH 04/14] Update non_null.rs --- library/core/src/ptr/non_null.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index cdef6152a458c..fd8a70fd65381 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1829,7 +1829,7 @@ mod verify { pub fn non_null_check_new() { let mut x: i32 = kani::any(); let xptr = &mut x; - let maybe_null_ptr = if kani::any() { xptr as *mut i32 } else { null_mut() }; + let maybe_null_ptr = if kani::any() { xptr as *mut i32 } else { null_mut() }; let _ = NonNull::new(maybe_null_ptr); } From d024fc295a2ab20620e4b8aec61c7fd45d237704 Mon Sep 17 00:00:00 2001 From: Dhvani-Kapadia <159494547+Dhvani-Kapadia@users.noreply.github.com> Date: Wed, 13 Nov 2024 00:00:34 -0800 Subject: [PATCH 05/14] feedback --- error.log | 50 + library/core/src/ptr/non_null.rs | 148 +-- verify-err.log | 0 verify-error.log | 1666 ++++++++++++++++++++++++++++++ 4 files changed, 1763 insertions(+), 101 deletions(-) create mode 100644 error.log create mode 100644 verify-err.log create mode 100644 verify-error.log diff --git a/error.log b/error.log new file mode 100644 index 0000000000000..c8749fe08bc0f --- /dev/null +++ b/error.log @@ -0,0 +1,50 @@ +Kani Rust Verifier 0.56.0 (standalone) +error: expected `]`, found `&&` + --> /Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/ptr/non_null.rs:943:99 + | +173 | impl NonNull { + | - while parsing this item list starting here +... +943 | ub_checks::can_dereference(dest.as_ptr() as *const T, count * core::mem::size_of::())) &&//The pointer is valid for the specified number of ... + | ^^ expected `]` +... +1447 | } + | - the item list ends here + +error[E0599]: no method named `copy_to` found for struct `ptr::non_null::NonNull` in the current scope + --> /Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/ptr/non_null.rs:1846:13 + | +76 | pub struct NonNull { + | ----------------------------- method `copy_to` not found for this struct +... +1846 | src.copy_to(dest, count); + | ^^^^^^^ method not found in `NonNull` + | +help: one of the expressions' fields has a method of the same name + | +1846 | src.pointer.copy_to(dest, count); + | ++++++++ + +error[E0599]: no method named `copy_from` found for struct `ptr::non_null::NonNull` in the current scope + --> /Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/ptr/non_null.rs:1863:13 + | +76 | pub struct NonNull { + | ----------------------------- method `copy_from` not found for this struct +... +1863 | src.copy_from(dest, count); + | ^^^^^^^^^ + | +help: there is a method `clone_from` with a similar name, but with different arguments + --> /Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/clone.rs:174:5 + | +174 | fn clone_from(&mut self, source: &Self) { + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +error[E0599]: no method named `is_aligned` found for reference `&ptr::non_null::NonNull` in the current scope + --> /Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/alloc/layout.rs:254:31 + | +254 | #[ensures(|result| result.is_aligned())] + | ^^^^^^^^^^ method not found in `&NonNull` + +For more information about this error, try `rustc --explain E0599`. +error: Failed to execute cargo (exit status: 101). Found 4 compilation errors. diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index a77ed310c4179..f4534f0b5d9b8 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -964,17 +964,14 @@ impl NonNull { #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[stable(feature = "non_null_convenience", since = "1.80.0")] -<<<<<<< HEAD - #[rustc_const_unstable(feature = "const_intrinsic_copy", issue = "80697")] - #[kani::requires(count * core::mem::size_of::() <= isize::MAX as usize)] - #[requires(ub_checks::can_dereference(self.as_ptr()))] //The pointer is valid - #[requires(ub_checks::can_dereference(dest.as_ptr()))] - #[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr() as *const T))] - #[ensures(|result: &()| ub_checks::can_dereference(dest.as_ptr() as *const T))] - #[kani::modifies(dest.as_ptr())] -======= #[rustc_const_stable(feature = "const_intrinsic_copy", since = "1.83.0")] ->>>>>>> origin + #[requires(count.checked_mul(core::mem::size_of::()).map_or(false, |size| size <= isize::MAX as usize) + && ub_checks::can_dereference(self.as_ptr() as *const MaybeUninit) + && ub_checks::can_write(dest.as_ptr()) + && ub_checks::can_write(dest.as_ptr().add(count)))] + #[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr() as *const u8) + && ub_checks::can_dereference(dest.as_ptr() as *const u8))] + #[kani::modifies(dest.as_ptr())] pub const unsafe fn copy_to(self, dest: NonNull, count: usize) where T: Sized, @@ -994,19 +991,15 @@ impl NonNull { #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[stable(feature = "non_null_convenience", since = "1.80.0")] -<<<<<<< HEAD - #[rustc_const_unstable(feature = "const_intrinsic_copy", issue = "80697")] - #[kani::requires(count * core::mem::size_of::() <= isize::MAX as usize)] - #[requires(ub_checks::can_dereference(self.as_ptr()))] - #[requires(ub_checks::can_dereference(dest.as_ptr()))] - #[requires((self.as_ptr() as usize).abs_diff(dest.as_ptr() as usize) >= count * core::mem::size_of::())] - #[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr()))] - #[ensures(|result: &()| ub_checks::can_dereference(dest.as_ptr()))] - #[kani::modifies(dest.as_ptr())] - #[kani::modifies(self.as_ptr())] -======= #[rustc_const_stable(feature = "const_intrinsic_copy", since = "1.83.0")] ->>>>>>> origin + #[requires(count.checked_mul(core::mem::size_of::()).map_or(false, |size| size <= isize::MAX as usize) + && ub_checks::can_dereference(self.as_ptr() as *const MaybeUninit) + && ub_checks::can_write(dest.as_ptr()) + && ub_checks::can_write(dest.as_ptr().add(count)) + && (self.as_ptr() as usize).abs_diff(dest.as_ptr() as usize) >= count * core::mem::size_of::())] + #[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr() as *const u8) + && ub_checks::can_dereference(dest.as_ptr() as *const u8))] + #[kani::modifies(dest.as_ptr())] pub const unsafe fn copy_to_nonoverlapping(self, dest: NonNull, count: usize) where T: Sized, @@ -1026,18 +1019,15 @@ impl NonNull { #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[stable(feature = "non_null_convenience", since = "1.80.0")] -<<<<<<< HEAD - #[rustc_const_unstable(feature = "const_intrinsic_copy", issue = "80697")] - #[kani::requires(count * core::mem::size_of::() <= isize::MAX as usize)] - #[requires(ub_checks::can_dereference(src.as_ptr()) )]//The pointer is valid - #[requires( ub_checks::can_dereference(self.as_ptr()))]//The pointer is valid - #[requires((src.as_ptr() as usize).abs_diff(self.as_ptr() as usize) >= count * core::mem::size_of::())] - #[ensures(|result: &()| ub_checks::can_dereference(src.as_ptr()))] - #[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr()))] - #[kani::modifies(self.as_ptr())] -======= #[rustc_const_stable(feature = "const_intrinsic_copy", since = "1.83.0")] ->>>>>>> origin + #[requires (count.checked_mul(core::mem::size_of::()).map_or(false, |size| size <= isize::MAX as usize + && ub_checks::can_dereference(src.as_ptr() as *const MaybeUninit) + && ub_checks::can_write(self.as_ptr()) + && ub_checks::can_write (self.as_ptr().add(count))) + && (src.as_ptr() as usize).abs_diff(self.as_ptr() as usize) >= count * core::mem::size_of::())] + #[ensures (|result: &()| ub_checks::can_dereference(src.as_ptr() as *const u8) + && ub_checks::can_dereference(self.as_ptr()))] + #[kani::modifies(self.as_ptr())] pub const unsafe fn copy_from(self, src: NonNull, count: usize) where T: Sized, @@ -1057,19 +1047,15 @@ impl NonNull { #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[stable(feature = "non_null_convenience", since = "1.80.0")] -<<<<<<< HEAD - #[rustc_const_unstable(feature = "const_intrinsic_copy", issue = "80697")] - #[kani::requires(count * core::mem::size_of::() <= isize::MAX as usize)]//count check - #[requires(ub_checks::can_dereference(self.as_ptr()))] - #[requires(ub_checks::can_dereference(src.as_ptr()))] - #[requires((self.as_ptr() as usize).abs_diff(src.as_ptr() as usize) >= count * core::mem::size_of::())]//The source and destination regions do not overlap. - #[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr()))] - #[ensures(|result: &()| ub_checks::can_dereference(src.as_ptr()))] - #[kani::modifies(self.as_ptr())] - #[kani::modifies(src.as_ptr())] -======= #[rustc_const_stable(feature = "const_intrinsic_copy", since = "1.83.0")] ->>>>>>> origin + #[requires (count.checked_mul(core::mem::size_of::()).map_or(false, |size| size <= isize::MAX as usize + && ub_checks::can_dereference(src.as_ptr() as *const MaybeUninit) + && ub_checks::can_write(self.as_ptr()) + && ub_checks::can_write(self.as_ptr().add(count))) + && (self.as_ptr() as usize).abs_diff(src.as_ptr() as usize) >= count * core::mem::size_of::())]//The source and destination regions do not overlap. + #[ensures (|result: &()| ub_checks::can_dereference(src.as_ptr() as *const u8) + && ub_checks::can_dereference(self.as_ptr()))] + #[kani::modifies(self.as_ptr())] pub const unsafe fn copy_from_nonoverlapping(self, src: NonNull, count: usize) where T: Sized, @@ -1856,6 +1842,7 @@ impl From<&T> for NonNull { mod verify { use super::*; use crate::ptr::null_mut; + use kani::PointerGenerator; // pub const unsafe fn new_unchecked(ptr: *mut T) -> Self #[kani::proof_for_contract(NonNull::new_unchecked)] @@ -1877,30 +1864,19 @@ mod verify { #[kani::proof_for_contract(NonNull::::copy_to)] pub fn non_null_check_copy_to() { - // Create source and destination values - let mut src_value: i32 = kani::any(); - let mut dest_value: i32 = 0; + // PointerGenerator instance + let mut generator = PointerGenerator::<16>::new(); + // Generate arbitrary pointers for src and dest + let src_ptr = generator.any_in_bounds::().ptr; + let dest_ptr = generator.any_in_bounds::().ptr; + // Wrap the raw pointers in NonNull + let src = NonNull::new(src_ptr).unwrap(); + let dest = NonNull::new(dest_ptr).unwrap(); + // Generate an arbitrary count using kani::any + let count: usize = kani::any(); + unsafe { src.copy_to(dest, count);} +} - // Create NonNull pointers - let src = NonNull::new(&mut src_value as *mut i32).unwrap(); - let dest = NonNull::new(&mut dest_value as *mut i32).unwrap(); - //casting the pointer - let src_u8 = src.as_ptr() as *const u8; - let dest_u8 = dest.as_ptr() as *mut u8; - //count is 1 as working with single i32 value - let count = 1; - unsafe { - kani::assume(kani::mem::can_dereference(src_u8)); - kani::assume(kani::mem::can_dereference( - src_u8.add(core::mem::size_of::() - 1), - )); - kani::assume(kani::mem::can_dereference(dest_u8)); - kani::assume(kani::mem::can_dereference( - dest_u8.add(core::mem::size_of::() - 1), - )); - src.copy_to(dest, count); - } - } #[kani::proof_for_contract(NonNull::::copy_from)] pub fn non_null_check_copy_from() { // Create source and destination values @@ -1910,20 +1886,10 @@ mod verify { // Create NonNull pointers let src = NonNull::new(&mut src_value as *mut i32).unwrap(); let dest = NonNull::new(&mut dest_value as *mut i32).unwrap(); - //casting the pointer - let src_u8 = src.as_ptr() as *const u8; - let dest_u8 = dest.as_ptr() as *mut u8; + //count is 1 as working with single i32 value let count = 1; unsafe { - kani::assume(kani::mem::can_dereference(src_u8)); - kani::assume(kani::mem::can_dereference( - src_u8.add(core::mem::size_of::() - 1), - )); - kani::assume(kani::mem::can_dereference(dest_u8)); - kani::assume(kani::mem::can_dereference( - dest_u8.add(core::mem::size_of::() - 1), - )); src.copy_from(dest, count); } } @@ -1934,20 +1900,10 @@ mod verify { let src = NonNull::new(&mut src_value as *mut i32).unwrap(); let dest = NonNull::new(&mut dest_value as *mut i32).unwrap(); - //casting the pointer - let src_u8 = src.as_ptr() as *const u8; - let dest_u8 = dest.as_ptr() as *mut u8; + //count represents no of elements to copy let count = 1; unsafe { - kani::assume(kani::mem::can_dereference(src_u8)); - kani::assume(kani::mem::can_dereference( - src_u8.add(core::mem::size_of::() - 1), - )); - kani::assume(kani::mem::can_dereference(dest_u8)); - kani::assume(kani::mem::can_dereference( - dest_u8.add(core::mem::size_of::() - 1), - )); src.copy_to_nonoverlapping(dest, count); } } @@ -1958,21 +1914,11 @@ mod verify { let src = NonNull::new(&mut src_value as *mut i32).unwrap(); let dest = NonNull::new(&mut dest_value as *mut i32).unwrap(); - //casting the pointer - let src_u8 = src.as_ptr() as *const u8; - let dest_u8 = dest.as_ptr() as *mut u8; + //count represents no of elements to copy let count = 1; unsafe { - kani::assume(kani::mem::can_dereference(src_u8)); - kani::assume(kani::mem::can_dereference( - src_u8.add(core::mem::size_of::() - 1), - )); - kani::assume(kani::mem::can_dereference(dest_u8)); - kani::assume(kani::mem::can_dereference( - dest_u8.add(core::mem::size_of::() - 1), - )); dest.copy_from_nonoverlapping(src, count); } } diff --git a/verify-err.log b/verify-err.log new file mode 100644 index 0000000000000..e69de29bb2d1d diff --git a/verify-error.log b/verify-error.log new file mode 100644 index 0000000000000..ad556b12c3b78 --- /dev/null +++ b/verify-error.log @@ -0,0 +1,1666 @@ +Kani Rust Verifier 0.56.0 (standalone) +Checking harness ptr::non_null::verify::non_null_check_copy_to... +CBMC 6.3.1 (cbmc-6.3.1) +CBMC version 6.3.1 (cbmc-6.3.1) 64-bit x86_64 macos +Reading GOTO program from file /Users/dhvanikapadia/Downloads/verify-rust-std/target/kani_verify_std/target/x86_64-apple-darwin/debug/deps/core-ccf4fba8e5214364__RNvNtNtNtCsdg7tvWISkkD_4core3ptr8non_null6verify22non_null_check_copy_to.out +Generating GOTO Program +Adding CPROVER library (x86_64) +Removal of function pointers and virtual functions +Generic Property Instrumentation +Running with 16 object bits, 48 offset bits (user-specified) +Starting Bounded Model Checking +aborting path on assume(false) at file /Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/option.rs line 969 column 15 function option::Option::>::unwrap thread 0 +aborting path on assume(false) at file /Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/option.rs line 2008 column 5 function option::unwrap_failed thread 0 +aborting path on assume(false) at file /Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/option.rs line 971 column 21 function option::Option::>::unwrap thread 0 +aborting path on assume(false) at file /Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/option.rs line 969 column 15 function option::Option::>::unwrap thread 0 +aborting path on assume(false) at file /Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/option.rs line 2008 column 5 function option::unwrap_failed thread 0 +aborting path on assume(false) at file /Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/option.rs line 971 column 21 function option::Option::>::unwrap thread 0 +aborting path on assume(false) at file /Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/option.rs line 1170 column 15 function option::Option::::map_or:: thread 0 +Runtime Symex: 0.459842s +size of program expression: 5048 steps +slicing removed 2760 assignments +Generated 330 VCC(s), 120 remaining after simplification +Runtime Postprocess Equation: 0.00268161s +Passing problem to propositional reduction +converting SSA +Runtime Convert SSA: 5.77538s +Running propositional reduction +Post-processing +Runtime Post-process: 0.0196502s +Solving with CaDiCaL 2.0.0 +156266 variables, 8577118 clauses +SAT checker: instance is SATISFIABLE +Runtime Solver: 0.0463924s +Runtime decision procedure: 5.82464s +Running propositional reduction +Solving with CaDiCaL 2.0.0 +156267 variables, 8577119 clauses +SAT checker: instance is SATISFIABLE +Runtime Solver: 0.00402602s +Runtime decision procedure: 0.00508257s +Running propositional reduction +Solving with CaDiCaL 2.0.0 +156268 variables, 8577120 clauses +SAT checker: instance is SATISFIABLE +Runtime Solver: 0.00341336s +Runtime decision procedure: 0.00449741s +Running propositional reduction +Solving with CaDiCaL 2.0.0 +156269 variables, 8577121 clauses +SAT checker: instance is SATISFIABLE +Runtime Solver: 0.00315195s +Runtime decision procedure: 0.00423291s +Running propositional reduction +Solving with CaDiCaL 2.0.0 +156270 variables, 8577122 clauses +SAT checker: instance is SATISFIABLE +Runtime Solver: 0.0126685s +Runtime decision procedure: 0.0137506s +Running propositional reduction +Solving with CaDiCaL 2.0.0 +156271 variables, 8577123 clauses +SAT checker: instance is SATISFIABLE +Runtime Solver: 0.00569658s +Runtime decision procedure: 0.00677048s +Running propositional reduction +Solving with CaDiCaL 2.0.0 +156272 variables, 8577124 clauses +SAT checker: instance is SATISFIABLE +Runtime Solver: 0.00284245s +Runtime decision procedure: 0.003917s +Running propositional reduction +Solving with CaDiCaL 2.0.0 +156273 variables, 8577125 clauses +SAT checker: instance is SATISFIABLE +Runtime Solver: 0.00519012s +Runtime decision procedure: 0.00622863s +Running propositional reduction +Solving with CaDiCaL 2.0.0 +156274 variables, 8577126 clauses +SAT checker: instance is SATISFIABLE +Runtime Solver: 0.00217965s +Runtime decision procedure: 0.00321794s +Running propositional reduction +Solving with CaDiCaL 2.0.0 +156275 variables, 8577127 clauses +SAT checker: instance is UNSATISFIABLE +Runtime Solver: 0.0236761s +Runtime decision procedure: 0.02421s + +RESULTS: +Check 1: __CPROVER_contracts_write_set_check_assignment.assertion.1 + - Status: SUCCESS + - Description: "ptr NULL or writable up to size" + - Location: :775 in function __CPROVER_contracts_write_set_check_assignment + +Check 2: __CPROVER_contracts_write_set_check_assignment.assertion.2 + - Status: SUCCESS + - Description: "CAR size is less than __CPROVER_max_malloc_size" + - Location: :792 in function __CPROVER_contracts_write_set_check_assignment + +Check 3: __CPROVER_contracts_write_set_check_assignment.assertion.3 + - Status: SUCCESS + - Description: "no offset bits overflow on CAR upper bound computation" + - Location: :798 in function __CPROVER_contracts_write_set_check_assignment + +Check 4: __CPROVER_contracts_write_set_check_assignment.unwind.1 + - Status: SUCCESS + - Description: "unwinding assertion loop 0" + - Location: :807 in function __CPROVER_contracts_write_set_check_assignment + +Check 5: __CPROVER_contracts_write_set_check_assignment.assertion.4 + - Status: SUCCESS + - Description: "ptr NULL or writable up to size" + - Location: :775 in function __CPROVER_contracts_write_set_check_assignment + +Check 6: __CPROVER_contracts_write_set_check_assignment.assertion.5 + - Status: SUCCESS + - Description: "CAR size is less than __CPROVER_max_malloc_size" + - Location: :792 in function __CPROVER_contracts_write_set_check_assignment + +Check 7: __CPROVER_contracts_write_set_check_assignment.assertion.6 + - Status: SUCCESS + - Description: "no offset bits overflow on CAR upper bound computation" + - Location: :798 in function __CPROVER_contracts_write_set_check_assignment + +Check 8: __CPROVER_contracts_write_set_check_assignment.unwind.2 + - Status: SUCCESS + - Description: "unwinding assertion loop 0" + - Location: :807 in function __CPROVER_contracts_write_set_check_assignment + +Check 9: __CPROVER_contracts_car_set_insert.assertion.1 + - Status: SUCCESS + - Description: "ptr NULL or writable up to size" + - Location: :161 in function __CPROVER_contracts_car_set_insert + +Check 10: __CPROVER_contracts_car_set_insert.assertion.2 + - Status: SUCCESS + - Description: "CAR size is less than __CPROVER_max_malloc_size" + - Location: :164 in function __CPROVER_contracts_car_set_insert + +Check 11: __CPROVER_contracts_car_set_insert.assertion.3 + - Status: SUCCESS + - Description: "no offset bits overflow on CAR upper bound computation" + - Location: :168 in function __CPROVER_contracts_car_set_insert + +Check 12: memmove.assigns.1 + - Status: SUCCESS + - Description: "Check that array_copy((const void *)src_n, ...) is allowed by the assigns clause" + - Location: :33 in function memmove + +Check 13: memmove.assigns.2 + - Status: FAILURE + - Description: "Check that array_replace((const void *)(char *)dest, ...) is allowed by the assigns clause" + - Location: :34 in function memmove + +Check 14: panicking::panic_fmt.unsupported_construct.1 + - Status: SUCCESS + - Description: "call to foreign "Rust" function `rust_begin_unwind` is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/new/choose" + - Location: library/core/src/panicking.rs:64:9 in function panicking::panic_fmt + +Check 15: option::Option::>::unwrap.unreachable.1 + - Status: SUCCESS + - Description: "unreachable code" + - Location: library/core/src/option.rs:969:15 in function option::Option::>::unwrap + +Check 16: free.frees.1 + - Status: SUCCESS + - Description: "Check that ptr is freeable" + - Location: :43 in function free + +Check 17: memcpy.assigns.1 + - Status: SUCCESS + - Description: "Check that array_copy((const void *)src_n, ...) is allowed by the assigns clause" + - Location: :45 in function memcpy + +Check 18: memcpy.assigns.2 + - Status: SUCCESS + - Description: "Check that array_replace((const void *)(char *)dst, ...) is allowed by the assigns clause" + - Location: :46 in function memcpy + +Check 19: __CPROVER_contracts_write_set_record_deallocated.unwind.1 + - Status: SUCCESS + - Description: "unwinding assertion loop 0" + - Location: :710 in function __CPROVER_contracts_write_set_record_deallocated + +Check 20: ub_checks::is_nonoverlapping::runtime.unreachable.1 + - Status: SUCCESS + - Description: "unreachable code" + - Location: library/core/src/ub_checks.rs:146:5 in function ub_checks::is_nonoverlapping::runtime + +Check 21: <() as kani::mem::PtrProperties>::is_ptr_aligned.assertion.1 + - Status: SUCCESS + - Description: "attempt to calculate the remainder with a divisor of zero" + - Location: ../../kani/library/kani_core/src/mem.rs:220:17 in function <() as kani::mem::PtrProperties>::is_ptr_aligned + +Check 22: <() as kani::mem::PtrProperties>::is_ptr_aligned.arithmetic_overflow.1 + - Status: SUCCESS + - Description: "attempt to calculate the remainder with a divisor of zero" + - Location: ../../kani/library/kani_core/src/mem.rs:220:17 in function <() as kani::mem::PtrProperties>::is_ptr_aligned + +Check 23: ptr::mut_ptr::::add::runtime_add_nowrap::runtime.unreachable.1 + - Status: SUCCESS + - Description: "unreachable code" + - Location: library/core/src/ptr/mut_ptr.rs:1010:13 in function ptr::mut_ptr::::add::runtime_add_nowrap::runtime + +Check 24: __CPROVER_contracts_write_set_check_assignment.assertion.7 + - Status: SUCCESS + - Description: "ptr NULL or writable up to size" + - Location: :775 in function __CPROVER_contracts_write_set_check_assignment + +Check 25: __CPROVER_contracts_write_set_check_assignment.assertion.8 + - Status: SUCCESS + - Description: "CAR size is less than __CPROVER_max_malloc_size" + - Location: :792 in function __CPROVER_contracts_write_set_check_assignment + +Check 26: __CPROVER_contracts_write_set_check_assignment.assertion.9 + - Status: SUCCESS + - Description: "no offset bits overflow on CAR upper bound computation" + - Location: :798 in function __CPROVER_contracts_write_set_check_assignment + +Check 27: __CPROVER_contracts_write_set_check_assignment.unwind.3 + - Status: SUCCESS + - Description: "unwinding assertion loop 0" + - Location: :807 in function __CPROVER_contracts_write_set_check_assignment + +Check 28: <() as kani::mem::PtrProperties>::is_ptr_aligned.assertion.1 + - Status: SUCCESS + - Description: "attempt to calculate the remainder with a divisor of zero" + - Location: ../../kani/library/kani_core/src/mem.rs:220:17 in function <() as kani::mem::PtrProperties>::is_ptr_aligned + +Check 29: <() as kani::mem::PtrProperties>::is_ptr_aligned.arithmetic_overflow.1 + - Status: SUCCESS + - Description: "attempt to calculate the remainder with a divisor of zero" + - Location: ../../kani/library/kani_core/src/mem.rs:220:17 in function <() as kani::mem::PtrProperties>::is_ptr_aligned + +Check 30: option::Option::::map_or::.unreachable.1 + - Status: SUCCESS + - Description: "unreachable code" + - Location: library/core/src/option.rs:1170:15 in function option::Option::::map_or:: + +Check 31: kani::mem::is_inbounds::<(), u8>.assertion.1 + - Status: SUCCESS + - Description: "Kani does not support reasoning about pointer to unallocated memory" + - Location: library/core/src/lib.rs:421:1 in function kani::mem::is_inbounds::<(), u8> + +Check 32: kani::mem::assert_is_initialized::.assertion.1 + - Status: SUCCESS + - Description: "Undefined Behavior: Reading from an uninitialized pointer" + - Location: library/core/src/lib.rs:421:1 in function kani::mem::assert_is_initialized:: + +Check 33: ptr::mut_ptr::::add.arithmetic_overflow.1 + - Status: SUCCESS + - Description: "offset: attempt to compute number in bytes which would overflow" + - Location: library/core/src/ptr/mut_ptr.rs:1037:18 in function ptr::mut_ptr::::add + +Check 34: ptr::mut_ptr::::add.arithmetic_overflow.2 + - Status: SUCCESS + - Description: "attempt to compute offset which would overflow" + - Location: library/core/src/ptr/mut_ptr.rs:1037:18 in function ptr::mut_ptr::::add + +Check 35: fmt::Arguments::<'_>::new_const::<1>.assigns.1 + - Status: SUCCESS + - Description: "Check that *((unsigned char **)&temp_0) is assignable" + - Location: library/core/src/fmt/mod.rs:342:34 in function fmt::Arguments::<'_>::new_const::<1> + +Check 36: kani::mem::is_inbounds::<(), i32>.assertion.1 + - Status: FAILURE + - Description: "Kani does not support reasoning about pointer to unallocated memory" + - Location: library/core/src/lib.rs:421:1 in function kani::mem::is_inbounds::<(), i32> + +Check 37: >::copy_to::{closure#2}::{closure#2}.single_top_level_call.1 + - Status: SUCCESS + - Description: "Only a single top-level call to function _RNCNCNvMs1_NtNtCsdg7tvWISkkD_4core3ptr8non_nullINtB9_7NonNulllE7copy_tos0_0s0_0Bd_ when checking contract _RNCNCNvMs1_NtNtCsdg7tvWISkkD_4core3ptr8non_nullINtB9_7NonNulllE7copy_tos0_0s0_0Bd_" + - Location: library/core/src/ptr/non_null.rs:974:5 in function >::copy_to::{closure#2}::{closure#2} + +Check 38: >::copy_to::{closure#2}::{closure#2}.no_alloc_dealloc_in_requires.1 + - Status: SUCCESS + - Description: "Check that requires do not allocate or deallocate memory" + - Location: library/core/src/ptr/non_null.rs:974:5 in function >::copy_to::{closure#2}::{closure#2} + +Check 39: >::copy_to::{closure#2}::{closure#2}.no_alloc_dealloc_in_ensures.1 + - Status: SUCCESS + - Description: "Check that ensures do not allocate or deallocate memory" + - Location: library/core/src/ptr/non_null.rs:974:5 in function >::copy_to::{closure#2}::{closure#2} + +Check 40: >::copy_to::{closure#2}::{closure#2}.no_recursive_call.1 + - Status: SUCCESS + - Description: "No recursive call to function _RNCNCNvMs1_NtNtCsdg7tvWISkkD_4core3ptr8non_nullINtB9_7NonNulllE7copy_tos0_0s0_0Bd_ when checking contract _RNCNCNvMs1_NtNtCsdg7tvWISkkD_4core3ptr8non_nullINtB9_7NonNulllE7copy_tos0_0s0_0Bd_" + - Location: library/core/src/ptr/non_null.rs:974:5 in function >::copy_to::{closure#2}::{closure#2} + +Check 41: panic::location::Location::<'_>::caller.unsupported_construct.1 + - Status: SUCCESS + - Description: "caller_location is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/374" + - Location: library/core/src/panic/location.rs:89:9 in function panic::location::Location::<'_>::caller + +Check 42: ptr::non_null::NonNull::::copy_to::{closure#1}.unreachable.1 + - Status: SUCCESS + - Description: "unreachable code" + - Location: library/core/src/ptr/non_null.rs:968:5 in function ptr::non_null::NonNull::::copy_to::{closure#1} + +Check 43: ptr::non_null::NonNull::::new::{closure#2}.unreachable.1 + - Status: SUCCESS + - Description: "unreachable code" + - Location: library/core/src/ptr/non_null.rs:229:5 in function ptr::non_null::NonNull::::new::{closure#2} + +Check 44: ptr::non_null::NonNull::::new_unchecked::{closure#0}.unreachable.1 + - Status: SUCCESS + - Description: "unreachable code" + - Location: library/core/src/ptr/non_null.rs:198:5 in function ptr::non_null::NonNull::::new_unchecked::{closure#0} + +Check 45: kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0}.assertion.1 + - Status: SUCCESS + - Description: "attempt to subtract with overflow" + - Location: ../../kani/library/kani_core/src/arbitrary/pointer.rs:334:64 in function kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0} + +Check 46: ptr::non_null::NonNull::::new.assigns.1 + - Status: SUCCESS + - Description: "Check that *((unsigned char **)&temp_0) is assignable" + - Location: library/core/src/ptr/non_null.rs:236:13 in function ptr::non_null::NonNull::::new + +Check 47: num::::abs_diff.assertion.1 + - Status: UNREACHABLE + - Description: "attempt to subtract with overflow" + - Location: library/core/src/num/uint_macros.rs:2426:21 in function num::::abs_diff + +Check 48: num::::abs_diff.assertion.2 + - Status: UNREACHABLE + - Description: "attempt to subtract with overflow" + - Location: library/core/src/num/uint_macros.rs:2428:21 in function num::::abs_diff + +Check 49: ptr::mut_ptr::::add.arithmetic_overflow.1 + - Status: SUCCESS + - Description: "offset: attempt to compute number in bytes which would overflow" + - Location: library/core/src/ptr/mut_ptr.rs:1037:18 in function ptr::mut_ptr::::add + +Check 50: ptr::mut_ptr::::add.arithmetic_overflow.2 + - Status: FAILURE + - Description: "attempt to compute offset which would overflow" + - Location: library/core/src/ptr/mut_ptr.rs:1037:18 in function ptr::mut_ptr::::add + +Check 51: ptr::non_null::NonNull::::copy_to::{closure#2}.assertion.1 + - Status: SUCCESS + - Description: "|result: &()| ub_checks::can_dereference(self.as_ptr() as *const u8) && +ub_checks::can_dereference(dest.as_ptr() as *const u8)" + - Location: library/core/src/ptr/non_null.rs:972:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 52: kani::arbitrary_ptr::PointerGenerator::<16>::any_in_bounds::.assertion.1 + - Status: SUCCESS + - Description: "This is a placeholder message; Kani doesn't support message formatted at runtime" + - Location: library/core/src/lib.rs:421:1 in function kani::arbitrary_ptr::PointerGenerator::<16>::any_in_bounds:: + +Check 53: intrinsics::copy::.safety_check.1 + - Status: SUCCESS + - Description: "`src` must be properly aligned" + - Location: library/core/src/intrinsics.rs:3414:9 in function intrinsics::copy:: + +Check 54: intrinsics::copy::.safety_check.2 + - Status: SUCCESS + - Description: "`dst` must be properly aligned" + - Location: library/core/src/intrinsics.rs:3414:9 in function intrinsics::copy:: + +Check 55: intrinsics::copy::.arithmetic_overflow.1 + - Status: SUCCESS + - Description: "copy: attempt to compute number in bytes which would overflow" + - Location: library/core/src/intrinsics.rs:3414:9 in function intrinsics::copy:: + +Check 56: ptr::non_null::NonNull::::new_unchecked::{closure#1}.unreachable.1 + - Status: SUCCESS + - Description: "unreachable code" + - Location: library/core/src/ptr/non_null.rs:198:5 in function ptr::non_null::NonNull::::new_unchecked::{closure#1} + +Check 57: option::unwrap_failed.assertion.1 + - Status: SUCCESS + - Description: "called `Option::unwrap()` on a `None` value" + - Location: library/core/src/option.rs:2008:5 in function option::unwrap_failed + +Check 58: num::::abs.assertion.1 + - Status: UNREACHABLE + - Description: "attempt to negate with overflow" + - Location: library/core/src/num/int_macros.rs:3381:17 in function num::::abs + +Check 59: kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::.assertion.1 + - Status: SUCCESS + - Description: "This is a placeholder message; Kani doesn't support message formatted at runtime" + - Location: library/core/src/lib.rs:421:1 in function kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr:: + +Check 60: kani::mem::assert_is_initialized::>.assertion.1 + - Status: SUCCESS + - Description: "Undefined Behavior: Reading from an uninitialized pointer" + - Location: library/core/src/lib.rs:421:1 in function kani::mem::assert_is_initialized::> + +Check 61: ptr::non_null::NonNull::::new_unchecked::{closure#2}.unreachable.1 + - Status: SUCCESS + - Description: "unreachable code" + - Location: library/core/src/ptr/non_null.rs:198:5 in function ptr::non_null::NonNull::::new_unchecked::{closure#2} + +Check 62: ptr::non_null::NonNull::::copy_to::{closure#0}.unreachable.1 + - Status: SUCCESS + - Description: "unreachable code" + - Location: library/core/src/ptr/non_null.rs:968:5 in function ptr::non_null::NonNull::::copy_to::{closure#0} + +Check 63: ptr::const_ptr::::is_aligned_to.assertion.1 + - Status: SUCCESS + - Description: "This is a placeholder message; Kani doesn't support message formatted at runtime" + - Location: library/core/src/ptr/const_ptr.rs:1640:13 in function ptr::const_ptr::::is_aligned_to + +Check 64: <() as kani::mem::PtrProperties>>::is_ptr_aligned.assertion.1 + - Status: SUCCESS + - Description: "attempt to calculate the remainder with a divisor of zero" + - Location: ../../kani/library/kani_core/src/mem.rs:220:17 in function <() as kani::mem::PtrProperties>>::is_ptr_aligned + +Check 65: <() as kani::mem::PtrProperties>>::is_ptr_aligned.arithmetic_overflow.1 + - Status: SUCCESS + - Description: "attempt to calculate the remainder with a divisor of zero" + - Location: ../../kani/library/kani_core/src/mem.rs:220:17 in function <() as kani::mem::PtrProperties>>::is_ptr_aligned + +Check 66: ptr::const_ptr::::is_aligned_to::runtime_impl.assertion.1 + - Status: UNREACHABLE + - Description: "attempt to subtract with overflow" + - Location: library/core/src/ptr/const_ptr.rs:1645:26 in function ptr::const_ptr::::is_aligned_to::runtime_impl + +Check 67: ptr::non_null::NonNull::::new::{closure#0}.unreachable.1 + - Status: SUCCESS + - Description: "unreachable code" + - Location: library/core/src/ptr/non_null.rs:229:5 in function ptr::non_null::NonNull::::new::{closure#0} + +Check 68: intrinsics::copy_nonoverlapping::.safety_check.1 + - Status: SUCCESS + - Description: "`src` must be properly aligned" + - Location: library/core/src/intrinsics.rs:3308:14 in function intrinsics::copy_nonoverlapping:: + +Check 69: intrinsics::copy_nonoverlapping::.safety_check.2 + - Status: SUCCESS + - Description: "`dst` must be properly aligned" + - Location: library/core/src/intrinsics.rs:3308:14 in function intrinsics::copy_nonoverlapping:: + +Check 70: intrinsics::copy_nonoverlapping::.arithmetic_overflow.1 + - Status: SUCCESS + - Description: "copy_nonoverlapping: attempt to compute number in bytes which would overflow" + - Location: library/core/src/intrinsics.rs:3308:14 in function intrinsics::copy_nonoverlapping:: + +Check 71: ptr::non_null::NonNull::::new::{closure#1}.unreachable.1 + - Status: SUCCESS + - Description: "unreachable code" + - Location: library/core/src/ptr/non_null.rs:229:5 in function ptr::non_null::NonNull::::new::{closure#1} + +Check 72: kani::mem::is_inbounds::<(), mem::maybe_uninit::MaybeUninit>.assertion.1 + - Status: SUCCESS + - Description: "Kani does not support reasoning about pointer to unallocated memory" + - Location: library/core/src/lib.rs:421:1 in function kani::mem::is_inbounds::<(), mem::maybe_uninit::MaybeUninit> + +Check 73: __sincospi.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:685 in function __sincospi + +Check 74: __sincospi.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:685 in function __sincospi + +Check 75: __sincospi.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:685 in function __sincospi + +Check 76: __sincospi.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:685 in function __sincospi + +Check 77: __sincospi.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:685 in function __sincospi + +Check 78: __sincospi.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:685 in function __sincospi + +Check 79: __sincospi.pointer_dereference.7 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:685 in function __sincospi + +Check 80: __sincospi.pointer_dereference.8 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:685 in function __sincospi + +Check 81: __sincospi.pointer_dereference.9 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:685 in function __sincospi + +Check 82: __sincospi.pointer_dereference.10 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:685 in function __sincospi + +Check 83: __sincospi.pointer_dereference.11 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:685 in function __sincospi + +Check 84: __sincospi.pointer_dereference.12 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:685 in function __sincospi + +Check 85: __sincos.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:675 in function __sincos + +Check 86: __sincos.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:675 in function __sincos + +Check 87: __sincos.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:675 in function __sincos + +Check 88: __sincos.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:675 in function __sincos + +Check 89: __sincos.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:675 in function __sincos + +Check 90: __sincos.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:675 in function __sincos + +Check 91: __sincos.pointer_dereference.7 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:675 in function __sincos + +Check 92: __sincos.pointer_dereference.8 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:675 in function __sincos + +Check 93: __sincos.pointer_dereference.9 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:675 in function __sincos + +Check 94: __sincos.pointer_dereference.10 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:675 in function __sincos + +Check 95: __sincos.pointer_dereference.11 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:675 in function __sincos + +Check 96: __sincos.pointer_dereference.12 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:675 in function __sincos + +Check 97: __sincospif.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:680 in function __sincospif + +Check 98: __sincospif.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:680 in function __sincospif + +Check 99: __sincospif.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:680 in function __sincospif + +Check 100: __sincospif.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:680 in function __sincospif + +Check 101: __sincospif.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:680 in function __sincospif + +Check 102: __sincospif.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:680 in function __sincospif + +Check 103: __sincospif.pointer_dereference.7 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:680 in function __sincospif + +Check 104: __sincospif.pointer_dereference.8 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:680 in function __sincospif + +Check 105: __sincospif.pointer_dereference.9 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:680 in function __sincospif + +Check 106: __sincospif.pointer_dereference.10 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:680 in function __sincospif + +Check 107: __sincospif.pointer_dereference.11 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:680 in function __sincospif + +Check 108: __sincospif.pointer_dereference.12 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:680 in function __sincospif + +Check 109: __sincosf.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:670 in function __sincosf + +Check 110: __sincosf.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:670 in function __sincosf + +Check 111: __sincosf.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:670 in function __sincosf + +Check 112: __sincosf.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:670 in function __sincosf + +Check 113: __sincosf.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:670 in function __sincosf + +Check 114: __sincosf.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:670 in function __sincosf + +Check 115: __sincosf.pointer_dereference.7 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:670 in function __sincosf + +Check 116: __sincosf.pointer_dereference.8 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:670 in function __sincosf + +Check 117: __sincosf.pointer_dereference.9 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:670 in function __sincosf + +Check 118: __sincosf.pointer_dereference.10 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:670 in function __sincosf + +Check 119: __sincosf.pointer_dereference.11 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:670 in function __sincosf + +Check 120: __sincosf.pointer_dereference.12 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:670 in function __sincosf + +Check 121: __CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.1 + - Status: SUCCESS + - Description: "count leading zeros is undefined for value zero" + - Location: :251 in function __CPROVER_contracts_obj_set_create_indexed_by_object_id + +Check 122: ptr::non_null::verify::non_null_check_copy_to.precondition_instance.1 + - Status: SUCCESS + - Description: "free argument must be NULL or valid pointer" + - Location: library/core/src/ptr/non_null.rs:1884:5 in function ptr::non_null::verify::non_null_check_copy_to + +Check 123: ptr::non_null::verify::non_null_check_copy_to.precondition_instance.2 + - Status: SUCCESS + - Description: "free argument must be dynamic object" + - Location: library/core/src/ptr/non_null.rs:1884:5 in function ptr::non_null::verify::non_null_check_copy_to + +Check 124: ptr::non_null::verify::non_null_check_copy_to.precondition_instance.3 + - Status: SUCCESS + - Description: "free argument has offset zero" + - Location: library/core/src/ptr/non_null.rs:1884:5 in function ptr::non_null::verify::non_null_check_copy_to + +Check 125: ptr::non_null::verify::non_null_check_copy_to.precondition_instance.4 + - Status: SUCCESS + - Description: "double free" + - Location: library/core/src/ptr/non_null.rs:1884:5 in function ptr::non_null::verify::non_null_check_copy_to + +Check 126: ptr::non_null::verify::non_null_check_copy_to.precondition_instance.5 + - Status: SUCCESS + - Description: "free called for new[] object" + - Location: library/core/src/ptr/non_null.rs:1884:5 in function ptr::non_null::verify::non_null_check_copy_to + +Check 127: ptr::non_null::verify::non_null_check_copy_to.precondition_instance.6 + - Status: SUCCESS + - Description: "free called for stack-allocated object" + - Location: library/core/src/ptr/non_null.rs:1884:5 in function ptr::non_null::verify::non_null_check_copy_to + +Check 128: <() as kani::mem::PtrProperties>>::is_ptr_aligned.division-by-zero.1 + - Status: SUCCESS + - Description: "division by zero" + - Location: ../../kani/library/kani_core/src/mem.rs:220:17 in function <() as kani::mem::PtrProperties>>::is_ptr_aligned + +Check 129: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: library/core/src/ptr/non_null.rs:972:56 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} + +Check 130: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: library/core/src/ptr/non_null.rs:972:56 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} + +Check 131: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: library/core/src/ptr/non_null.rs:972:56 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} + +Check 132: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:972:56 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} + +Check 133: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: library/core/src/ptr/non_null.rs:972:56 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} + +Check 134: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: library/core/src/ptr/non_null.rs:972:56 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} + +Check 135: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.7 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: library/core/src/ptr/non_null.rs:972:56 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} + +Check 136: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.8 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: library/core/src/ptr/non_null.rs:972:56 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} + +Check 137: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.9 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: library/core/src/ptr/non_null.rs:972:56 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} + +Check 138: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.10 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:972:56 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} + +Check 139: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.11 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: library/core/src/ptr/non_null.rs:972:56 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} + +Check 140: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.12 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: library/core/src/ptr/non_null.rs:972:56 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} + +Check 141: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.13 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: library/core/src/ptr/non_null.rs:973:39 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} + +Check 142: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.14 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: library/core/src/ptr/non_null.rs:973:39 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} + +Check 143: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.15 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: library/core/src/ptr/non_null.rs:973:39 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} + +Check 144: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.16 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:973:39 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} + +Check 145: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.17 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: library/core/src/ptr/non_null.rs:973:39 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} + +Check 146: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.18 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: library/core/src/ptr/non_null.rs:973:39 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} + +Check 147: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.19 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: library/core/src/ptr/non_null.rs:973:39 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} + +Check 148: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.20 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: library/core/src/ptr/non_null.rs:973:39 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} + +Check 149: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.21 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: library/core/src/ptr/non_null.rs:973:39 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} + +Check 150: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.22 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:973:39 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} + +Check 151: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.23 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: library/core/src/ptr/non_null.rs:973:39 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} + +Check 152: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.24 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: library/core/src/ptr/non_null.rs:973:39 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} + +Check 153: __CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.2 + - Status: SUCCESS + - Description: "count leading zeros is undefined for value zero" + - Location: :251 in function __CPROVER_contracts_obj_set_create_indexed_by_object_id + +Check 154: __CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.3 + - Status: SUCCESS + - Description: "count leading zeros is undefined for value zero" + - Location: :251 in function __CPROVER_contracts_obj_set_create_indexed_by_object_id + +Check 155: __CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.4 + - Status: SUCCESS + - Description: "count leading zeros is undefined for value zero" + - Location: :251 in function __CPROVER_contracts_obj_set_create_indexed_by_object_id + +Check 156: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: library/core/src/ptr/non_null.rs:968:16 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 157: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: library/core/src/ptr/non_null.rs:968:16 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 158: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: library/core/src/ptr/non_null.rs:968:16 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 159: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:968:16 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 160: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: library/core/src/ptr/non_null.rs:968:16 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 161: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: library/core/src/ptr/non_null.rs:968:16 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 162: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.7 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: library/core/src/ptr/non_null.rs:968:16 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 163: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.8 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: library/core/src/ptr/non_null.rs:968:16 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 164: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.9 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: library/core/src/ptr/non_null.rs:968:16 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 165: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.10 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:968:16 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 166: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.11 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: library/core/src/ptr/non_null.rs:968:16 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 167: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.12 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: library/core/src/ptr/non_null.rs:968:16 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 168: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.13 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: library/core/src/ptr/non_null.rs:969:39 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 169: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.14 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: library/core/src/ptr/non_null.rs:969:39 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 170: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.15 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: library/core/src/ptr/non_null.rs:969:39 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 171: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.16 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:969:39 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 172: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.17 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: library/core/src/ptr/non_null.rs:969:39 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 173: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.18 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: library/core/src/ptr/non_null.rs:969:39 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 174: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.19 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: library/core/src/ptr/non_null.rs:969:39 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 175: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.20 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: library/core/src/ptr/non_null.rs:969:39 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 176: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.21 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: library/core/src/ptr/non_null.rs:969:39 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 177: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.22 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:969:39 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 178: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.23 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: library/core/src/ptr/non_null.rs:969:39 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 179: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.24 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: library/core/src/ptr/non_null.rs:969:39 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 180: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.25 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: library/core/src/ptr/non_null.rs:970:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 181: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.26 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: library/core/src/ptr/non_null.rs:970:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 182: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.27 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: library/core/src/ptr/non_null.rs:970:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 183: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.28 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:970:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 184: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.29 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: library/core/src/ptr/non_null.rs:970:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 185: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.30 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: library/core/src/ptr/non_null.rs:970:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 186: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.31 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: library/core/src/ptr/non_null.rs:970:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 187: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.32 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: library/core/src/ptr/non_null.rs:970:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 188: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.33 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: library/core/src/ptr/non_null.rs:970:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 189: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.34 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:970:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 190: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.35 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: library/core/src/ptr/non_null.rs:970:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 191: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.36 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: library/core/src/ptr/non_null.rs:970:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 192: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.37 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: library/core/src/ptr/non_null.rs:971:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 193: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.38 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: library/core/src/ptr/non_null.rs:971:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 194: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.39 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: library/core/src/ptr/non_null.rs:971:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 195: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.40 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:971:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 196: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.41 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: library/core/src/ptr/non_null.rs:971:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 197: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.42 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: library/core/src/ptr/non_null.rs:971:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 198: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.43 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: library/core/src/ptr/non_null.rs:971:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 199: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.44 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: library/core/src/ptr/non_null.rs:971:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 200: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.45 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: library/core/src/ptr/non_null.rs:971:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 201: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.46 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:971:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 202: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.47 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: library/core/src/ptr/non_null.rs:971:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 203: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.48 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: library/core/src/ptr/non_null.rs:971:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 204: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.49 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: library/core/src/ptr/non_null.rs:971:51 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 205: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.50 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: library/core/src/ptr/non_null.rs:971:51 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 206: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.51 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: library/core/src/ptr/non_null.rs:971:51 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 207: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.52 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:971:51 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 208: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.53 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: library/core/src/ptr/non_null.rs:971:51 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 209: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.54 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: library/core/src/ptr/non_null.rs:971:51 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 210: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.55 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: library/core/src/ptr/non_null.rs:971:51 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 211: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.56 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: library/core/src/ptr/non_null.rs:971:51 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 212: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.57 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: library/core/src/ptr/non_null.rs:971:51 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 213: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.58 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:971:51 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 214: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.59 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: library/core/src/ptr/non_null.rs:971:51 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 215: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.60 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: library/core/src/ptr/non_null.rs:971:51 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 216: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.61 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: library/core/src/ptr/non_null.rs:974:22 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 217: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.62 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: library/core/src/ptr/non_null.rs:974:22 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 218: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.63 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: library/core/src/ptr/non_null.rs:974:22 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 219: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.64 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:974:22 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 220: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.65 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: library/core/src/ptr/non_null.rs:974:22 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 221: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.66 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: library/core/src/ptr/non_null.rs:974:22 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 222: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.67 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: library/core/src/ptr/non_null.rs:974:22 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 223: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.68 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: library/core/src/ptr/non_null.rs:974:22 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 224: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.69 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: library/core/src/ptr/non_null.rs:974:22 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 225: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.70 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:974:22 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 226: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.71 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: library/core/src/ptr/non_null.rs:974:22 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 227: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.72 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: library/core/src/ptr/non_null.rs:974:22 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 228: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.73 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 229: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.74 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 230: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.75 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 231: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.76 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 232: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.77 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 233: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.78 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 234: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.79 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 235: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.80 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 236: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.81 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 237: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.82 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 238: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.83 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 239: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.84 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 240: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.85 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 241: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.86 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 242: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.87 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 243: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.88 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 244: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.89 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 245: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.90 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 246: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.91 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: library/core/src/ptr/non_null.rs:972:15 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 247: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.92 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: library/core/src/ptr/non_null.rs:972:15 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 248: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.93 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: library/core/src/ptr/non_null.rs:972:15 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 249: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.94 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:972:15 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 250: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.95 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: library/core/src/ptr/non_null.rs:972:15 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 251: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.96 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: library/core/src/ptr/non_null.rs:972:15 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 252: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.97 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: library/core/src/ptr/non_null.rs:972:15 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 253: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.98 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: library/core/src/ptr/non_null.rs:972:15 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 254: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.99 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: library/core/src/ptr/non_null.rs:972:15 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 255: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.100 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:972:15 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 256: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.101 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: library/core/src/ptr/non_null.rs:972:15 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 257: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.102 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: library/core/src/ptr/non_null.rs:972:15 in function ptr::non_null::NonNull::::copy_to::{closure#2} + +Check 258: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: library/core/src/ptr/non_null.rs:980:28 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 259: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: library/core/src/ptr/non_null.rs:980:28 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 260: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: library/core/src/ptr/non_null.rs:980:28 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 261: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:980:28 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 262: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: library/core/src/ptr/non_null.rs:980:28 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 263: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: library/core/src/ptr/non_null.rs:980:28 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 264: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.7 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: library/core/src/ptr/non_null.rs:980:28 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 265: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.8 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: library/core/src/ptr/non_null.rs:980:28 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 266: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.9 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: library/core/src/ptr/non_null.rs:980:28 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 267: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.10 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:980:28 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 268: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.11 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: library/core/src/ptr/non_null.rs:980:28 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 269: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.12 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: library/core/src/ptr/non_null.rs:980:28 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 270: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.13 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: library/core/src/ptr/non_null.rs:980:42 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 271: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.14 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: library/core/src/ptr/non_null.rs:980:42 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 272: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.15 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: library/core/src/ptr/non_null.rs:980:42 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 273: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.16 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:980:42 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 274: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.17 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: library/core/src/ptr/non_null.rs:980:42 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 275: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.18 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: library/core/src/ptr/non_null.rs:980:42 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 276: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.19 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: library/core/src/ptr/non_null.rs:980:42 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 277: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.20 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: library/core/src/ptr/non_null.rs:980:42 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 278: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.21 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: library/core/src/ptr/non_null.rs:980:42 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 279: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.22 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:980:42 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 280: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.23 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: library/core/src/ptr/non_null.rs:980:42 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 281: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.24 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: library/core/src/ptr/non_null.rs:980:42 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 282: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.25 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: library/core/src/ptr/non_null.rs:980:57 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 283: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.26 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: library/core/src/ptr/non_null.rs:980:57 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 284: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.27 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: library/core/src/ptr/non_null.rs:980:57 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 285: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.28 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:980:57 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 286: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.29 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: library/core/src/ptr/non_null.rs:980:57 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 287: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.30 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: library/core/src/ptr/non_null.rs:980:57 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 288: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.31 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: library/core/src/ptr/non_null.rs:980:57 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 289: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.32 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: library/core/src/ptr/non_null.rs:980:57 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 290: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.33 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: library/core/src/ptr/non_null.rs:980:57 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 291: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.34 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:980:57 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 292: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.35 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: library/core/src/ptr/non_null.rs:980:57 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 293: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.36 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: library/core/src/ptr/non_null.rs:980:57 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} + +Check 294: fmt::Arguments::<'_>::new_const::<1>.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/fmt/mod.rs:342:34 in function fmt::Arguments::<'_>::new_const::<1> + +Check 295: <() as kani::mem::PtrProperties>::is_ptr_aligned.division-by-zero.1 + - Status: SUCCESS + - Description: "division by zero" + - Location: ../../kani/library/kani_core/src/mem.rs:220:17 in function <() as kani::mem::PtrProperties>::is_ptr_aligned + +Check 296: intrinsics::copy::.precondition_instance.1 + - Status: FAILURE + - Description: "memmove source region readable" + - Location: library/core/src/intrinsics.rs:3414:9 in function intrinsics::copy:: + +Check 297: intrinsics::copy::.precondition_instance.2 + - Status: FAILURE + - Description: "memmove destination region writeable" + - Location: library/core/src/intrinsics.rs:3414:9 in function intrinsics::copy:: + +Check 298: kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0}.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../kani/library/kani_core/src/arbitrary/pointer.rs:334:58 in function kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0} + +Check 299: kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0}.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../kani/library/kani_core/src/arbitrary/pointer.rs:334:58 in function kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0} + +Check 300: kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0}.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../kani/library/kani_core/src/arbitrary/pointer.rs:334:58 in function kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0} + +Check 301: kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0}.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../kani/library/kani_core/src/arbitrary/pointer.rs:334:58 in function kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0} + +Check 302: kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0}.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../kani/library/kani_core/src/arbitrary/pointer.rs:334:58 in function kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0} + +Check 303: kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0}.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../kani/library/kani_core/src/arbitrary/pointer.rs:334:58 in function kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0} + +Check 304: <() as kani::mem::PtrProperties>::is_ptr_aligned.division-by-zero.1 + - Status: SUCCESS + - Description: "division by zero" + - Location: ../../kani/library/kani_core/src/mem.rs:220:17 in function <() as kani::mem::PtrProperties>::is_ptr_aligned + +Check 305: option::Option::>::unwrap.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/option.rs:969:15 in function option::Option::>::unwrap + +Check 306: memcpy.pointer.1 + - Status: SUCCESS + - Description: "same object violation" + - Location: :33 in function memcpy + +Check 307: memcpy.pointer.2 + - Status: SUCCESS + - Description: "same object violation" + - Location: :34 in function memcpy + +Check 308: intrinsics::copy_nonoverlapping::.precondition_instance.1 + - Status: SUCCESS + - Description: "memcpy src/dst overlap" + - Location: library/core/src/intrinsics.rs:3308:14 in function intrinsics::copy_nonoverlapping:: + +Check 309: intrinsics::copy_nonoverlapping::.precondition_instance.2 + - Status: SUCCESS + - Description: "memcpy source region readable" + - Location: library/core/src/intrinsics.rs:3308:14 in function intrinsics::copy_nonoverlapping:: + +Check 310: intrinsics::copy_nonoverlapping::.precondition_instance.3 + - Status: SUCCESS + - Description: "memcpy destination region writeable" + - Location: library/core/src/intrinsics.rs:3308:14 in function intrinsics::copy_nonoverlapping:: + +Check 311: ptr::non_null::NonNull::::new.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: library/core/src/ptr/non_null.rs:236:13 in function ptr::non_null::NonNull::::new + + +SUMMARY: + ** 5 of 311 failed (4 unreachable) +Failed Checks: Check that array_replace((const void *)(char *)dest, ...) is allowed by the assigns clause + File: "", line 34, in memmove +Failed Checks: Kani does not support reasoning about pointer to unallocated memory + File: "/Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/lib.rs", line 421, in kani::mem::is_inbounds::<(), i32> +Failed Checks: attempt to compute offset which would overflow + File: "/Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/ptr/mut_ptr.rs", line 1037, in ptr::mut_ptr::::add +Failed Checks: memmove source region readable + File: "/Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/intrinsics.rs", line 3414, in intrinsics::copy:: +Failed Checks: memmove destination region writeable + File: "/Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/intrinsics.rs", line 3414, in intrinsics::copy:: + +VERIFICATION:- FAILED +Verification Time: 16.64629s + +Summary: +Verification failed for - ptr::non_null::verify::non_null_check_copy_to +Complete - 0 successfully verified harnesses, 1 failures, 1 total. From 2da2f7426cabe3f161d43ec7ddbec8b48e0bd0e6 Mon Sep 17 00:00:00 2001 From: Dhvani-Kapadia <159494547+Dhvani-Kapadia@users.noreply.github.com> Date: Wed, 13 Nov 2024 00:05:22 -0800 Subject: [PATCH 06/14] removing log files --- error.log | 50 -- verify-err.log | 0 verify-error.log | 1666 ---------------------------------------------- 3 files changed, 1716 deletions(-) delete mode 100644 error.log delete mode 100644 verify-err.log delete mode 100644 verify-error.log diff --git a/error.log b/error.log deleted file mode 100644 index c8749fe08bc0f..0000000000000 --- a/error.log +++ /dev/null @@ -1,50 +0,0 @@ -Kani Rust Verifier 0.56.0 (standalone) -error: expected `]`, found `&&` - --> /Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/ptr/non_null.rs:943:99 - | -173 | impl NonNull { - | - while parsing this item list starting here -... -943 | ub_checks::can_dereference(dest.as_ptr() as *const T, count * core::mem::size_of::())) &&//The pointer is valid for the specified number of ... - | ^^ expected `]` -... -1447 | } - | - the item list ends here - -error[E0599]: no method named `copy_to` found for struct `ptr::non_null::NonNull` in the current scope - --> /Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/ptr/non_null.rs:1846:13 - | -76 | pub struct NonNull { - | ----------------------------- method `copy_to` not found for this struct -... -1846 | src.copy_to(dest, count); - | ^^^^^^^ method not found in `NonNull` - | -help: one of the expressions' fields has a method of the same name - | -1846 | src.pointer.copy_to(dest, count); - | ++++++++ - -error[E0599]: no method named `copy_from` found for struct `ptr::non_null::NonNull` in the current scope - --> /Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/ptr/non_null.rs:1863:13 - | -76 | pub struct NonNull { - | ----------------------------- method `copy_from` not found for this struct -... -1863 | src.copy_from(dest, count); - | ^^^^^^^^^ - | -help: there is a method `clone_from` with a similar name, but with different arguments - --> /Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/clone.rs:174:5 - | -174 | fn clone_from(&mut self, source: &Self) { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -error[E0599]: no method named `is_aligned` found for reference `&ptr::non_null::NonNull` in the current scope - --> /Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/alloc/layout.rs:254:31 - | -254 | #[ensures(|result| result.is_aligned())] - | ^^^^^^^^^^ method not found in `&NonNull` - -For more information about this error, try `rustc --explain E0599`. -error: Failed to execute cargo (exit status: 101). Found 4 compilation errors. diff --git a/verify-err.log b/verify-err.log deleted file mode 100644 index e69de29bb2d1d..0000000000000 diff --git a/verify-error.log b/verify-error.log deleted file mode 100644 index ad556b12c3b78..0000000000000 --- a/verify-error.log +++ /dev/null @@ -1,1666 +0,0 @@ -Kani Rust Verifier 0.56.0 (standalone) -Checking harness ptr::non_null::verify::non_null_check_copy_to... -CBMC 6.3.1 (cbmc-6.3.1) -CBMC version 6.3.1 (cbmc-6.3.1) 64-bit x86_64 macos -Reading GOTO program from file /Users/dhvanikapadia/Downloads/verify-rust-std/target/kani_verify_std/target/x86_64-apple-darwin/debug/deps/core-ccf4fba8e5214364__RNvNtNtNtCsdg7tvWISkkD_4core3ptr8non_null6verify22non_null_check_copy_to.out -Generating GOTO Program -Adding CPROVER library (x86_64) -Removal of function pointers and virtual functions -Generic Property Instrumentation -Running with 16 object bits, 48 offset bits (user-specified) -Starting Bounded Model Checking -aborting path on assume(false) at file /Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/option.rs line 969 column 15 function option::Option::>::unwrap thread 0 -aborting path on assume(false) at file /Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/option.rs line 2008 column 5 function option::unwrap_failed thread 0 -aborting path on assume(false) at file /Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/option.rs line 971 column 21 function option::Option::>::unwrap thread 0 -aborting path on assume(false) at file /Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/option.rs line 969 column 15 function option::Option::>::unwrap thread 0 -aborting path on assume(false) at file /Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/option.rs line 2008 column 5 function option::unwrap_failed thread 0 -aborting path on assume(false) at file /Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/option.rs line 971 column 21 function option::Option::>::unwrap thread 0 -aborting path on assume(false) at file /Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/option.rs line 1170 column 15 function option::Option::::map_or:: thread 0 -Runtime Symex: 0.459842s -size of program expression: 5048 steps -slicing removed 2760 assignments -Generated 330 VCC(s), 120 remaining after simplification -Runtime Postprocess Equation: 0.00268161s -Passing problem to propositional reduction -converting SSA -Runtime Convert SSA: 5.77538s -Running propositional reduction -Post-processing -Runtime Post-process: 0.0196502s -Solving with CaDiCaL 2.0.0 -156266 variables, 8577118 clauses -SAT checker: instance is SATISFIABLE -Runtime Solver: 0.0463924s -Runtime decision procedure: 5.82464s -Running propositional reduction -Solving with CaDiCaL 2.0.0 -156267 variables, 8577119 clauses -SAT checker: instance is SATISFIABLE -Runtime Solver: 0.00402602s -Runtime decision procedure: 0.00508257s -Running propositional reduction -Solving with CaDiCaL 2.0.0 -156268 variables, 8577120 clauses -SAT checker: instance is SATISFIABLE -Runtime Solver: 0.00341336s -Runtime decision procedure: 0.00449741s -Running propositional reduction -Solving with CaDiCaL 2.0.0 -156269 variables, 8577121 clauses -SAT checker: instance is SATISFIABLE -Runtime Solver: 0.00315195s -Runtime decision procedure: 0.00423291s -Running propositional reduction -Solving with CaDiCaL 2.0.0 -156270 variables, 8577122 clauses -SAT checker: instance is SATISFIABLE -Runtime Solver: 0.0126685s -Runtime decision procedure: 0.0137506s -Running propositional reduction -Solving with CaDiCaL 2.0.0 -156271 variables, 8577123 clauses -SAT checker: instance is SATISFIABLE -Runtime Solver: 0.00569658s -Runtime decision procedure: 0.00677048s -Running propositional reduction -Solving with CaDiCaL 2.0.0 -156272 variables, 8577124 clauses -SAT checker: instance is SATISFIABLE -Runtime Solver: 0.00284245s -Runtime decision procedure: 0.003917s -Running propositional reduction -Solving with CaDiCaL 2.0.0 -156273 variables, 8577125 clauses -SAT checker: instance is SATISFIABLE -Runtime Solver: 0.00519012s -Runtime decision procedure: 0.00622863s -Running propositional reduction -Solving with CaDiCaL 2.0.0 -156274 variables, 8577126 clauses -SAT checker: instance is SATISFIABLE -Runtime Solver: 0.00217965s -Runtime decision procedure: 0.00321794s -Running propositional reduction -Solving with CaDiCaL 2.0.0 -156275 variables, 8577127 clauses -SAT checker: instance is UNSATISFIABLE -Runtime Solver: 0.0236761s -Runtime decision procedure: 0.02421s - -RESULTS: -Check 1: __CPROVER_contracts_write_set_check_assignment.assertion.1 - - Status: SUCCESS - - Description: "ptr NULL or writable up to size" - - Location: :775 in function __CPROVER_contracts_write_set_check_assignment - -Check 2: __CPROVER_contracts_write_set_check_assignment.assertion.2 - - Status: SUCCESS - - Description: "CAR size is less than __CPROVER_max_malloc_size" - - Location: :792 in function __CPROVER_contracts_write_set_check_assignment - -Check 3: __CPROVER_contracts_write_set_check_assignment.assertion.3 - - Status: SUCCESS - - Description: "no offset bits overflow on CAR upper bound computation" - - Location: :798 in function __CPROVER_contracts_write_set_check_assignment - -Check 4: __CPROVER_contracts_write_set_check_assignment.unwind.1 - - Status: SUCCESS - - Description: "unwinding assertion loop 0" - - Location: :807 in function __CPROVER_contracts_write_set_check_assignment - -Check 5: __CPROVER_contracts_write_set_check_assignment.assertion.4 - - Status: SUCCESS - - Description: "ptr NULL or writable up to size" - - Location: :775 in function __CPROVER_contracts_write_set_check_assignment - -Check 6: __CPROVER_contracts_write_set_check_assignment.assertion.5 - - Status: SUCCESS - - Description: "CAR size is less than __CPROVER_max_malloc_size" - - Location: :792 in function __CPROVER_contracts_write_set_check_assignment - -Check 7: __CPROVER_contracts_write_set_check_assignment.assertion.6 - - Status: SUCCESS - - Description: "no offset bits overflow on CAR upper bound computation" - - Location: :798 in function __CPROVER_contracts_write_set_check_assignment - -Check 8: __CPROVER_contracts_write_set_check_assignment.unwind.2 - - Status: SUCCESS - - Description: "unwinding assertion loop 0" - - Location: :807 in function __CPROVER_contracts_write_set_check_assignment - -Check 9: __CPROVER_contracts_car_set_insert.assertion.1 - - Status: SUCCESS - - Description: "ptr NULL or writable up to size" - - Location: :161 in function __CPROVER_contracts_car_set_insert - -Check 10: __CPROVER_contracts_car_set_insert.assertion.2 - - Status: SUCCESS - - Description: "CAR size is less than __CPROVER_max_malloc_size" - - Location: :164 in function __CPROVER_contracts_car_set_insert - -Check 11: __CPROVER_contracts_car_set_insert.assertion.3 - - Status: SUCCESS - - Description: "no offset bits overflow on CAR upper bound computation" - - Location: :168 in function __CPROVER_contracts_car_set_insert - -Check 12: memmove.assigns.1 - - Status: SUCCESS - - Description: "Check that array_copy((const void *)src_n, ...) is allowed by the assigns clause" - - Location: :33 in function memmove - -Check 13: memmove.assigns.2 - - Status: FAILURE - - Description: "Check that array_replace((const void *)(char *)dest, ...) is allowed by the assigns clause" - - Location: :34 in function memmove - -Check 14: panicking::panic_fmt.unsupported_construct.1 - - Status: SUCCESS - - Description: "call to foreign "Rust" function `rust_begin_unwind` is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/new/choose" - - Location: library/core/src/panicking.rs:64:9 in function panicking::panic_fmt - -Check 15: option::Option::>::unwrap.unreachable.1 - - Status: SUCCESS - - Description: "unreachable code" - - Location: library/core/src/option.rs:969:15 in function option::Option::>::unwrap - -Check 16: free.frees.1 - - Status: SUCCESS - - Description: "Check that ptr is freeable" - - Location: :43 in function free - -Check 17: memcpy.assigns.1 - - Status: SUCCESS - - Description: "Check that array_copy((const void *)src_n, ...) is allowed by the assigns clause" - - Location: :45 in function memcpy - -Check 18: memcpy.assigns.2 - - Status: SUCCESS - - Description: "Check that array_replace((const void *)(char *)dst, ...) is allowed by the assigns clause" - - Location: :46 in function memcpy - -Check 19: __CPROVER_contracts_write_set_record_deallocated.unwind.1 - - Status: SUCCESS - - Description: "unwinding assertion loop 0" - - Location: :710 in function __CPROVER_contracts_write_set_record_deallocated - -Check 20: ub_checks::is_nonoverlapping::runtime.unreachable.1 - - Status: SUCCESS - - Description: "unreachable code" - - Location: library/core/src/ub_checks.rs:146:5 in function ub_checks::is_nonoverlapping::runtime - -Check 21: <() as kani::mem::PtrProperties>::is_ptr_aligned.assertion.1 - - Status: SUCCESS - - Description: "attempt to calculate the remainder with a divisor of zero" - - Location: ../../kani/library/kani_core/src/mem.rs:220:17 in function <() as kani::mem::PtrProperties>::is_ptr_aligned - -Check 22: <() as kani::mem::PtrProperties>::is_ptr_aligned.arithmetic_overflow.1 - - Status: SUCCESS - - Description: "attempt to calculate the remainder with a divisor of zero" - - Location: ../../kani/library/kani_core/src/mem.rs:220:17 in function <() as kani::mem::PtrProperties>::is_ptr_aligned - -Check 23: ptr::mut_ptr::::add::runtime_add_nowrap::runtime.unreachable.1 - - Status: SUCCESS - - Description: "unreachable code" - - Location: library/core/src/ptr/mut_ptr.rs:1010:13 in function ptr::mut_ptr::::add::runtime_add_nowrap::runtime - -Check 24: __CPROVER_contracts_write_set_check_assignment.assertion.7 - - Status: SUCCESS - - Description: "ptr NULL or writable up to size" - - Location: :775 in function __CPROVER_contracts_write_set_check_assignment - -Check 25: __CPROVER_contracts_write_set_check_assignment.assertion.8 - - Status: SUCCESS - - Description: "CAR size is less than __CPROVER_max_malloc_size" - - Location: :792 in function __CPROVER_contracts_write_set_check_assignment - -Check 26: __CPROVER_contracts_write_set_check_assignment.assertion.9 - - Status: SUCCESS - - Description: "no offset bits overflow on CAR upper bound computation" - - Location: :798 in function __CPROVER_contracts_write_set_check_assignment - -Check 27: __CPROVER_contracts_write_set_check_assignment.unwind.3 - - Status: SUCCESS - - Description: "unwinding assertion loop 0" - - Location: :807 in function __CPROVER_contracts_write_set_check_assignment - -Check 28: <() as kani::mem::PtrProperties>::is_ptr_aligned.assertion.1 - - Status: SUCCESS - - Description: "attempt to calculate the remainder with a divisor of zero" - - Location: ../../kani/library/kani_core/src/mem.rs:220:17 in function <() as kani::mem::PtrProperties>::is_ptr_aligned - -Check 29: <() as kani::mem::PtrProperties>::is_ptr_aligned.arithmetic_overflow.1 - - Status: SUCCESS - - Description: "attempt to calculate the remainder with a divisor of zero" - - Location: ../../kani/library/kani_core/src/mem.rs:220:17 in function <() as kani::mem::PtrProperties>::is_ptr_aligned - -Check 30: option::Option::::map_or::.unreachable.1 - - Status: SUCCESS - - Description: "unreachable code" - - Location: library/core/src/option.rs:1170:15 in function option::Option::::map_or:: - -Check 31: kani::mem::is_inbounds::<(), u8>.assertion.1 - - Status: SUCCESS - - Description: "Kani does not support reasoning about pointer to unallocated memory" - - Location: library/core/src/lib.rs:421:1 in function kani::mem::is_inbounds::<(), u8> - -Check 32: kani::mem::assert_is_initialized::.assertion.1 - - Status: SUCCESS - - Description: "Undefined Behavior: Reading from an uninitialized pointer" - - Location: library/core/src/lib.rs:421:1 in function kani::mem::assert_is_initialized:: - -Check 33: ptr::mut_ptr::::add.arithmetic_overflow.1 - - Status: SUCCESS - - Description: "offset: attempt to compute number in bytes which would overflow" - - Location: library/core/src/ptr/mut_ptr.rs:1037:18 in function ptr::mut_ptr::::add - -Check 34: ptr::mut_ptr::::add.arithmetic_overflow.2 - - Status: SUCCESS - - Description: "attempt to compute offset which would overflow" - - Location: library/core/src/ptr/mut_ptr.rs:1037:18 in function ptr::mut_ptr::::add - -Check 35: fmt::Arguments::<'_>::new_const::<1>.assigns.1 - - Status: SUCCESS - - Description: "Check that *((unsigned char **)&temp_0) is assignable" - - Location: library/core/src/fmt/mod.rs:342:34 in function fmt::Arguments::<'_>::new_const::<1> - -Check 36: kani::mem::is_inbounds::<(), i32>.assertion.1 - - Status: FAILURE - - Description: "Kani does not support reasoning about pointer to unallocated memory" - - Location: library/core/src/lib.rs:421:1 in function kani::mem::is_inbounds::<(), i32> - -Check 37: >::copy_to::{closure#2}::{closure#2}.single_top_level_call.1 - - Status: SUCCESS - - Description: "Only a single top-level call to function _RNCNCNvMs1_NtNtCsdg7tvWISkkD_4core3ptr8non_nullINtB9_7NonNulllE7copy_tos0_0s0_0Bd_ when checking contract _RNCNCNvMs1_NtNtCsdg7tvWISkkD_4core3ptr8non_nullINtB9_7NonNulllE7copy_tos0_0s0_0Bd_" - - Location: library/core/src/ptr/non_null.rs:974:5 in function >::copy_to::{closure#2}::{closure#2} - -Check 38: >::copy_to::{closure#2}::{closure#2}.no_alloc_dealloc_in_requires.1 - - Status: SUCCESS - - Description: "Check that requires do not allocate or deallocate memory" - - Location: library/core/src/ptr/non_null.rs:974:5 in function >::copy_to::{closure#2}::{closure#2} - -Check 39: >::copy_to::{closure#2}::{closure#2}.no_alloc_dealloc_in_ensures.1 - - Status: SUCCESS - - Description: "Check that ensures do not allocate or deallocate memory" - - Location: library/core/src/ptr/non_null.rs:974:5 in function >::copy_to::{closure#2}::{closure#2} - -Check 40: >::copy_to::{closure#2}::{closure#2}.no_recursive_call.1 - - Status: SUCCESS - - Description: "No recursive call to function _RNCNCNvMs1_NtNtCsdg7tvWISkkD_4core3ptr8non_nullINtB9_7NonNulllE7copy_tos0_0s0_0Bd_ when checking contract _RNCNCNvMs1_NtNtCsdg7tvWISkkD_4core3ptr8non_nullINtB9_7NonNulllE7copy_tos0_0s0_0Bd_" - - Location: library/core/src/ptr/non_null.rs:974:5 in function >::copy_to::{closure#2}::{closure#2} - -Check 41: panic::location::Location::<'_>::caller.unsupported_construct.1 - - Status: SUCCESS - - Description: "caller_location is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/374" - - Location: library/core/src/panic/location.rs:89:9 in function panic::location::Location::<'_>::caller - -Check 42: ptr::non_null::NonNull::::copy_to::{closure#1}.unreachable.1 - - Status: SUCCESS - - Description: "unreachable code" - - Location: library/core/src/ptr/non_null.rs:968:5 in function ptr::non_null::NonNull::::copy_to::{closure#1} - -Check 43: ptr::non_null::NonNull::::new::{closure#2}.unreachable.1 - - Status: SUCCESS - - Description: "unreachable code" - - Location: library/core/src/ptr/non_null.rs:229:5 in function ptr::non_null::NonNull::::new::{closure#2} - -Check 44: ptr::non_null::NonNull::::new_unchecked::{closure#0}.unreachable.1 - - Status: SUCCESS - - Description: "unreachable code" - - Location: library/core/src/ptr/non_null.rs:198:5 in function ptr::non_null::NonNull::::new_unchecked::{closure#0} - -Check 45: kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0}.assertion.1 - - Status: SUCCESS - - Description: "attempt to subtract with overflow" - - Location: ../../kani/library/kani_core/src/arbitrary/pointer.rs:334:64 in function kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0} - -Check 46: ptr::non_null::NonNull::::new.assigns.1 - - Status: SUCCESS - - Description: "Check that *((unsigned char **)&temp_0) is assignable" - - Location: library/core/src/ptr/non_null.rs:236:13 in function ptr::non_null::NonNull::::new - -Check 47: num::::abs_diff.assertion.1 - - Status: UNREACHABLE - - Description: "attempt to subtract with overflow" - - Location: library/core/src/num/uint_macros.rs:2426:21 in function num::::abs_diff - -Check 48: num::::abs_diff.assertion.2 - - Status: UNREACHABLE - - Description: "attempt to subtract with overflow" - - Location: library/core/src/num/uint_macros.rs:2428:21 in function num::::abs_diff - -Check 49: ptr::mut_ptr::::add.arithmetic_overflow.1 - - Status: SUCCESS - - Description: "offset: attempt to compute number in bytes which would overflow" - - Location: library/core/src/ptr/mut_ptr.rs:1037:18 in function ptr::mut_ptr::::add - -Check 50: ptr::mut_ptr::::add.arithmetic_overflow.2 - - Status: FAILURE - - Description: "attempt to compute offset which would overflow" - - Location: library/core/src/ptr/mut_ptr.rs:1037:18 in function ptr::mut_ptr::::add - -Check 51: ptr::non_null::NonNull::::copy_to::{closure#2}.assertion.1 - - Status: SUCCESS - - Description: "|result: &()| ub_checks::can_dereference(self.as_ptr() as *const u8) && -ub_checks::can_dereference(dest.as_ptr() as *const u8)" - - Location: library/core/src/ptr/non_null.rs:972:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 52: kani::arbitrary_ptr::PointerGenerator::<16>::any_in_bounds::.assertion.1 - - Status: SUCCESS - - Description: "This is a placeholder message; Kani doesn't support message formatted at runtime" - - Location: library/core/src/lib.rs:421:1 in function kani::arbitrary_ptr::PointerGenerator::<16>::any_in_bounds:: - -Check 53: intrinsics::copy::.safety_check.1 - - Status: SUCCESS - - Description: "`src` must be properly aligned" - - Location: library/core/src/intrinsics.rs:3414:9 in function intrinsics::copy:: - -Check 54: intrinsics::copy::.safety_check.2 - - Status: SUCCESS - - Description: "`dst` must be properly aligned" - - Location: library/core/src/intrinsics.rs:3414:9 in function intrinsics::copy:: - -Check 55: intrinsics::copy::.arithmetic_overflow.1 - - Status: SUCCESS - - Description: "copy: attempt to compute number in bytes which would overflow" - - Location: library/core/src/intrinsics.rs:3414:9 in function intrinsics::copy:: - -Check 56: ptr::non_null::NonNull::::new_unchecked::{closure#1}.unreachable.1 - - Status: SUCCESS - - Description: "unreachable code" - - Location: library/core/src/ptr/non_null.rs:198:5 in function ptr::non_null::NonNull::::new_unchecked::{closure#1} - -Check 57: option::unwrap_failed.assertion.1 - - Status: SUCCESS - - Description: "called `Option::unwrap()` on a `None` value" - - Location: library/core/src/option.rs:2008:5 in function option::unwrap_failed - -Check 58: num::::abs.assertion.1 - - Status: UNREACHABLE - - Description: "attempt to negate with overflow" - - Location: library/core/src/num/int_macros.rs:3381:17 in function num::::abs - -Check 59: kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::.assertion.1 - - Status: SUCCESS - - Description: "This is a placeholder message; Kani doesn't support message formatted at runtime" - - Location: library/core/src/lib.rs:421:1 in function kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr:: - -Check 60: kani::mem::assert_is_initialized::>.assertion.1 - - Status: SUCCESS - - Description: "Undefined Behavior: Reading from an uninitialized pointer" - - Location: library/core/src/lib.rs:421:1 in function kani::mem::assert_is_initialized::> - -Check 61: ptr::non_null::NonNull::::new_unchecked::{closure#2}.unreachable.1 - - Status: SUCCESS - - Description: "unreachable code" - - Location: library/core/src/ptr/non_null.rs:198:5 in function ptr::non_null::NonNull::::new_unchecked::{closure#2} - -Check 62: ptr::non_null::NonNull::::copy_to::{closure#0}.unreachable.1 - - Status: SUCCESS - - Description: "unreachable code" - - Location: library/core/src/ptr/non_null.rs:968:5 in function ptr::non_null::NonNull::::copy_to::{closure#0} - -Check 63: ptr::const_ptr::::is_aligned_to.assertion.1 - - Status: SUCCESS - - Description: "This is a placeholder message; Kani doesn't support message formatted at runtime" - - Location: library/core/src/ptr/const_ptr.rs:1640:13 in function ptr::const_ptr::::is_aligned_to - -Check 64: <() as kani::mem::PtrProperties>>::is_ptr_aligned.assertion.1 - - Status: SUCCESS - - Description: "attempt to calculate the remainder with a divisor of zero" - - Location: ../../kani/library/kani_core/src/mem.rs:220:17 in function <() as kani::mem::PtrProperties>>::is_ptr_aligned - -Check 65: <() as kani::mem::PtrProperties>>::is_ptr_aligned.arithmetic_overflow.1 - - Status: SUCCESS - - Description: "attempt to calculate the remainder with a divisor of zero" - - Location: ../../kani/library/kani_core/src/mem.rs:220:17 in function <() as kani::mem::PtrProperties>>::is_ptr_aligned - -Check 66: ptr::const_ptr::::is_aligned_to::runtime_impl.assertion.1 - - Status: UNREACHABLE - - Description: "attempt to subtract with overflow" - - Location: library/core/src/ptr/const_ptr.rs:1645:26 in function ptr::const_ptr::::is_aligned_to::runtime_impl - -Check 67: ptr::non_null::NonNull::::new::{closure#0}.unreachable.1 - - Status: SUCCESS - - Description: "unreachable code" - - Location: library/core/src/ptr/non_null.rs:229:5 in function ptr::non_null::NonNull::::new::{closure#0} - -Check 68: intrinsics::copy_nonoverlapping::.safety_check.1 - - Status: SUCCESS - - Description: "`src` must be properly aligned" - - Location: library/core/src/intrinsics.rs:3308:14 in function intrinsics::copy_nonoverlapping:: - -Check 69: intrinsics::copy_nonoverlapping::.safety_check.2 - - Status: SUCCESS - - Description: "`dst` must be properly aligned" - - Location: library/core/src/intrinsics.rs:3308:14 in function intrinsics::copy_nonoverlapping:: - -Check 70: intrinsics::copy_nonoverlapping::.arithmetic_overflow.1 - - Status: SUCCESS - - Description: "copy_nonoverlapping: attempt to compute number in bytes which would overflow" - - Location: library/core/src/intrinsics.rs:3308:14 in function intrinsics::copy_nonoverlapping:: - -Check 71: ptr::non_null::NonNull::::new::{closure#1}.unreachable.1 - - Status: SUCCESS - - Description: "unreachable code" - - Location: library/core/src/ptr/non_null.rs:229:5 in function ptr::non_null::NonNull::::new::{closure#1} - -Check 72: kani::mem::is_inbounds::<(), mem::maybe_uninit::MaybeUninit>.assertion.1 - - Status: SUCCESS - - Description: "Kani does not support reasoning about pointer to unallocated memory" - - Location: library/core/src/lib.rs:421:1 in function kani::mem::is_inbounds::<(), mem::maybe_uninit::MaybeUninit> - -Check 73: __sincospi.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:685 in function __sincospi - -Check 74: __sincospi.pointer_dereference.2 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:685 in function __sincospi - -Check 75: __sincospi.pointer_dereference.3 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:685 in function __sincospi - -Check 76: __sincospi.pointer_dereference.4 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:685 in function __sincospi - -Check 77: __sincospi.pointer_dereference.5 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:685 in function __sincospi - -Check 78: __sincospi.pointer_dereference.6 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:685 in function __sincospi - -Check 79: __sincospi.pointer_dereference.7 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:685 in function __sincospi - -Check 80: __sincospi.pointer_dereference.8 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:685 in function __sincospi - -Check 81: __sincospi.pointer_dereference.9 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:685 in function __sincospi - -Check 82: __sincospi.pointer_dereference.10 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:685 in function __sincospi - -Check 83: __sincospi.pointer_dereference.11 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:685 in function __sincospi - -Check 84: __sincospi.pointer_dereference.12 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:685 in function __sincospi - -Check 85: __sincos.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:675 in function __sincos - -Check 86: __sincos.pointer_dereference.2 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:675 in function __sincos - -Check 87: __sincos.pointer_dereference.3 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:675 in function __sincos - -Check 88: __sincos.pointer_dereference.4 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:675 in function __sincos - -Check 89: __sincos.pointer_dereference.5 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:675 in function __sincos - -Check 90: __sincos.pointer_dereference.6 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:675 in function __sincos - -Check 91: __sincos.pointer_dereference.7 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:675 in function __sincos - -Check 92: __sincos.pointer_dereference.8 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:675 in function __sincos - -Check 93: __sincos.pointer_dereference.9 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:675 in function __sincos - -Check 94: __sincos.pointer_dereference.10 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:675 in function __sincos - -Check 95: __sincos.pointer_dereference.11 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:675 in function __sincos - -Check 96: __sincos.pointer_dereference.12 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:675 in function __sincos - -Check 97: __sincospif.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:680 in function __sincospif - -Check 98: __sincospif.pointer_dereference.2 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:680 in function __sincospif - -Check 99: __sincospif.pointer_dereference.3 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:680 in function __sincospif - -Check 100: __sincospif.pointer_dereference.4 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:680 in function __sincospif - -Check 101: __sincospif.pointer_dereference.5 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:680 in function __sincospif - -Check 102: __sincospif.pointer_dereference.6 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:680 in function __sincospif - -Check 103: __sincospif.pointer_dereference.7 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:680 in function __sincospif - -Check 104: __sincospif.pointer_dereference.8 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:680 in function __sincospif - -Check 105: __sincospif.pointer_dereference.9 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:680 in function __sincospif - -Check 106: __sincospif.pointer_dereference.10 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:680 in function __sincospif - -Check 107: __sincospif.pointer_dereference.11 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:680 in function __sincospif - -Check 108: __sincospif.pointer_dereference.12 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:680 in function __sincospif - -Check 109: __sincosf.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:670 in function __sincosf - -Check 110: __sincosf.pointer_dereference.2 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:670 in function __sincosf - -Check 111: __sincosf.pointer_dereference.3 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:670 in function __sincosf - -Check 112: __sincosf.pointer_dereference.4 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:670 in function __sincosf - -Check 113: __sincosf.pointer_dereference.5 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:670 in function __sincosf - -Check 114: __sincosf.pointer_dereference.6 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:670 in function __sincosf - -Check 115: __sincosf.pointer_dereference.7 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:670 in function __sincosf - -Check 116: __sincosf.pointer_dereference.8 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:670 in function __sincosf - -Check 117: __sincosf.pointer_dereference.9 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:670 in function __sincosf - -Check 118: __sincosf.pointer_dereference.10 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:670 in function __sincosf - -Check 119: __sincosf.pointer_dereference.11 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:670 in function __sincosf - -Check 120: __sincosf.pointer_dereference.12 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/math.h:670 in function __sincosf - -Check 121: __CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.1 - - Status: SUCCESS - - Description: "count leading zeros is undefined for value zero" - - Location: :251 in function __CPROVER_contracts_obj_set_create_indexed_by_object_id - -Check 122: ptr::non_null::verify::non_null_check_copy_to.precondition_instance.1 - - Status: SUCCESS - - Description: "free argument must be NULL or valid pointer" - - Location: library/core/src/ptr/non_null.rs:1884:5 in function ptr::non_null::verify::non_null_check_copy_to - -Check 123: ptr::non_null::verify::non_null_check_copy_to.precondition_instance.2 - - Status: SUCCESS - - Description: "free argument must be dynamic object" - - Location: library/core/src/ptr/non_null.rs:1884:5 in function ptr::non_null::verify::non_null_check_copy_to - -Check 124: ptr::non_null::verify::non_null_check_copy_to.precondition_instance.3 - - Status: SUCCESS - - Description: "free argument has offset zero" - - Location: library/core/src/ptr/non_null.rs:1884:5 in function ptr::non_null::verify::non_null_check_copy_to - -Check 125: ptr::non_null::verify::non_null_check_copy_to.precondition_instance.4 - - Status: SUCCESS - - Description: "double free" - - Location: library/core/src/ptr/non_null.rs:1884:5 in function ptr::non_null::verify::non_null_check_copy_to - -Check 126: ptr::non_null::verify::non_null_check_copy_to.precondition_instance.5 - - Status: SUCCESS - - Description: "free called for new[] object" - - Location: library/core/src/ptr/non_null.rs:1884:5 in function ptr::non_null::verify::non_null_check_copy_to - -Check 127: ptr::non_null::verify::non_null_check_copy_to.precondition_instance.6 - - Status: SUCCESS - - Description: "free called for stack-allocated object" - - Location: library/core/src/ptr/non_null.rs:1884:5 in function ptr::non_null::verify::non_null_check_copy_to - -Check 128: <() as kani::mem::PtrProperties>>::is_ptr_aligned.division-by-zero.1 - - Status: SUCCESS - - Description: "division by zero" - - Location: ../../kani/library/kani_core/src/mem.rs:220:17 in function <() as kani::mem::PtrProperties>>::is_ptr_aligned - -Check 129: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: library/core/src/ptr/non_null.rs:972:56 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} - -Check 130: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.2 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: library/core/src/ptr/non_null.rs:972:56 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} - -Check 131: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.3 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: library/core/src/ptr/non_null.rs:972:56 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} - -Check 132: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.4 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:972:56 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} - -Check 133: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.5 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: library/core/src/ptr/non_null.rs:972:56 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} - -Check 134: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.6 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: library/core/src/ptr/non_null.rs:972:56 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} - -Check 135: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.7 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: library/core/src/ptr/non_null.rs:972:56 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} - -Check 136: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.8 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: library/core/src/ptr/non_null.rs:972:56 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} - -Check 137: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.9 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: library/core/src/ptr/non_null.rs:972:56 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} - -Check 138: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.10 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:972:56 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} - -Check 139: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.11 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: library/core/src/ptr/non_null.rs:972:56 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} - -Check 140: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.12 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: library/core/src/ptr/non_null.rs:972:56 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} - -Check 141: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.13 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: library/core/src/ptr/non_null.rs:973:39 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} - -Check 142: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.14 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: library/core/src/ptr/non_null.rs:973:39 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} - -Check 143: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.15 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: library/core/src/ptr/non_null.rs:973:39 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} - -Check 144: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.16 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:973:39 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} - -Check 145: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.17 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: library/core/src/ptr/non_null.rs:973:39 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} - -Check 146: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.18 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: library/core/src/ptr/non_null.rs:973:39 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} - -Check 147: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.19 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: library/core/src/ptr/non_null.rs:973:39 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} - -Check 148: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.20 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: library/core/src/ptr/non_null.rs:973:39 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} - -Check 149: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.21 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: library/core/src/ptr/non_null.rs:973:39 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} - -Check 150: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.22 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:973:39 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} - -Check 151: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.23 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: library/core/src/ptr/non_null.rs:973:39 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} - -Check 152: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1}.pointer_dereference.24 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: library/core/src/ptr/non_null.rs:973:39 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#1} - -Check 153: __CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.2 - - Status: SUCCESS - - Description: "count leading zeros is undefined for value zero" - - Location: :251 in function __CPROVER_contracts_obj_set_create_indexed_by_object_id - -Check 154: __CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.3 - - Status: SUCCESS - - Description: "count leading zeros is undefined for value zero" - - Location: :251 in function __CPROVER_contracts_obj_set_create_indexed_by_object_id - -Check 155: __CPROVER_contracts_obj_set_create_indexed_by_object_id.bit_count.4 - - Status: SUCCESS - - Description: "count leading zeros is undefined for value zero" - - Location: :251 in function __CPROVER_contracts_obj_set_create_indexed_by_object_id - -Check 156: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: library/core/src/ptr/non_null.rs:968:16 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 157: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.2 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: library/core/src/ptr/non_null.rs:968:16 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 158: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.3 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: library/core/src/ptr/non_null.rs:968:16 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 159: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.4 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:968:16 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 160: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.5 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: library/core/src/ptr/non_null.rs:968:16 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 161: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.6 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: library/core/src/ptr/non_null.rs:968:16 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 162: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.7 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: library/core/src/ptr/non_null.rs:968:16 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 163: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.8 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: library/core/src/ptr/non_null.rs:968:16 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 164: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.9 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: library/core/src/ptr/non_null.rs:968:16 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 165: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.10 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:968:16 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 166: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.11 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: library/core/src/ptr/non_null.rs:968:16 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 167: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.12 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: library/core/src/ptr/non_null.rs:968:16 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 168: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.13 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: library/core/src/ptr/non_null.rs:969:39 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 169: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.14 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: library/core/src/ptr/non_null.rs:969:39 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 170: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.15 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: library/core/src/ptr/non_null.rs:969:39 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 171: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.16 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:969:39 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 172: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.17 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: library/core/src/ptr/non_null.rs:969:39 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 173: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.18 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: library/core/src/ptr/non_null.rs:969:39 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 174: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.19 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: library/core/src/ptr/non_null.rs:969:39 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 175: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.20 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: library/core/src/ptr/non_null.rs:969:39 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 176: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.21 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: library/core/src/ptr/non_null.rs:969:39 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 177: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.22 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:969:39 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 178: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.23 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: library/core/src/ptr/non_null.rs:969:39 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 179: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.24 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: library/core/src/ptr/non_null.rs:969:39 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 180: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.25 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: library/core/src/ptr/non_null.rs:970:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 181: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.26 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: library/core/src/ptr/non_null.rs:970:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 182: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.27 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: library/core/src/ptr/non_null.rs:970:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 183: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.28 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:970:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 184: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.29 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: library/core/src/ptr/non_null.rs:970:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 185: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.30 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: library/core/src/ptr/non_null.rs:970:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 186: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.31 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: library/core/src/ptr/non_null.rs:970:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 187: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.32 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: library/core/src/ptr/non_null.rs:970:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 188: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.33 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: library/core/src/ptr/non_null.rs:970:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 189: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.34 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:970:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 190: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.35 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: library/core/src/ptr/non_null.rs:970:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 191: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.36 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: library/core/src/ptr/non_null.rs:970:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 192: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.37 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: library/core/src/ptr/non_null.rs:971:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 193: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.38 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: library/core/src/ptr/non_null.rs:971:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 194: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.39 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: library/core/src/ptr/non_null.rs:971:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 195: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.40 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:971:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 196: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.41 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: library/core/src/ptr/non_null.rs:971:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 197: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.42 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: library/core/src/ptr/non_null.rs:971:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 198: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.43 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: library/core/src/ptr/non_null.rs:971:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 199: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.44 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: library/core/src/ptr/non_null.rs:971:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 200: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.45 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: library/core/src/ptr/non_null.rs:971:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 201: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.46 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:971:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 202: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.47 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: library/core/src/ptr/non_null.rs:971:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 203: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.48 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: library/core/src/ptr/non_null.rs:971:33 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 204: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.49 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: library/core/src/ptr/non_null.rs:971:51 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 205: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.50 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: library/core/src/ptr/non_null.rs:971:51 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 206: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.51 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: library/core/src/ptr/non_null.rs:971:51 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 207: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.52 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:971:51 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 208: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.53 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: library/core/src/ptr/non_null.rs:971:51 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 209: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.54 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: library/core/src/ptr/non_null.rs:971:51 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 210: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.55 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: library/core/src/ptr/non_null.rs:971:51 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 211: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.56 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: library/core/src/ptr/non_null.rs:971:51 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 212: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.57 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: library/core/src/ptr/non_null.rs:971:51 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 213: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.58 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:971:51 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 214: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.59 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: library/core/src/ptr/non_null.rs:971:51 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 215: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.60 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: library/core/src/ptr/non_null.rs:971:51 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 216: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.61 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: library/core/src/ptr/non_null.rs:974:22 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 217: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.62 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: library/core/src/ptr/non_null.rs:974:22 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 218: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.63 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: library/core/src/ptr/non_null.rs:974:22 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 219: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.64 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:974:22 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 220: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.65 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: library/core/src/ptr/non_null.rs:974:22 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 221: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.66 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: library/core/src/ptr/non_null.rs:974:22 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 222: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.67 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: library/core/src/ptr/non_null.rs:974:22 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 223: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.68 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: library/core/src/ptr/non_null.rs:974:22 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 224: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.69 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: library/core/src/ptr/non_null.rs:974:22 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 225: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.70 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:974:22 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 226: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.71 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: library/core/src/ptr/non_null.rs:974:22 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 227: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.72 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: library/core/src/ptr/non_null.rs:974:22 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 228: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.73 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 229: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.74 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 230: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.75 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 231: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.76 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 232: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.77 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 233: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.78 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 234: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.79 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 235: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.80 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 236: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.81 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 237: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.82 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 238: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.83 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 239: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.84 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 240: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.85 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 241: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.86 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 242: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.87 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 243: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.88 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 244: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.89 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 245: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.90 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: library/core/src/ptr/non_null.rs:974:5 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 246: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.91 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: library/core/src/ptr/non_null.rs:972:15 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 247: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.92 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: library/core/src/ptr/non_null.rs:972:15 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 248: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.93 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: library/core/src/ptr/non_null.rs:972:15 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 249: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.94 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:972:15 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 250: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.95 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: library/core/src/ptr/non_null.rs:972:15 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 251: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.96 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: library/core/src/ptr/non_null.rs:972:15 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 252: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.97 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: library/core/src/ptr/non_null.rs:972:15 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 253: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.98 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: library/core/src/ptr/non_null.rs:972:15 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 254: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.99 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: library/core/src/ptr/non_null.rs:972:15 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 255: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.100 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:972:15 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 256: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.101 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: library/core/src/ptr/non_null.rs:972:15 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 257: ptr::non_null::NonNull::::copy_to::{closure#2}.pointer_dereference.102 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: library/core/src/ptr/non_null.rs:972:15 in function ptr::non_null::NonNull::::copy_to::{closure#2} - -Check 258: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: library/core/src/ptr/non_null.rs:980:28 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 259: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.2 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: library/core/src/ptr/non_null.rs:980:28 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 260: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.3 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: library/core/src/ptr/non_null.rs:980:28 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 261: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.4 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:980:28 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 262: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.5 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: library/core/src/ptr/non_null.rs:980:28 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 263: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.6 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: library/core/src/ptr/non_null.rs:980:28 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 264: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.7 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: library/core/src/ptr/non_null.rs:980:28 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 265: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.8 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: library/core/src/ptr/non_null.rs:980:28 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 266: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.9 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: library/core/src/ptr/non_null.rs:980:28 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 267: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.10 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:980:28 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 268: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.11 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: library/core/src/ptr/non_null.rs:980:28 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 269: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.12 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: library/core/src/ptr/non_null.rs:980:28 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 270: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.13 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: library/core/src/ptr/non_null.rs:980:42 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 271: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.14 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: library/core/src/ptr/non_null.rs:980:42 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 272: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.15 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: library/core/src/ptr/non_null.rs:980:42 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 273: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.16 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:980:42 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 274: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.17 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: library/core/src/ptr/non_null.rs:980:42 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 275: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.18 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: library/core/src/ptr/non_null.rs:980:42 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 276: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.19 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: library/core/src/ptr/non_null.rs:980:42 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 277: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.20 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: library/core/src/ptr/non_null.rs:980:42 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 278: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.21 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: library/core/src/ptr/non_null.rs:980:42 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 279: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.22 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:980:42 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 280: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.23 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: library/core/src/ptr/non_null.rs:980:42 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 281: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.24 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: library/core/src/ptr/non_null.rs:980:42 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 282: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.25 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: library/core/src/ptr/non_null.rs:980:57 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 283: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.26 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: library/core/src/ptr/non_null.rs:980:57 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 284: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.27 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: library/core/src/ptr/non_null.rs:980:57 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 285: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.28 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:980:57 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 286: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.29 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: library/core/src/ptr/non_null.rs:980:57 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 287: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.30 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: library/core/src/ptr/non_null.rs:980:57 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 288: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.31 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: library/core/src/ptr/non_null.rs:980:57 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 289: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.32 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: library/core/src/ptr/non_null.rs:980:57 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 290: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.33 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: library/core/src/ptr/non_null.rs:980:57 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 291: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.34 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:980:57 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 292: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.35 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: library/core/src/ptr/non_null.rs:980:57 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 293: ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2}.pointer_dereference.36 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: library/core/src/ptr/non_null.rs:980:57 in function ptr::non_null::NonNull::::copy_to::{closure#2}::{closure#2} - -Check 294: fmt::Arguments::<'_>::new_const::<1>.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/fmt/mod.rs:342:34 in function fmt::Arguments::<'_>::new_const::<1> - -Check 295: <() as kani::mem::PtrProperties>::is_ptr_aligned.division-by-zero.1 - - Status: SUCCESS - - Description: "division by zero" - - Location: ../../kani/library/kani_core/src/mem.rs:220:17 in function <() as kani::mem::PtrProperties>::is_ptr_aligned - -Check 296: intrinsics::copy::.precondition_instance.1 - - Status: FAILURE - - Description: "memmove source region readable" - - Location: library/core/src/intrinsics.rs:3414:9 in function intrinsics::copy:: - -Check 297: intrinsics::copy::.precondition_instance.2 - - Status: FAILURE - - Description: "memmove destination region writeable" - - Location: library/core/src/intrinsics.rs:3414:9 in function intrinsics::copy:: - -Check 298: kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0}.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../kani/library/kani_core/src/arbitrary/pointer.rs:334:58 in function kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0} - -Check 299: kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0}.pointer_dereference.2 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../kani/library/kani_core/src/arbitrary/pointer.rs:334:58 in function kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0} - -Check 300: kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0}.pointer_dereference.3 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../kani/library/kani_core/src/arbitrary/pointer.rs:334:58 in function kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0} - -Check 301: kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0}.pointer_dereference.4 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../kani/library/kani_core/src/arbitrary/pointer.rs:334:58 in function kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0} - -Check 302: kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0}.pointer_dereference.5 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../kani/library/kani_core/src/arbitrary/pointer.rs:334:58 in function kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0} - -Check 303: kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0}.pointer_dereference.6 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../kani/library/kani_core/src/arbitrary/pointer.rs:334:58 in function kani::arbitrary_ptr::PointerGenerator::<16>::create_in_bounds_ptr::::{closure#0} - -Check 304: <() as kani::mem::PtrProperties>::is_ptr_aligned.division-by-zero.1 - - Status: SUCCESS - - Description: "division by zero" - - Location: ../../kani/library/kani_core/src/mem.rs:220:17 in function <() as kani::mem::PtrProperties>::is_ptr_aligned - -Check 305: option::Option::>::unwrap.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/option.rs:969:15 in function option::Option::>::unwrap - -Check 306: memcpy.pointer.1 - - Status: SUCCESS - - Description: "same object violation" - - Location: :33 in function memcpy - -Check 307: memcpy.pointer.2 - - Status: SUCCESS - - Description: "same object violation" - - Location: :34 in function memcpy - -Check 308: intrinsics::copy_nonoverlapping::.precondition_instance.1 - - Status: SUCCESS - - Description: "memcpy src/dst overlap" - - Location: library/core/src/intrinsics.rs:3308:14 in function intrinsics::copy_nonoverlapping:: - -Check 309: intrinsics::copy_nonoverlapping::.precondition_instance.2 - - Status: SUCCESS - - Description: "memcpy source region readable" - - Location: library/core/src/intrinsics.rs:3308:14 in function intrinsics::copy_nonoverlapping:: - -Check 310: intrinsics::copy_nonoverlapping::.precondition_instance.3 - - Status: SUCCESS - - Description: "memcpy destination region writeable" - - Location: library/core/src/intrinsics.rs:3308:14 in function intrinsics::copy_nonoverlapping:: - -Check 311: ptr::non_null::NonNull::::new.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: library/core/src/ptr/non_null.rs:236:13 in function ptr::non_null::NonNull::::new - - -SUMMARY: - ** 5 of 311 failed (4 unreachable) -Failed Checks: Check that array_replace((const void *)(char *)dest, ...) is allowed by the assigns clause - File: "", line 34, in memmove -Failed Checks: Kani does not support reasoning about pointer to unallocated memory - File: "/Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/lib.rs", line 421, in kani::mem::is_inbounds::<(), i32> -Failed Checks: attempt to compute offset which would overflow - File: "/Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/ptr/mut_ptr.rs", line 1037, in ptr::mut_ptr::::add -Failed Checks: memmove source region readable - File: "/Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/intrinsics.rs", line 3414, in intrinsics::copy:: -Failed Checks: memmove destination region writeable - File: "/Users/dhvanikapadia/Downloads/verify-rust-std/library/core/src/intrinsics.rs", line 3414, in intrinsics::copy:: - -VERIFICATION:- FAILED -Verification Time: 16.64629s - -Summary: -Verification failed for - ptr::non_null::verify::non_null_check_copy_to -Complete - 0 successfully verified harnesses, 1 failures, 1 total. From 57cc963f5762b7b5df383d4b6dd0035e04ed8b59 Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Wed, 4 Dec 2024 15:26:45 -0800 Subject: [PATCH 07/14] resolve copy_to failed checks, modify contract to refer to entire slice --- library/core/src/ptr/non_null.rs | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index fe8bc13bbeac7..594bf44b15f35 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1018,12 +1018,11 @@ impl NonNull { #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "const_intrinsic_copy", since = "1.83.0")] #[requires(count.checked_mul(core::mem::size_of::()).map_or(false, |size| size <= isize::MAX as usize) - && ub_checks::can_dereference(self.as_ptr() as *const MaybeUninit) - && ub_checks::can_write(dest.as_ptr()) - && ub_checks::can_write(dest.as_ptr().add(count)))] + && ub_checks::can_dereference(NonNull::slice_from_raw_parts(self, count).as_ptr()) + && ub_checks::can_write(NonNull::slice_from_raw_parts(dest, count).as_ptr()))] #[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr() as *const u8) && ub_checks::can_dereference(dest.as_ptr() as *const u8))] - #[kani::modifies(dest.as_ptr())] + #[kani::modifies(NonNull::slice_from_raw_parts(dest, count).as_ptr())] pub const unsafe fn copy_to(self, dest: NonNull, count: usize) where T: Sized, From 4c9fdfaacd66e6f4007f9b0fa3743e684267adaf Mon Sep 17 00:00:00 2001 From: Dhvani-Kapadia <159494547+Dhvani-Kapadia@users.noreply.github.com> Date: Wed, 4 Dec 2024 23:28:51 -0800 Subject: [PATCH 08/14] updating all contrac ts --- library/core/src/ptr/non_null.rs | 111 +++++++++++++++---------------- 1 file changed, 52 insertions(+), 59 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 594bf44b15f35..353ec44999302 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1044,13 +1044,12 @@ impl NonNull { #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "const_intrinsic_copy", since = "1.83.0")] #[requires(count.checked_mul(core::mem::size_of::()).map_or(false, |size| size <= isize::MAX as usize) - && ub_checks::can_dereference(self.as_ptr() as *const MaybeUninit) - && ub_checks::can_write(dest.as_ptr()) - && ub_checks::can_write(dest.as_ptr().add(count)) + && ub_checks::can_dereference(NonNull::slice_from_raw_parts(self, count).as_ptr()) + && ub_checks::can_write(NonNull::slice_from_raw_parts(dest, count).as_ptr()) && (self.as_ptr() as usize).abs_diff(dest.as_ptr() as usize) >= count * core::mem::size_of::())] #[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr() as *const u8) && ub_checks::can_dereference(dest.as_ptr() as *const u8))] - #[kani::modifies(dest.as_ptr())] + #[kani::modifies(NonNull::slice_from_raw_parts(dest, count).as_ptr())] pub const unsafe fn copy_to_nonoverlapping(self, dest: NonNull, count: usize) where T: Sized, @@ -1071,14 +1070,12 @@ impl NonNull { #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "const_intrinsic_copy", since = "1.83.0")] - #[requires (count.checked_mul(core::mem::size_of::()).map_or(false, |size| size <= isize::MAX as usize - && ub_checks::can_dereference(src.as_ptr() as *const MaybeUninit) - && ub_checks::can_write(self.as_ptr()) - && ub_checks::can_write (self.as_ptr().add(count))) - && (src.as_ptr() as usize).abs_diff(self.as_ptr() as usize) >= count * core::mem::size_of::())] - #[ensures (|result: &()| ub_checks::can_dereference(src.as_ptr() as *const u8) - && ub_checks::can_dereference(self.as_ptr()))] - #[kani::modifies(self.as_ptr())] + #[requires(count.checked_mul(core::mem::size_of::()).map_or(false, |size| size <= isize::MAX as usize) + && ub_checks::can_dereference(NonNull::slice_from_raw_parts(src, count).as_ptr()) + && ub_checks::can_write(NonNull::slice_from_raw_parts(self, count).as_ptr()))] + #[ensures(|result: &()| ub_checks::can_dereference(src.as_ptr() as *const u8) + && ub_checks::can_dereference(self.as_ptr() as *const u8))] + #[kani::modifies(NonNull::slice_from_raw_parts(self, count).as_ptr())] pub const unsafe fn copy_from(self, src: NonNull, count: usize) where T: Sized, @@ -1099,14 +1096,13 @@ impl NonNull { #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "const_intrinsic_copy", since = "1.83.0")] - #[requires (count.checked_mul(core::mem::size_of::()).map_or(false, |size| size <= isize::MAX as usize - && ub_checks::can_dereference(src.as_ptr() as *const MaybeUninit) - && ub_checks::can_write(self.as_ptr()) - && ub_checks::can_write(self.as_ptr().add(count))) - && (self.as_ptr() as usize).abs_diff(src.as_ptr() as usize) >= count * core::mem::size_of::())]//The source and destination regions do not overlap. - #[ensures (|result: &()| ub_checks::can_dereference(src.as_ptr() as *const u8) - && ub_checks::can_dereference(self.as_ptr()))] - #[kani::modifies(self.as_ptr())] + #[requires(count.checked_mul(core::mem::size_of::()).map_or(false, |size| size <= isize::MAX as usize) + && ub_checks::can_dereference(NonNull::slice_from_raw_parts(src, count).as_ptr()) + && ub_checks::can_write(NonNull::slice_from_raw_parts(self, count).as_ptr()) + && (self.as_ptr() as usize).abs_diff(dest.as_ptr() as usize) >= count * core::mem::size_of::())] + #[ensures(|result: &()| ub_checks::can_dereference(src.as_ptr() as *const u8) + && ub_checks::can_dereference(self.as_ptr() as *const u8))] + #[kani::modifies(NonNull::slice_from_raw_parts(self, count).as_ptr())] pub const unsafe fn copy_from_nonoverlapping(self, src: NonNull, count: usize) where T: Sized, @@ -2475,51 +2471,48 @@ mod verify { // Generate an arbitrary count using kani::any let count: usize = kani::any(); unsafe { src.copy_to(dest, count);} -} + } #[kani::proof_for_contract(NonNull::::copy_from)] pub fn non_null_check_copy_from() { - // Create source and destination values - let mut src_value: i32 = kani::any(); - let mut dest_value: i32 = 0; - - // Create NonNull pointers - let src = NonNull::new(&mut src_value as *mut i32).unwrap(); - let dest = NonNull::new(&mut dest_value as *mut i32).unwrap(); - - //count is 1 as working with single i32 value - let count = 1; - unsafe { - src.copy_from(dest, count); - } + // PointerGenerator instance + let mut generator = PointerGenerator::<16>::new(); + // Generate arbitrary pointers for src and dest + let src_ptr = generator.any_in_bounds::().ptr; + let dest_ptr = generator.any_in_bounds::().ptr; + // Wrap the raw pointers in NonNull + let src = NonNull::new(src_ptr).unwrap(); + let dest = NonNull::new(dest_ptr).unwrap(); + // Generate an arbitrary count using kani::any + let count: usize = kani::any(); + unsafe { src.copy_from(dest, count);} } #[kani::proof_for_contract(NonNull::::copy_to_nonoverlapping)] pub fn non_null_check_copy_to_nonoverlapping() { - let mut src_value: i32 = kani::any(); - let mut dest_value: i32 = 0; - - let src = NonNull::new(&mut src_value as *mut i32).unwrap(); - let dest = NonNull::new(&mut dest_value as *mut i32).unwrap(); - - //count represents no of elements to copy - let count = 1; - unsafe { - src.copy_to_nonoverlapping(dest, count); - } + // PointerGenerator instance + let mut generator = PointerGenerator::<16>::new(); + // Generate arbitrary pointers for src and dest + let src_ptr = generator.any_in_bounds::().ptr; + let dest_ptr = generator.any_in_bounds::().ptr; + // Wrap the raw pointers in NonNull + let src = NonNull::new(src_ptr).unwrap(); + let dest = NonNull::new(dest_ptr).unwrap(); + // Generate an arbitrary count using kani::any + let count: usize = kani::any(); + unsafe { src.copy_to_nonoverlapping(dest, count);} } #[kani::proof_for_contract(NonNull::::copy_from_nonoverlapping)] pub fn non_null_check_copy_from_nonoverlapping() { - let mut src_value: i32 = kani::any(); - let mut dest_value: i32 = 0; - - let src = NonNull::new(&mut src_value as *mut i32).unwrap(); - let dest = NonNull::new(&mut dest_value as *mut i32).unwrap(); - - //count represents no of elements to copy - let count = 1; - - unsafe { - dest.copy_from_nonoverlapping(src, count); - } - } -} + // PointerGenerator instance + let mut generator = PointerGenerator::<16>::new(); + // Generate arbitrary pointers for src and dest + let src_ptr = generator.any_in_bounds::().ptr; + let dest_ptr = generator.any_in_bounds::().ptr; + // Wrap the raw pointers in NonNull + let src = NonNull::new(src_ptr).unwrap(); + let dest = NonNull::new(dest_ptr).unwrap(); + // Generate an arbitrary count using kani::any + let count: usize = kani::any(); + unsafe { src.copy_from_nonoverlapping(dest, count);} + } +} \ No newline at end of file From 73c22f645394cf4b1304fe8c095b582f7fbaaa5f Mon Sep 17 00:00:00 2001 From: Dhvani-Kapadia <159494547+Dhvani-Kapadia@users.noreply.github.com> Date: Wed, 4 Dec 2024 23:33:40 -0800 Subject: [PATCH 09/14] updating all contracts --- library/core/src/ptr/non_null.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 353ec44999302..41fc1ca34761d 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1818,7 +1818,7 @@ mod verify { pub fn non_null_check_new() { let mut x: i32 = kani::any(); let xptr = &mut x; - let maybe_null_ptr = if kani::any() { xptr as *mut i32 } else { null_mut() }; + let maybe_null_ptr = if kani::any() { xptr as *mut i32 } else { null_mut() }; let _ = NonNull::new(maybe_null_ptr); } From 2f0e4b1d790f91635186768b82743921291e53d5 Mon Sep 17 00:00:00 2001 From: Dhvani-Kapadia <159494547+Dhvani-Kapadia@users.noreply.github.com> Date: Wed, 4 Dec 2024 23:49:08 -0800 Subject: [PATCH 10/14] changes made --- library/core/src/ptr/non_null.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 41fc1ca34761d..a504412ab9600 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1099,7 +1099,7 @@ impl NonNull { #[requires(count.checked_mul(core::mem::size_of::()).map_or(false, |size| size <= isize::MAX as usize) && ub_checks::can_dereference(NonNull::slice_from_raw_parts(src, count).as_ptr()) && ub_checks::can_write(NonNull::slice_from_raw_parts(self, count).as_ptr()) - && (self.as_ptr() as usize).abs_diff(dest.as_ptr() as usize) >= count * core::mem::size_of::())] + && (self.as_ptr() as usize).abs_diff(self.as_ptr() as usize) >= count * core::mem::size_of::())] #[ensures(|result: &()| ub_checks::can_dereference(src.as_ptr() as *const u8) && ub_checks::can_dereference(self.as_ptr() as *const u8))] #[kani::modifies(NonNull::slice_from_raw_parts(self, count).as_ptr())] From fa037b1f5533fc6f2e30130be3d45b163c10d106 Mon Sep 17 00:00:00 2001 From: Dhvani-Kapadia <159494547+Dhvani-Kapadia@users.noreply.github.com> Date: Thu, 5 Dec 2024 15:53:28 -0800 Subject: [PATCH 11/14] changes --- library/core/src/ptr/non_null.rs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index a504412ab9600..42f8f49fc16ba 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1017,7 +1017,7 @@ impl NonNull { #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "const_intrinsic_copy", since = "1.83.0")] - #[requires(count.checked_mul(core::mem::size_of::()).map_or(false, |size| size <= isize::MAX as usize) + #[requires(count.checked_mul(core::mem::size_of::()).map_or_else(|| false, |size| size <= isize::MAX as usize) && ub_checks::can_dereference(NonNull::slice_from_raw_parts(self, count).as_ptr()) && ub_checks::can_write(NonNull::slice_from_raw_parts(dest, count).as_ptr()))] #[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr() as *const u8) @@ -1043,10 +1043,10 @@ impl NonNull { #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "const_intrinsic_copy", since = "1.83.0")] - #[requires(count.checked_mul(core::mem::size_of::()).map_or(false, |size| size <= isize::MAX as usize) + #[requires(count.checked_mul(core::mem::size_of::()).map_or_else(|| false, |size| size <= isize::MAX as usize) && ub_checks::can_dereference(NonNull::slice_from_raw_parts(self, count).as_ptr()) && ub_checks::can_write(NonNull::slice_from_raw_parts(dest, count).as_ptr()) - && (self.as_ptr() as usize).abs_diff(dest.as_ptr() as usize) >= count * core::mem::size_of::())] + && ub_checks::maybe_is_nonoverlapping(self.as_ptr() as *const (), dest.as_ptr() as *const (), count, core::mem::size_of::()))] #[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr() as *const u8) && ub_checks::can_dereference(dest.as_ptr() as *const u8))] #[kani::modifies(NonNull::slice_from_raw_parts(dest, count).as_ptr())] @@ -1070,7 +1070,7 @@ impl NonNull { #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "const_intrinsic_copy", since = "1.83.0")] - #[requires(count.checked_mul(core::mem::size_of::()).map_or(false, |size| size <= isize::MAX as usize) + #[requires(count.checked_mul(core::mem::size_of::()).map_or_else(|| false, |size| size <= isize::MAX as usize) && ub_checks::can_dereference(NonNull::slice_from_raw_parts(src, count).as_ptr()) && ub_checks::can_write(NonNull::slice_from_raw_parts(self, count).as_ptr()))] #[ensures(|result: &()| ub_checks::can_dereference(src.as_ptr() as *const u8) @@ -1096,10 +1096,10 @@ impl NonNull { #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "const_intrinsic_copy", since = "1.83.0")] - #[requires(count.checked_mul(core::mem::size_of::()).map_or(false, |size| size <= isize::MAX as usize) + #[requires(count.checked_mul(core::mem::size_of::()).map_or_else(|| false, |size| size <= isize::MAX as usize) && ub_checks::can_dereference(NonNull::slice_from_raw_parts(src, count).as_ptr()) && ub_checks::can_write(NonNull::slice_from_raw_parts(self, count).as_ptr()) - && (self.as_ptr() as usize).abs_diff(self.as_ptr() as usize) >= count * core::mem::size_of::())] + && ub_checks::maybe_is_nonoverlapping(src.as_ptr() as *const (), self.as_ptr() as *const (), count, core::mem::size_of::()))] #[ensures(|result: &()| ub_checks::can_dereference(src.as_ptr() as *const u8) && ub_checks::can_dereference(self.as_ptr() as *const u8))] #[kani::modifies(NonNull::slice_from_raw_parts(self, count).as_ptr())] From cb3c0de83fce9fa3811572159a49635fc338149c Mon Sep 17 00:00:00 2001 From: Dhvani-Kapadia <159494547+Dhvani-Kapadia@users.noreply.github.com> Date: Thu, 5 Dec 2024 15:56:28 -0800 Subject: [PATCH 12/14] Update library/core/src/ptr/non_null.rs Co-authored-by: Carolyn Zech --- library/core/src/ptr/non_null.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index f5f4802637f31..adacaa25b0c45 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -2559,4 +2559,4 @@ mod verify { let count: usize = kani::any(); unsafe { src.copy_from_nonoverlapping(dest, count);} } -} \ No newline at end of file +} From eccd7da4d5c7e5ec154b72df07beaac9bf45850b Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Wed, 11 Dec 2024 10:29:56 -0800 Subject: [PATCH 13/14] fix modify clause format --- library/core/src/ptr/non_null.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index adacaa25b0c45..108326605fdfe 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1019,6 +1019,7 @@ impl NonNull { /// [`ptr::copy`]: crate::ptr::copy() #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[cfg_attr(kani, kani::modifies(NonNull::slice_from_raw_parts(dest, count).as_ptr()))] #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "const_intrinsic_copy", since = "1.83.0")] #[requires(count.checked_mul(core::mem::size_of::()).map_or_else(|| false, |size| size <= isize::MAX as usize) @@ -1026,7 +1027,6 @@ impl NonNull { && ub_checks::can_write(NonNull::slice_from_raw_parts(dest, count).as_ptr()))] #[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr() as *const u8) && ub_checks::can_dereference(dest.as_ptr() as *const u8))] - #[kani::modifies(NonNull::slice_from_raw_parts(dest, count).as_ptr())] pub const unsafe fn copy_to(self, dest: NonNull, count: usize) where T: Sized, @@ -1045,6 +1045,7 @@ impl NonNull { /// [`ptr::copy_nonoverlapping`]: crate::ptr::copy_nonoverlapping() #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[cfg_attr(kani, kani::modifies(NonNull::slice_from_raw_parts(dest, count).as_ptr()))] #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "const_intrinsic_copy", since = "1.83.0")] #[requires(count.checked_mul(core::mem::size_of::()).map_or_else(|| false, |size| size <= isize::MAX as usize) @@ -1053,7 +1054,6 @@ impl NonNull { && ub_checks::maybe_is_nonoverlapping(self.as_ptr() as *const (), dest.as_ptr() as *const (), count, core::mem::size_of::()))] #[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr() as *const u8) && ub_checks::can_dereference(dest.as_ptr() as *const u8))] - #[kani::modifies(NonNull::slice_from_raw_parts(dest, count).as_ptr())] pub const unsafe fn copy_to_nonoverlapping(self, dest: NonNull, count: usize) where T: Sized, @@ -1072,6 +1072,7 @@ impl NonNull { /// [`ptr::copy`]: crate::ptr::copy() #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[cfg_attr(kani, kani::modifies(NonNull::slice_from_raw_parts(self, count).as_ptr()))] #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "const_intrinsic_copy", since = "1.83.0")] #[requires(count.checked_mul(core::mem::size_of::()).map_or_else(|| false, |size| size <= isize::MAX as usize) @@ -1079,7 +1080,6 @@ impl NonNull { && ub_checks::can_write(NonNull::slice_from_raw_parts(self, count).as_ptr()))] #[ensures(|result: &()| ub_checks::can_dereference(src.as_ptr() as *const u8) && ub_checks::can_dereference(self.as_ptr() as *const u8))] - #[kani::modifies(NonNull::slice_from_raw_parts(self, count).as_ptr())] pub const unsafe fn copy_from(self, src: NonNull, count: usize) where T: Sized, @@ -1098,6 +1098,7 @@ impl NonNull { /// [`ptr::copy_nonoverlapping`]: crate::ptr::copy_nonoverlapping() #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[cfg_attr(kani, kani::modifies(NonNull::slice_from_raw_parts(self, count).as_ptr()))] #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "const_intrinsic_copy", since = "1.83.0")] #[requires(count.checked_mul(core::mem::size_of::()).map_or_else(|| false, |size| size <= isize::MAX as usize) @@ -1106,7 +1107,6 @@ impl NonNull { && ub_checks::maybe_is_nonoverlapping(src.as_ptr() as *const (), self.as_ptr() as *const (), count, core::mem::size_of::()))] #[ensures(|result: &()| ub_checks::can_dereference(src.as_ptr() as *const u8) && ub_checks::can_dereference(self.as_ptr() as *const u8))] - #[kani::modifies(NonNull::slice_from_raw_parts(self, count).as_ptr())] pub const unsafe fn copy_from_nonoverlapping(self, src: NonNull, count: usize) where T: Sized, From a93a1b0841d4dfaea3e7ed36d12745e1e222cdc8 Mon Sep 17 00:00:00 2001 From: Dhvani-Kapadia <159494547+Dhvani-Kapadia@users.noreply.github.com> Date: Wed, 11 Dec 2024 13:29:36 -0800 Subject: [PATCH 14/14] Update library/core/src/ptr/non_null.rs Co-authored-by: Michael Tautschnig --- library/core/src/ptr/non_null.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 44abbdce15e73..714104930dd5a 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1068,7 +1068,7 @@ impl NonNull { && ub_checks::can_dereference(NonNull::slice_from_raw_parts(self, count).as_ptr()) && ub_checks::can_write(NonNull::slice_from_raw_parts(dest, count).as_ptr()) && ub_checks::maybe_is_nonoverlapping(self.as_ptr() as *const (), dest.as_ptr() as *const (), count, core::mem::size_of::()))] - #[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr() as *const u8) + #[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr() as *const u8) && ub_checks::can_dereference(dest.as_ptr() as *const u8))] pub const unsafe fn copy_to_nonoverlapping(self, dest: NonNull, count: usize) where