diff --git a/library/Cargo.lock b/library/Cargo.lock index 47fbf5169f491..4689c78a98f7d 100644 --- a/library/Cargo.lock +++ b/library/Cargo.lock @@ -28,6 +28,7 @@ version = "0.0.0" dependencies = [ "compiler_builtins", "core", + "safety", ] [[package]] @@ -67,6 +68,9 @@ dependencies = [ [[package]] name = "core" version = "0.0.0" +dependencies = [ + "safety", +] [[package]] name = "coretests" @@ -196,6 +200,39 @@ dependencies = [ "unwind", ] +[[package]] +name = "proc-macro-error" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c" +dependencies = [ + "proc-macro-error-attr", + "proc-macro2", + "quote", + "syn 1.0.109", + "version_check", +] + +[[package]] +name = "proc-macro-error-attr" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869" +dependencies = [ + "proc-macro2", + "quote", + "version_check", +] + +[[package]] +name = "proc-macro2" +version = "1.0.106" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934" +dependencies = [ + "unicode-ident", +] + [[package]] name = "proc_macro" version = "0.0.0" @@ -212,6 +249,15 @@ dependencies = [ "cc", ] +[[package]] +name = "quote" +version = "1.0.45" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "41f2619966050689382d2b44f664f4bc593e129785a36d6ee376ddf37259b924" +dependencies = [ + "proc-macro2", +] + [[package]] name = "r-efi" version = "5.3.0" @@ -296,6 +342,16 @@ dependencies = [ "std", ] +[[package]] +name = "safety" +version = "0.1.0" +dependencies = [ + "proc-macro-error", + "proc-macro2", + "quote", + "syn 2.0.117", +] + [[package]] name = "shlex" version = "1.3.0" @@ -324,6 +380,7 @@ dependencies = [ "rand", "rand_xorshift", "rustc-demangle", + "safety", "std_detect", "unwind", "vex-sdk", @@ -341,6 +398,27 @@ dependencies = [ "rustc-std-workspace-core", ] +[[package]] +name = "syn" +version = "1.0.109" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" +dependencies = [ + "proc-macro2", + "unicode-ident", +] + +[[package]] +name = "syn" +version = "2.0.117" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e665b8803e7b1d2a727f4023456bbbbe74da67099c585258af0ad9c5013b9b99" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + [[package]] name = "sysroot" version = "0.0.0" @@ -361,6 +439,12 @@ dependencies = [ "std", ] +[[package]] +name = "unicode-ident" +version = "1.0.24" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75" + [[package]] name = "unwind" version = "0.0.0" @@ -380,6 +464,12 @@ dependencies = [ "rustc-std-workspace-core", ] +[[package]] +name = "version_check" +version = "0.9.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" + [[package]] name = "vex-sdk" version = "0.27.0" diff --git a/library/alloc/src/rc.rs b/library/alloc/src/rc.rs index 2b62b92d43886..d4057492ee718 100644 --- a/library/alloc/src/rc.rs +++ b/library/alloc/src/rc.rs @@ -274,6 +274,9 @@ use crate::string::String; #[cfg(not(no_global_oom_handling))] use crate::vec::Vec; +#[cfg(kani)] +use core::kani; + // This is repr(C) to future-proof against possible field-reordering, which // would interfere with otherwise safe [into|from]_raw() of transmutable // inner types. @@ -292,7 +295,11 @@ fn rc_inner_layout_for_value_layout(layout: Layout) -> Layout { // Previously, layout was calculated on the expression // `&*(ptr as *const RcInner)`, but this created a misaligned // reference (see #54908). - Layout::new::>().extend(layout).unwrap().0.pad_to_align() + Layout::new::>() + .extend(layout) + .unwrap() + .0 + .pad_to_align() } /// A single-threaded reference-counting pointer. 'Rc' stands for 'Reference @@ -372,7 +379,11 @@ impl Rc { #[inline] unsafe fn from_inner_in(ptr: NonNull>, alloc: A) -> Self { - Self { ptr, phantom: PhantomData, alloc } + Self { + ptr, + phantom: PhantomData, + alloc, + } } #[inline] @@ -386,7 +397,10 @@ impl Rc { // Reconstruct the "strong weak" pointer and drop it when this // variable goes out of scope. This ensures that the memory is // deallocated even if the destructor of `T` panics. - let _weak = Weak { ptr: self.ptr, alloc: &self.alloc }; + let _weak = Weak { + ptr: self.ptr, + alloc: &self.alloc, + }; // Destroy the contained object. // We cannot use `get_mut_unchecked` here, because `self.alloc` is borrowed. @@ -415,8 +429,12 @@ impl Rc { // if the weak pointer is stored inside the strong one. unsafe { Self::from_inner( - Box::leak(Box::new(RcInner { strong: Cell::new(1), weak: Cell::new(1), value })) - .into(), + Box::leak(Box::new(RcInner { + strong: Cell::new(1), + weak: Cell::new(1), + value, + })) + .into(), ) } } @@ -788,7 +806,10 @@ impl Rc { let uninit_ptr: NonNull<_> = (unsafe { &mut *uninit_raw_ptr }).into(); let init_ptr: NonNull> = uninit_ptr.cast(); - let weak = Weak { ptr: init_ptr, alloc }; + let weak = Weak { + ptr: init_ptr, + alloc, + }; // It's important we don't give up ownership of the weak pointer, or // else the memory might be freed by the time `data_fn` returns. If @@ -839,7 +860,11 @@ impl Rc { // the allocation while the strong destructor is running, even // if the weak pointer is stored inside the strong one. let (ptr, alloc) = Box::into_unique(Box::try_new_in( - RcInner { strong: Cell::new(1), weak: Cell::new(1), value }, + RcInner { + strong: Cell::new(1), + weak: Cell::new(1), + value, + }, alloc, )?); Ok(unsafe { Self::from_inner_in(ptr.into(), alloc) }) @@ -967,7 +992,10 @@ impl Rc { // pointer while also handling drop logic by just crafting a // fake Weak. this.inner().dec_strong(); - let _weak = Weak { ptr: this.ptr, alloc }; + let _weak = Weak { + ptr: this.ptr, + alloc, + }; Ok(val) } else { Err(this) @@ -1195,6 +1223,20 @@ impl Rc, A> { /// ``` #[stable(feature = "new_uninit", since = "1.82.0")] #[inline] + #[cfg_attr( + // Kani 0.65 limitation: proof_for_contract cannot target this + // MaybeUninit-based generic impl reliably. Verified via kani::proof + // harnesses (verify_1198 / verify_1239) with explicit postcondition checks. + kani, + kani::requires({ + let p = Rc::, A>::as_ptr(&self); + kani::mem::can_dereference(p) + }) + )] + #[cfg_attr( + kani, + kani::ensures(|result: &Rc| Rc::::strong_count(result) >= 1) + )] pub unsafe fn assume_init(self) -> Rc { let (ptr, alloc) = Rc::into_inner_with_allocator(self); unsafe { Rc::from_inner_in(ptr.cast(), alloc) } @@ -1233,6 +1275,20 @@ impl Rc<[mem::MaybeUninit], A> { /// ``` #[stable(feature = "new_uninit", since = "1.82.0")] #[inline] + #[cfg_attr( + // Kani 0.65 limitation: proof_for_contract cannot target this + // MaybeUninit-based generic impl reliably. Verified via kani::proof + // harnesses (verify_1198 / verify_1239) with explicit postcondition checks. + kani, + kani::requires({ + let p = Rc::<[mem::MaybeUninit], A>::as_ptr(&self); + kani::mem::can_dereference(p) + }) + )] + #[cfg_attr( + kani, + kani::ensures(|result: &Rc<[T], A>| Rc::<[T], A>::strong_count(result) >= 1) + )] pub unsafe fn assume_init(self) -> Rc<[T], A> { let (ptr, alloc) = Rc::into_inner_with_allocator(self); unsafe { Rc::from_ptr_in(ptr.as_ptr() as _, alloc) } @@ -1303,6 +1359,19 @@ impl Rc { /// ``` #[inline] #[stable(feature = "rc_raw", since = "1.17.0")] + #[cfg_attr( + kani, + kani::requires({ + let offset = unsafe { data_offset(ptr) }; + let inner = unsafe { ptr.byte_sub(offset) as *const RcInner }; + let rebuilt_ptr = unsafe { &raw const (*inner).value }; + + kani::mem::checked_align_of_raw(ptr).is_some() + && kani::mem::checked_size_of_raw(ptr).is_some() + && ptr == rebuilt_ptr + && unsafe { (*inner).strong.get() >= 1 } + }) + )] pub unsafe fn from_raw(ptr: *const T) -> Self { unsafe { Self::from_raw_in(ptr, Global) } } @@ -1363,6 +1432,22 @@ impl Rc { /// ``` #[inline] #[stable(feature = "rc_mutate_strong_count", since = "1.53.0")] + #[cfg_attr(kani, kani::requires(!ptr.is_null()))] + #[cfg_attr(kani, kani::requires(kani::mem::can_dereference(ptr)))] + #[cfg_attr(kani, kani::requires({ + let offset = unsafe { data_offset(ptr) }; + let rc_ptr = ptr.byte_sub(offset) as *const RcInner; + kani::mem::can_dereference(rc_ptr) + }))] + #[cfg_attr(kani, kani::requires({ + let offset = unsafe { data_offset(ptr) }; + let rc_ptr = ptr.byte_sub(offset) as *const RcInner; + kani::mem::can_dereference(rc_ptr) && unsafe { (*rc_ptr).strong.get() >= 1 } + }))] + #[cfg_attr(kani, kani::modifies({ + let offset = unsafe { data_offset(ptr) }; + ptr.byte_sub(offset) as *const RcInner + }))] pub unsafe fn increment_strong_count(ptr: *const T) { unsafe { Self::increment_strong_count_in(ptr, Global) } } @@ -1400,6 +1485,33 @@ impl Rc { /// ``` #[inline] #[stable(feature = "rc_mutate_strong_count", since = "1.53.0")] + #[cfg_attr( + kani, + kani::requires({ + let offset = unsafe { data_offset(ptr) }; + let inner_mut = unsafe { ptr.byte_sub(offset) as *mut RcInner }; + let inner = inner_mut as *const RcInner; + let rebuilt_ptr = unsafe { &raw const (*inner).value }; + let strong_ptr = unsafe { &raw mut (*inner_mut).strong }; + + let into_raw_roundtrip_ptr = { + let rc = unsafe { Rc::::from_raw(ptr) }; + Rc::::into_raw(rc) + }; + + ptr == rebuilt_ptr + && ptr == into_raw_roundtrip_ptr + && kani::mem::checked_size_of_raw(ptr) + == Some(unsafe { mem::size_of_val_raw(rebuilt_ptr) }) + && kani::mem::checked_align_of_raw(ptr) + == Some(unsafe { align_of_val_raw(rebuilt_ptr) }) + && unsafe { (*strong_ptr).get() >= 1 } + }) + )] + #[cfg_attr(kani, kani::modifies({ + let offset = unsafe { data_offset(ptr) }; + ptr.byte_sub(offset) as *const RcInner + }))] pub unsafe fn decrement_strong_count(ptr: *const T) { unsafe { Self::decrement_strong_count_in(ptr, Global) } } @@ -1540,6 +1652,25 @@ impl Rc { /// } /// ``` #[unstable(feature = "allocator_api", issue = "32838")] + #[cfg_attr( + kani, + kani::requires({ + let offset = unsafe { data_offset(ptr) }; + let inner = unsafe { ptr.byte_sub(offset) as *const RcInner }; + let rebuilt_ptr = unsafe { &raw const (*inner).value }; + + ptr == rebuilt_ptr + && kani::mem::checked_size_of_raw(ptr) + == Some(unsafe { mem::size_of_val_raw(rebuilt_ptr) }) + && kani::mem::checked_align_of_raw(ptr) + == Some(unsafe { align_of_val_raw(rebuilt_ptr) }) + && unsafe { (*inner).strong.get() >= 1 } + }) + )] + #[cfg_attr( + kani, + kani::ensures(|result: &Self| Rc::::as_ptr(result) == ptr) + )] pub unsafe fn from_raw_in(ptr: *const T, alloc: A) -> Self { let offset = unsafe { data_offset(ptr) }; @@ -1570,7 +1701,10 @@ impl Rc { this.inner().inc_weak(); // Make sure we do not create a dangling Weak debug_assert!(!is_dangling(this.ptr.as_ptr())); - Weak { ptr: this.ptr, alloc: this.alloc.clone() } + Weak { + ptr: this.ptr, + alloc: this.alloc.clone(), + } } /// Gets the number of [`Weak`] pointers to this allocation. @@ -1644,6 +1778,34 @@ impl Rc { /// ``` #[inline] #[unstable(feature = "allocator_api", issue = "32838")] + #[cfg_attr( + kani, + kani::requires({ + let offset = unsafe { data_offset(ptr) }; + let inner_mut = unsafe { ptr.byte_sub(offset) as *mut RcInner }; + let inner = inner_mut as *const RcInner; + let rebuilt_ptr = unsafe { &raw const (*inner).value }; + let strong_ptr = unsafe { &raw mut (*inner_mut).strong }; + + let into_raw_roundtrip_ptr = { + let rc = unsafe { Rc::::from_raw_in(ptr, alloc.clone()) }; + let (raw_ptr, _raw_alloc) = Rc::::into_raw_with_allocator(rc); + raw_ptr + }; + + ptr == rebuilt_ptr + && ptr == into_raw_roundtrip_ptr + && kani::mem::checked_size_of_raw(ptr) + == Some(unsafe { mem::size_of_val_raw(rebuilt_ptr) }) + && kani::mem::checked_align_of_raw(ptr) + == Some(unsafe { align_of_val_raw(rebuilt_ptr) }) + && unsafe { (*strong_ptr).get() >= 1 } + }) + )] + #[cfg_attr(kani, kani::modifies({ + let offset = unsafe { data_offset(ptr) }; + ptr.byte_sub(offset) as *const RcInner + }))] pub unsafe fn increment_strong_count_in(ptr: *const T, alloc: A) where A: Clone, @@ -1690,6 +1852,28 @@ impl Rc { /// ``` #[inline] #[unstable(feature = "allocator_api", issue = "32838")] + #[cfg_attr( + kani, + kani::requires({ + let offset = unsafe { data_offset(ptr) }; + let inner_mut = unsafe { ptr.byte_sub(offset) as *mut RcInner }; + let inner = inner_mut as *const RcInner; + let rebuilt_ptr = unsafe { &raw const (*inner).value }; + + let strong_ptr = unsafe { &raw mut (*inner_mut).strong }; + + ptr == rebuilt_ptr + && kani::mem::checked_size_of_raw(ptr) + == Some(unsafe { mem::size_of_val_raw(rebuilt_ptr) }) + && kani::mem::checked_align_of_raw(ptr) + == Some(unsafe { align_of_val_raw(rebuilt_ptr) }) + && unsafe { (*strong_ptr).get() >= 1 } + }) + )] + #[cfg_attr(kani, kani::modifies({ + let offset = unsafe { data_offset(ptr) }; + ptr.byte_sub(offset) as *const RcInner + }))] pub unsafe fn decrement_strong_count_in(ptr: *const T, alloc: A) { unsafe { drop(Rc::from_raw_in(ptr, alloc)) }; } @@ -1728,7 +1912,11 @@ impl Rc { #[inline] #[stable(feature = "rc_unique", since = "1.4.0")] pub fn get_mut(this: &mut Self) -> Option<&mut T> { - if Rc::is_unique(this) { unsafe { Some(Rc::get_mut_unchecked(this)) } } else { None } + if Rc::is_unique(this) { + unsafe { Some(Rc::get_mut_unchecked(this)) } + } else { + None + } } /// Returns a mutable reference into the given `Rc`, @@ -1793,6 +1981,25 @@ impl Rc { /// ``` #[inline] #[unstable(feature = "get_mut_unchecked", issue = "63292")] + #[cfg_attr( + kani, + kani::requires({ + let inner = this.ptr.as_ptr(); + let value = unsafe { &raw mut (*inner).value }; + + kani::mem::can_dereference(inner) + && kani::mem::can_dereference(value) + && kani::mem::can_write(value) + }) + )] + #[cfg_attr( + kani, + kani::ensures(|result: &&mut T| { + let inner = old(this.ptr.as_ptr()); + let value = unsafe { &raw const (*inner).value }; + core::ptr::addr_eq((*result) as *const T, value) + }) + )] pub unsafe fn get_mut_unchecked(this: &mut Self) -> &mut T { // We are careful to *not* create a reference covering the "count" fields, as // this would conflict with accesses to the reference counts (e.g. by `Weak`). @@ -2026,6 +2233,7 @@ impl Rc { /// [`downcast`]: Self::downcast #[inline] #[unstable(feature = "downcast_unchecked", issue = "90850")] + #[cfg_attr(kani, kani::requires((*self).is::()))] pub unsafe fn downcast_unchecked(self) -> Rc { unsafe { let (ptr, alloc) = Rc::into_inner_with_allocator(self); @@ -2180,7 +2388,12 @@ impl Rc<[T]> { // Pointer to first element let elems = (&raw mut (*ptr).value) as *mut T; - let mut guard = Guard { mem: NonNull::new_unchecked(mem), elems, layout, n_elems: 0 }; + let mut guard = Guard { + mem: NonNull::new_unchecked(mem), + elems, + layout, + n_elems: 0, + }; for (i, item) in iter.enumerate() { ptr::write(elems.add(i), item); @@ -2347,7 +2560,11 @@ impl Default for Rc { Self::from_inner( Box::leak(Box::write( Box::new_uninit(), - RcInner { strong: Cell::new(1), weak: Cell::new(1), value: T::default() }, + RcInner { + strong: Cell::new(1), + weak: Cell::new(1), + value: T::default(), + }, )) .into(), ) @@ -3040,7 +3257,10 @@ impl Weak { #[rustc_const_stable(feature = "const_weak_new", since = "1.73.0")] #[must_use] pub const fn new() -> Weak { - Weak { ptr: NonNull::without_provenance(NonZeroUsize::MAX), alloc: Global } + Weak { + ptr: NonNull::without_provenance(NonZeroUsize::MAX), + alloc: Global, + } } } @@ -3062,7 +3282,10 @@ impl Weak { #[inline] #[unstable(feature = "allocator_api", issue = "32838")] pub fn new_in(alloc: A) -> Weak { - Weak { ptr: NonNull::without_provenance(NonZeroUsize::MAX), alloc } + Weak { + ptr: NonNull::without_provenance(NonZeroUsize::MAX), + alloc, + } } } @@ -3122,6 +3345,63 @@ impl Weak { /// [`new`]: Weak::new #[inline] #[stable(feature = "weak_into_raw", since = "1.45.0")] + #[cfg_attr( + kani, + kani::requires({ + let is_sentinel = is_dangling(ptr); + if is_sentinel { + true + } else { + let offset = unsafe { data_offset(ptr) }; + let inner = unsafe { ptr.byte_sub(offset) as *const RcInner }; + let rebuilt_ptr = unsafe { &raw const (*inner).value }; + + kani::mem::same_allocation(ptr.cast::(), inner.cast::()) + && ptr == rebuilt_ptr + && kani::mem::can_dereference(unsafe { &raw const (*inner).strong }) + && kani::mem::can_dereference(unsafe { &raw const (*inner).weak }) + } + }) + )] + #[cfg_attr( + kani, + kani::requires({ + let is_sentinel = is_dangling(ptr); + is_sentinel || { + let offset = unsafe { data_offset(ptr) }; + let inner = unsafe { ptr.byte_sub(offset) as *const RcInner }; + unsafe { (*inner).weak.get() > 0 } + } + }) + )] + #[cfg_attr( + kani, + kani::ensures(|result: &Self| { + if old(is_dangling(ptr)) { + (result.ptr.as_ptr().cast::<()>()).addr() == usize::MAX + && (result.as_ptr().cast::<()>()).addr() == usize::MAX + } else { + result.as_ptr() == ptr + && result.ptr.as_ptr() + == old({ + let offset = unsafe { data_offset(ptr) }; + unsafe { ptr.byte_sub(offset) as *mut RcInner } + }) + } + }) + )] + #[cfg_attr( + kani, + kani::ensures(|result: &Self| { + old(is_dangling(ptr)) + || unsafe { (*result.ptr.as_ptr()).weak.get() } + == old({ + let offset = unsafe { data_offset(ptr) }; + let inner = unsafe { ptr.byte_sub(offset) as *const RcInner }; + unsafe { (*inner).weak.get() } + }) + }) + )] pub unsafe fn from_raw(ptr: *const T) -> Self { unsafe { Self::from_raw_in(ptr, Global) } } @@ -3294,6 +3574,53 @@ impl Weak { /// [`new`]: Weak::new #[inline] #[unstable(feature = "allocator_api", issue = "32838")] + #[cfg_attr( + kani, + kani::requires({ + let is_sentinel = is_dangling(ptr); + if is_sentinel { + true + } else { + let offset = unsafe { data_offset(ptr) }; + let inner = unsafe { ptr.byte_sub(offset) as *const RcInner }; + let rebuilt_ptr = unsafe { &raw const (*inner).value }; + + kani::mem::same_allocation(ptr.cast::(), inner.cast::()) + && ptr == rebuilt_ptr + && kani::mem::can_dereference(unsafe { &raw const (*inner).strong }) + && kani::mem::can_dereference(unsafe { &raw const (*inner).weak }) + && unsafe { (*inner).weak.get() > 0 } + } + }) + )] + #[cfg_attr( + kani, + kani::ensures(|result: &Self| { + if old(is_dangling(ptr)) { + (result.ptr.as_ptr().cast::<()>()).addr() == usize::MAX + && (result.as_ptr().cast::<()>()).addr() == usize::MAX + } else { + result.as_ptr() == ptr + && result.ptr.as_ptr() + == old({ + let offset = unsafe { data_offset(ptr) }; + unsafe { ptr.byte_sub(offset) as *mut RcInner } + }) + } + }) + )] + #[cfg_attr( + kani, + kani::ensures(|result: &Self| { + old(is_dangling(ptr)) + || unsafe { (*result.ptr.as_ptr()).weak.get() } + == old({ + let offset = unsafe { data_offset(ptr) }; + let inner = unsafe { ptr.byte_sub(offset) as *const RcInner }; + unsafe { (*inner).weak.get() } + }) + }) + )] pub unsafe fn from_raw_in(ptr: *const T, alloc: A) -> Self { // See Weak::as_ptr for context on how the input pointer is derived. @@ -3310,7 +3637,10 @@ impl Weak { }; // SAFETY: we now have recovered the original Weak pointer, so can create the Weak. - Weak { ptr: unsafe { NonNull::new_unchecked(ptr) }, alloc } + Weak { + ptr: unsafe { NonNull::new_unchecked(ptr) }, + alloc, + } } /// Attempts to upgrade the `Weak` pointer to an [`Rc`], delaying @@ -3361,7 +3691,11 @@ impl Weak { #[must_use] #[stable(feature = "weak_counts", since = "1.41.0")] pub fn strong_count(&self) -> usize { - if let Some(inner) = self.inner() { inner.strong() } else { 0 } + if let Some(inner) = self.inner() { + inner.strong() + } else { + 0 + } } /// Gets the number of `Weak` pointers pointing to this allocation. @@ -3393,7 +3727,10 @@ impl Weak { // is dropped, the data field will be dropped in-place). Some(unsafe { let ptr = self.ptr.as_ptr(); - WeakInner { strong: &(*ptr).strong, weak: &(*ptr).weak } + WeakInner { + strong: &(*ptr).strong, + weak: &(*ptr).weak, + } }) } } @@ -3472,14 +3809,19 @@ unsafe impl<#[may_dangle] T: ?Sized, A: Allocator> Drop for Weak { /// assert!(other_weak_foo.upgrade().is_none()); /// ``` fn drop(&mut self) { - let inner = if let Some(inner) = self.inner() { inner } else { return }; + let inner = if let Some(inner) = self.inner() { + inner + } else { + return; + }; inner.dec_weak(); // the weak count starts at 1, and will only go to zero if all // the strong pointers have disappeared. if inner.weak() == 0 { unsafe { - self.alloc.deallocate(self.ptr.cast(), Layout::for_value_raw(self.ptr.as_ptr())); + self.alloc + .deallocate(self.ptr.cast(), Layout::for_value_raw(self.ptr.as_ptr())); } } } @@ -3503,7 +3845,10 @@ impl Clone for Weak { if let Some(inner) = self.inner() { inner.inc_weak() } - Weak { ptr: self.ptr, alloc: self.alloc.clone() } + Weak { + ptr: self.ptr, + alloc: self.alloc.clone(), + } } } @@ -4013,7 +4358,12 @@ impl UniqueRc { }, alloc, )); - Self { ptr: ptr.into(), _marker: PhantomData, _marker2: PhantomData, alloc } + Self { + ptr: ptr.into(), + _marker: PhantomData, + _marker2: PhantomData, + alloc, + } } } @@ -4055,7 +4405,10 @@ impl UniqueRc { unsafe { this.ptr.as_ref().inc_weak(); } - Weak { ptr: this.ptr, alloc: this.alloc.clone() } + Weak { + ptr: this.ptr, + alloc: this.alloc.clone(), + } } } @@ -4090,7 +4443,8 @@ unsafe impl<#[may_dangle] T: ?Sized, A: Allocator> Drop for UniqueRc { self.ptr.as_ref().dec_weak(); if self.ptr.as_ref().weak() == 0 { - self.alloc.deallocate(self.ptr.cast(), Layout::for_value_raw(self.ptr.as_ptr())); + self.alloc + .deallocate(self.ptr.cast(), Layout::for_value_raw(self.ptr.as_ptr())); } } } @@ -4121,7 +4475,11 @@ impl UniqueRcUninit { |mem| mem.with_metadata_of(ptr::from_ref(for_value) as *const RcInner), ) }; - Self { ptr: NonNull::new(ptr).unwrap(), layout_for_value: layout, alloc: Some(alloc) } + Self { + ptr: NonNull::new(ptr).unwrap(), + layout_for_value: layout, + alloc: Some(alloc), + } } /// Returns the pointer to be written into to initialize the [`Rc`]. @@ -4160,3 +4518,6709 @@ impl Drop for UniqueRcUninit { } } } + +// ========================================================================= +// Challenge 26: Verify reference-counted Cell implementation harnesses +// ========================================================================= + +#[cfg(kani)] +mod kani_rc_harness_helpers { + use super::*; + + pub(super) fn verifier_nondet_vec() -> Vec { + let cap: usize = kani::any(); + let elem_layout = Layout::new::(); + kani::assume(elem_layout.repeat(cap).is_ok()); + let mut v = Vec::::with_capacity(cap); + unsafe { + let sz: usize = kani::any(); + kani::assume(sz <= cap); + v.set_len(sz); + } + v + } + + pub(super) fn rc_slice_layout_ok(len: usize) -> bool { + Layout::array::(len) + .and_then(|value_layout| { + Layout::new::>() + .extend(value_layout) + .map(|_| ()) + }) + .is_ok() + } + + pub(super) fn nondet_rc_slice(vec: &Vec) -> &[T] { + let len = vec.len(); + kani::assume(rc_slice_layout_ok::(len)); + vec.as_slice() + } + + pub(super) fn verifier_nondet_vec_rc() -> Vec { + let vec = verifier_nondet_vec(); + kani::assume(rc_slice_layout_ok::(vec.len())); + vec + } +} + +// === UNSAFE FUNCTIONS (12 — all required) === + +#[cfg(kani)] +mod verify_1198 { + use super::*; + + // Kani 0.65 limitation: proof_for_contract cannot resolve paths for + // impl Rc, A> — the macro fails to map + // MaybeUninit back to the impl's generic parameter T. + // These harnesses use #[kani::proof] instead; the requires clause + // is still checked as an assertion at the call site, and we manually + // assert the postcondition (*init == value) below. + + #[kani::proof] + pub fn harness_assume_init_i32_global() { + let value: i32 = kani::any(); + let mut uninit: Rc, Global> = Rc::new_uninit_in(Global); + Rc::get_mut(&mut uninit).unwrap().write(value); + let init: Rc = unsafe { uninit.assume_init() }; + assert_eq!(*init, value); + } + + #[kani::proof] + pub fn harness_assume_init_u64_global() { + let value: u64 = kani::any(); + let mut uninit: Rc, Global> = Rc::new_uninit_in(Global); + Rc::get_mut(&mut uninit).unwrap().write(value); + let init: Rc = unsafe { uninit.assume_init() }; + assert_eq!(*init, value); + } + + #[kani::proof] + pub fn harness_assume_init_bool_global() { + let value: bool = kani::any(); + let mut uninit: Rc, Global> = Rc::new_uninit_in(Global); + Rc::get_mut(&mut uninit).unwrap().write(value); + let init: Rc = unsafe { uninit.assume_init() }; + assert_eq!(*init, value); + } +} + +#[cfg(kani)] +mod verify_1239 { + use super::*; + + // Kani 0.65 limitation: proof_for_contract cannot resolve paths for + // impl Rc<[MaybeUninit], A> (same issue as verify_1198). + // Uses #[kani::proof]; requires is checked as assertion at call site. + + #[kani::proof] + pub fn harness_assume_init_slice_u8_global() { + let values: [u8; 3] = kani::any(); + let mut uninit: Rc<[mem::MaybeUninit], Global> = Rc::new_uninit_slice(3); + let data = Rc::get_mut(&mut uninit).unwrap(); + data[0].write(values[0]); + data[1].write(values[1]); + data[2].write(values[2]); + let init: Rc<[u8], Global> = unsafe { uninit.assume_init() }; + assert_eq!(init[0], values[0]); + assert_eq!(init[1], values[1]); + assert_eq!(init[2], values[2]); + } + + #[kani::proof] + pub fn harness_assume_init_slice_bool_global() { + let values: [bool; 2] = kani::any(); + let mut uninit: Rc<[mem::MaybeUninit], Global> = Rc::new_uninit_slice(2); + let data = Rc::get_mut(&mut uninit).unwrap(); + data[0].write(values[0]); + data[1].write(values[1]); + let init: Rc<[bool], Global> = unsafe { uninit.assume_init() }; + assert_eq!(init[0], values[0]); + assert_eq!(init[1], values[1]); + } +} + +#[cfg(kani)] +mod verify_1327 { + use super::kani_rc_harness_helpers::*; + use super::*; + + #[kani::proof_for_contract(Rc::::from_raw)] + pub fn harness_rc_from_raw_i32() { + let value: i32 = kani::any(); + let rc: Rc = Rc::new(value); + let ptr: *const i32 = Rc::into_raw(rc); + let _recovered: Rc = unsafe { Rc::from_raw(ptr) }; + } + + #[kani::proof_for_contract(Rc::::from_raw)] + pub fn harness_rc_from_raw_u64() { + let value: u64 = kani::any(); + let rc: Rc = Rc::new(value); + let ptr: *const u64 = Rc::into_raw(rc); + let _recovered: Rc = unsafe { Rc::from_raw(ptr) }; + } + + #[kani::proof_for_contract(Rc::::from_raw)] + pub fn harness_rc_from_raw_bool() { + let value: bool = kani::any(); + let rc: Rc = Rc::new(value); + let ptr: *const bool = Rc::into_raw(rc); + let _recovered: Rc = unsafe { Rc::from_raw(ptr) }; + } + + #[kani::proof_for_contract(Rc::<()>::from_raw)] + pub fn harness_rc_from_raw_unit() { + let value: () = kani::any(); + let rc: Rc<()> = Rc::new(value); + let ptr: *const () = Rc::into_raw(rc); + let _recovered: Rc<()> = unsafe { Rc::from_raw(ptr) }; + } + + #[kani::proof_for_contract(Rc::<[u8; 4]>::from_raw)] + pub fn harness_rc_from_raw_array4_u8() { + let value: [u8; 4] = kani::any(); + let rc: Rc<[u8; 4]> = Rc::new(value); + let ptr: *const [u8; 4] = Rc::into_raw(rc); + let _recovered: Rc<[u8; 4]> = unsafe { Rc::from_raw(ptr) }; + } + + #[kani::proof_for_contract(Rc::<[u8]>::from_raw)] + pub fn harness_rc_from_raw_unsized_slice_u8() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new(slice); + let ptr = Rc::into_raw(rc); + let _recovered = unsafe { Rc::from_raw(ptr) }; + } + + #[kani::proof_for_contract(Rc::<[u16]>::from_raw)] + pub fn harness_rc_from_raw_unsized_slice_u16() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new(slice); + let ptr = Rc::into_raw(rc); + let _recovered = unsafe { Rc::from_raw(ptr) }; + } + + #[kani::proof_for_contract(Rc::<[u32]>::from_raw)] + pub fn harness_rc_from_raw_unsized_slice_u32() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new(slice); + let ptr = Rc::into_raw(rc); + let _recovered = unsafe { Rc::from_raw(ptr) }; + } +} + +#[cfg(kani)] +mod verify_1403 { + use super::kani_rc_harness_helpers::*; + use super::*; + + #[kani::proof_for_contract(Rc::::increment_strong_count)] + pub fn harness_increment_strong_count_i32() { + let value: i32 = kani::any(); + let rc = Rc::new(value); + let ptr = Rc::into_raw(rc); + + unsafe { + Rc::increment_strong_count(ptr); + let _recovered = Rc::from_raw(ptr); + Rc::decrement_strong_count(ptr); + } + } + + #[kani::proof_for_contract(Rc::<()>::increment_strong_count)] + pub fn harness_increment_strong_count_unit() { + let value: () = kani::any(); + let rc = Rc::new(value); + let ptr = Rc::into_raw(rc); + + unsafe { + Rc::increment_strong_count(ptr); + let _recovered = Rc::from_raw(ptr); + Rc::decrement_strong_count(ptr); + } + } + + #[kani::proof_for_contract(Rc::<[u8; 4]>::increment_strong_count)] + pub fn harness_increment_strong_count_array4_u8() { + let value: [u8; 4] = kani::any(); + let rc = Rc::new(value); + let ptr = Rc::into_raw(rc); + + unsafe { + Rc::increment_strong_count(ptr); + let _recovered = Rc::from_raw(ptr); + Rc::decrement_strong_count(ptr); + } + } + + #[kani::proof_for_contract(Rc::<[u8]>::increment_strong_count)] + pub fn harness_increment_strong_count_unsized_slice_u8() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new(slice); + let ptr = Rc::into_raw(rc); + + unsafe { + Rc::increment_strong_count(ptr); + let _recovered = Rc::from_raw(ptr); + Rc::decrement_strong_count(ptr); + } + } + + #[kani::proof_for_contract(Rc::<[u16]>::increment_strong_count)] + pub fn harness_increment_strong_count_unsized_slice_u16() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new(slice); + let ptr = Rc::into_raw(rc); + + unsafe { + Rc::increment_strong_count(ptr); + let _recovered = Rc::from_raw(ptr); + Rc::decrement_strong_count(ptr); + } + } + + #[kani::proof_for_contract(Rc::<[u32]>::increment_strong_count)] + pub fn harness_increment_strong_count_unsized_slice_u32() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new(slice); + let ptr = Rc::into_raw(rc); + + unsafe { + Rc::increment_strong_count(ptr); + let _recovered = Rc::from_raw(ptr); + Rc::decrement_strong_count(ptr); + } + } +} + +#[cfg(kani)] +mod verify_1486 { + use super::kani_rc_harness_helpers::*; + use super::*; + + #[kani::proof_for_contract(Rc::::decrement_strong_count)] + pub fn harness_rc_decrement_strong_count_i32() { + let value: i32 = kani::any(); + let rc: Rc = Rc::new(value); + let ptr: *const i32 = Rc::into_raw(rc); + unsafe { + Rc::increment_strong_count(ptr); + } + unsafe { + Rc::::decrement_strong_count(ptr); + } + } + + #[kani::proof_for_contract(Rc::<()>::decrement_strong_count)] + pub fn harness_rc_decrement_strong_count_unit() { + let value: () = kani::any(); + let rc: Rc<()> = Rc::new(value); + let ptr: *const () = Rc::into_raw(rc); + unsafe { + Rc::increment_strong_count(ptr); + } + unsafe { + Rc::<()>::decrement_strong_count(ptr); + } + } + + #[kani::proof_for_contract(Rc::<[u8; 4]>::decrement_strong_count)] + pub fn harness_rc_decrement_strong_count_array4_u8() { + let value: [u8; 4] = kani::any(); + let rc: Rc<[u8; 4]> = Rc::new(value); + let ptr: *const [u8; 4] = Rc::into_raw(rc); + unsafe { + Rc::increment_strong_count(ptr); + } + unsafe { + Rc::<[u8; 4]>::decrement_strong_count(ptr); + } + } + + #[kani::proof_for_contract(Rc::<[u8]>::decrement_strong_count)] + pub fn harness_rc_decrement_strong_count_unsized_slice_u8() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new(slice); + let ptr = Rc::into_raw(rc); + unsafe { + Rc::increment_strong_count(ptr); + } + unsafe { + Rc::decrement_strong_count(ptr); + } + } + + #[kani::proof_for_contract(Rc::<[u16]>::decrement_strong_count)] + pub fn harness_rc_decrement_strong_count_unsized_slice_u16() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new(slice); + let ptr = Rc::into_raw(rc); + unsafe { + Rc::increment_strong_count(ptr); + } + unsafe { + Rc::decrement_strong_count(ptr); + } + } + + #[kani::proof_for_contract(Rc::<[u32]>::decrement_strong_count)] + pub fn harness_rc_decrement_strong_count_unsized_slice_u32() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new(slice); + let ptr = Rc::into_raw(rc); + unsafe { + Rc::increment_strong_count(ptr); + } + unsafe { + Rc::decrement_strong_count(ptr); + } + } +} + +#[cfg(kani)] +mod verify_1650 { + use super::kani_rc_harness_helpers::*; + use super::*; + + #[kani::proof_for_contract(Rc::::from_raw_in)] + pub fn harness_rc_from_raw_in_i32_global() { + let value: i32 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + let (ptr, alloc): (*const i32, Global) = Rc::into_raw_with_allocator(rc); + let _recovered: Rc = unsafe { Rc::from_raw_in(ptr, alloc) }; + } + + #[kani::proof_for_contract(Rc::::from_raw_in)] + pub fn harness_rc_from_raw_in_bool_global() { + let value: bool = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + let (ptr, alloc): (*const bool, Global) = Rc::into_raw_with_allocator(rc); + let _recovered: Rc = unsafe { Rc::from_raw_in(ptr, alloc) }; + } + + #[kani::proof_for_contract(Rc::<(), Global>::from_raw_in)] + pub fn harness_rc_from_raw_in_unit_global() { + let value: () = kani::any(); + let rc: Rc<(), Global> = Rc::new_in(value, Global); + let (ptr, alloc): (*const (), Global) = Rc::into_raw_with_allocator(rc); + let _recovered: Rc<(), Global> = unsafe { Rc::from_raw_in(ptr, alloc) }; + } + + #[kani::proof_for_contract(Rc::<[u32; 3], Global>::from_raw_in)] + pub fn harness_rc_from_raw_in_array3_global() { + let values: [u32; 3] = kani::any(); + let rc: Rc<[u32], Global> = Rc::new_in(values, Global); + let (ptr, alloc): (*const [u32], Global) = Rc::into_raw_with_allocator(rc); + let _recovered: Rc<[u32; 3], Global> = + unsafe { Rc::from_raw_in(ptr.cast::<[u32; 3]>(), alloc) }; + } + + #[kani::proof_for_contract(Rc::<[u8], Global>::from_raw_in)] + pub fn harness_rc_from_raw_in_unsized_slice_u8_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + let (ptr, alloc) = Rc::into_raw_with_allocator(rc); + let _recovered = unsafe { Rc::from_raw_in(ptr, alloc) }; + } + + #[kani::proof_for_contract(Rc::<[u16], Global>::from_raw_in)] + pub fn harness_rc_from_raw_in_unsized_slice_u16_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + let (ptr, alloc) = Rc::into_raw_with_allocator(rc); + let _recovered = unsafe { Rc::from_raw_in(ptr, alloc) }; + } + + #[kani::proof_for_contract(Rc::<[u32], Global>::from_raw_in)] + pub fn harness_rc_from_raw_in_unsized_slice_u32_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + let (ptr, alloc) = Rc::into_raw_with_allocator(rc); + let _recovered = unsafe { Rc::from_raw_in(ptr, alloc) }; + } +} + +#[cfg(kani)] +mod verify_1792 { + use super::kani_rc_harness_helpers::*; + use super::*; + + #[kani::proof_for_contract(Rc::::increment_strong_count_in)] + pub fn harness_rc_increment_strong_count_in_i32_global() { + let value: i32 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + let rc2 = rc.clone(); + let (ptr, _alloc): (*const i32, Global) = Rc::into_raw_with_allocator(rc2); + unsafe { + Rc::::increment_strong_count_in(ptr, Global); + Rc::::decrement_strong_count_in(ptr, Global); + Rc::::decrement_strong_count_in(ptr, Global); + } + } + + #[kani::proof_for_contract(Rc::<(), Global>::increment_strong_count_in)] + pub fn harness_rc_increment_strong_count_in_unit_global() { + let value: () = kani::any(); + let rc: Rc<(), Global> = Rc::new_in(value, Global); + let rc2 = rc.clone(); + let (ptr, _alloc): (*const (), Global) = Rc::into_raw_with_allocator(rc2); + unsafe { + Rc::<(), Global>::increment_strong_count_in(ptr, Global); + Rc::<(), Global>::decrement_strong_count_in(ptr, Global); + Rc::<(), Global>::decrement_strong_count_in(ptr, Global); + } + } + + #[kani::proof_for_contract(Rc::<[u8; 4], Global>::increment_strong_count_in)] + pub fn harness_rc_increment_strong_count_in_slice_u8_global() { + let value: [u8; 4] = kani::any(); + let rc: Rc<[u8; 4], Global> = Rc::new_in(value, Global); + let rc2 = rc.clone(); + let (ptr, _alloc): (*const [u8; 4], Global) = Rc::into_raw_with_allocator(rc2); + unsafe { + Rc::<[u8; 4], Global>::increment_strong_count_in(ptr, Global); + Rc::<[u8; 4], Global>::decrement_strong_count_in(ptr, Global); + Rc::<[u8; 4], Global>::decrement_strong_count_in(ptr, Global); + } + } + + #[kani::proof_for_contract(Rc::<[u8]>::increment_strong_count_in)] + pub fn harness_rc_increment_strong_count_in_unsized_slice_u8_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + let rc2 = rc.clone(); + let (ptr, _alloc) = Rc::into_raw_with_allocator(rc2); + unsafe { + Rc::increment_strong_count_in(ptr, Global); + Rc::decrement_strong_count_in(ptr, Global); + Rc::decrement_strong_count_in(ptr, Global); + } + } + + #[kani::proof_for_contract(Rc::<[u16]>::increment_strong_count_in)] + pub fn harness_rc_increment_strong_count_in_unsized_slice_u16_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + let rc2 = rc.clone(); + let (ptr, _alloc) = Rc::into_raw_with_allocator(rc2); + unsafe { + Rc::increment_strong_count_in(ptr, Global); + Rc::decrement_strong_count_in(ptr, Global); + Rc::decrement_strong_count_in(ptr, Global); + } + } + + #[kani::proof_for_contract(Rc::<[u32]>::increment_strong_count_in)] + pub fn harness_rc_increment_strong_count_in_unsized_slice_u32_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + let rc2 = rc.clone(); + let (ptr, _alloc) = Rc::into_raw_with_allocator(rc2); + unsafe { + Rc::increment_strong_count_in(ptr, Global); + Rc::decrement_strong_count_in(ptr, Global); + Rc::decrement_strong_count_in(ptr, Global); + } + } +} + +#[cfg(kani)] +mod verify_1878 { + use core::u8; + + use super::kani_rc_harness_helpers::*; + use super::*; + use crate::rc; + + #[kani::proof_for_contract(Rc::::decrement_strong_count_in)] + pub fn harness_rc_decrement_strong_count_in_i32_global() { + let value: i32 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + let rc2 = rc.clone(); + let (ptr, alloc): (*const i32, Global) = Rc::into_raw_with_allocator(rc2); + unsafe { + Rc::::decrement_strong_count_in(ptr, alloc); + } + } + + #[kani::proof_for_contract(Rc::<(), Global>::decrement_strong_count_in)] + pub fn harness_rc_decrement_strong_count_in_unit_global() { + let value: () = kani::any(); + let rc: Rc<(), Global> = Rc::new_in(value, Global); + let rc2 = rc.clone(); + let (ptr, alloc): (*const (), Global) = Rc::into_raw_with_allocator(rc2); + unsafe { + Rc::<(), Global>::decrement_strong_count_in(ptr, alloc); + } + } + + #[kani::proof_for_contract(Rc::<[u8; 4], Global>::decrement_strong_count_in)] + pub fn harness_rc_decrement_strong_count_in_slice_u8_global() { + let value: [u8; 4] = kani::any(); + let rc: Rc<[u8; 4], Global> = Rc::new_in(value, Global); + let rc2 = rc.clone(); + let (ptr, alloc): (*const [u8; 4], Global) = Rc::into_raw_with_allocator(rc2); + unsafe { + Rc::<[u8; 4], Global>::decrement_strong_count_in(ptr, alloc); + } + } + + #[kani::proof_for_contract(Rc::<[u8]>::decrement_strong_count_in)] + pub fn harness_rc_decrement_strong_count_in_unsized_slice_u8_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + let rc2 = rc.clone(); + let (ptr, _alloc) = Rc::into_raw_with_allocator(rc2); + unsafe { + Rc::decrement_strong_count_in(ptr, Global); + } + } + + #[kani::proof_for_contract(Rc::<[u16]>::decrement_strong_count_in)] + pub fn harness_rc_decrement_strong_count_in_unsized_slice_u16_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + let rc2 = rc.clone(); + let (ptr, _alloc) = Rc::into_raw_with_allocator(rc2); + unsafe { + Rc::decrement_strong_count_in(ptr, Global); + } + } + + #[kani::proof_for_contract(Rc::<[u32]>::decrement_strong_count_in)] + pub fn harness_rc_decrement_strong_count_in_unsized_slice_u32_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + let rc2 = rc.clone(); + let (ptr, _alloc) = Rc::into_raw_with_allocator(rc2); + unsafe { + Rc::decrement_strong_count_in(ptr, Global); + } + } +} + +#[cfg(kani)] +mod verify_1982 { + use super::kani_rc_harness_helpers::*; + use super::*; + + #[kani::proof_for_contract(Rc::::get_mut_unchecked)] + pub fn harness_get_mut_unchecked_i32() { + let value: i32 = kani::any(); + let replacement: i32 = kani::any(); + let mut rc: Rc = Rc::new(value); + + unsafe { + *Rc::get_mut_unchecked(&mut rc) = replacement; + } + } + + #[kani::proof_for_contract(Rc::::get_mut_unchecked)] + pub fn harness_get_mut_unchecked_string() { + let mut rc: Rc = Rc::new(String::from("seed")); + + unsafe { + Rc::get_mut_unchecked(&mut rc).push_str(" value"); + } + } + + #[kani::proof_for_contract(Rc::::get_mut_unchecked)] + fn harness_get_mut_unchecked_shared_same_type_dormant() { + let mut rc1: Rc = Rc::new(String::new()); + let rc2 = rc1.clone(); + + unsafe { + Rc::get_mut_unchecked(&mut rc1).push_str("x"); + } + } + + #[kani::proof_for_contract(Rc::::get_mut_unchecked)] + fn harness_get_mut_unchecked_with_weak_dormant() { + let mut rc: Rc = Rc::new(String::new()); + let weak = Rc::downgrade(&rc); + + unsafe { + Rc::get_mut_unchecked(&mut rc).push_str("x"); + } + } + + #[kani::proof_for_contract(Rc::<()>::get_mut_unchecked)] + pub fn harness_get_mut_unchecked_unit() { + let value: () = kani::any(); + let replacement: () = kani::any(); + let mut rc: Rc<()> = Rc::new(value); + + unsafe { + *Rc::get_mut_unchecked(&mut rc) = replacement; + } + } + + #[kani::proof_for_contract(Rc::<[u8; 4]>::get_mut_unchecked)] + pub fn harness_get_mut_unchecked_array4_u8() { + let value: [u8; 4] = kani::any(); + let replacement: [u8; 4] = kani::any(); + let mut rc: Rc<[u8; 4]> = Rc::new(value); + + unsafe { + *Rc::get_mut_unchecked(&mut rc) = replacement; + } + } + + #[kani::proof_for_contract(Rc::<[u8]>::get_mut_unchecked)] + pub fn harness_get_mut_unchecked_unsized_slice_u8() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let mut rc = Rc::new(slice); + + let replacement_vec = verifier_nondet_vec::(); + let replacement_slice = nondet_rc_slice(&replacement_vec); + + unsafe { + *Rc::get_mut_unchecked(&mut rc) = replacement_slice; + } + } + + #[kani::proof_for_contract(Rc::<[u16]>::get_mut_unchecked)] + pub fn harness_get_mut_unchecked_unsized_slice_u16() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let mut rc = Rc::new(slice); + + let replacement_vec = verifier_nondet_vec::(); + let replacement_slice = nondet_rc_slice(&replacement_vec); + + unsafe { + *Rc::get_mut_unchecked(&mut rc) = replacement_slice; + } + } + + #[kani::proof_for_contract(Rc::<[u32]>::get_mut_unchecked)] + pub fn harness_get_mut_unchecked_unsized_slice_u32() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let mut rc = Rc::new(slice); + + let replacement_vec = verifier_nondet_vec::(); + let replacement_slice = nondet_rc_slice(&replacement_vec); + + unsafe { + *Rc::get_mut_unchecked(&mut rc) = replacement_slice; + } + } +} + +#[cfg(kani)] +mod verify_2216 { + use super::*; + + #[kani::proof_for_contract(Rc::downcast_unchecked::)] + pub fn harness_downcast_unchecked_i32() { + let value: i32 = kani::any(); + let rc_dyn: Rc = Rc::new(value); + let _downcasted: Rc = unsafe { rc_dyn.downcast_unchecked::() }; + } + + #[kani::proof_for_contract(Rc::downcast_unchecked::)] + pub fn harness_downcast_unchecked_bool() { + let value: bool = kani::any(); + let rc_dyn: Rc = Rc::new(value); + let _downcasted: Rc = unsafe { rc_dyn.downcast_unchecked::() }; + } + + #[kani::proof_for_contract(Rc::downcast_unchecked::<()>)] + pub fn harness_downcast_unchecked_unit() { + let value: () = kani::any(); + let rc_dyn: Rc = Rc::new(value); + let _downcasted: Rc<()> = unsafe { rc_dyn.downcast_unchecked() }; + } +} + +#[cfg(kani)] +mod verify_3369 { + use super::kani_rc_harness_helpers::*; + use super::*; + + #[kani::proof_for_contract(Weak::::from_raw)] + pub fn harness_weak_from_raw_i32() { + let value: i32 = kani::any(); + let strong: Rc = Rc::new(value); + let weak: Weak = Rc::downgrade(&strong); + let ptr: *const i32 = weak.into_raw(); + let _recovered: Weak = unsafe { Weak::from_raw(ptr) }; + } + + #[kani::proof_for_contract(Weak::::from_raw)] + pub fn harness_weak_from_raw_u64() { + let value: u64 = kani::any(); + let strong: Rc = Rc::new(value); + let weak: Weak = Rc::downgrade(&strong); + let ptr: *const u64 = weak.into_raw(); + let _recovered: Weak = unsafe { Weak::from_raw(ptr) }; + } + + #[kani::proof_for_contract(Weak::::from_raw)] + pub fn harness_weak_from_raw_bool() { + let value: bool = kani::any(); + let strong: Rc = Rc::new(value); + let weak: Weak = Rc::downgrade(&strong); + let ptr: *const bool = weak.into_raw(); + let _recovered: Weak = unsafe { Weak::from_raw(ptr) }; + } + + #[kani::proof_for_contract(Weak::<()>::from_raw)] + pub fn harness_weak_from_raw_unit() { + let value: () = kani::any(); + let strong: Rc<()> = Rc::new(value); + let weak: Weak<()> = Rc::downgrade(&strong); + let ptr: *const () = weak.into_raw(); + let _recovered: Weak<()> = unsafe { Weak::from_raw(ptr) }; + } + + #[kani::proof_for_contract(Weak::<[u8; 4]>::from_raw)] + pub fn harness_weak_from_raw_array4_u8() { + let value: [u8; 4] = kani::any(); + let strong: Rc<[u8; 4]> = Rc::new(value); + let weak: Weak<[u8; 4]> = Rc::downgrade(&strong); + let ptr: *const [u8; 4] = weak.into_raw(); + let _recovered: Weak<[u8; 4]> = unsafe { Weak::from_raw(ptr) }; + } + + #[kani::proof_for_contract(Weak::<[u8]>::from_raw)] + pub fn harness_weak_from_raw_unsized_slice_u8() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let strong = Rc::new(slice); + let weak = Rc::downgrade(&strong); + let ptr = weak.into_raw(); + let _recovered = unsafe { Weak::from_raw(ptr) }; + } + + #[kani::proof_for_contract(Weak::<[u16]>::from_raw)] + pub fn harness_weak_from_raw_unsized_slice_u16() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let strong = Rc::new(slice); + let weak = Rc::downgrade(&strong); + let ptr = weak.into_raw(); + let _recovered = unsafe { Weak::from_raw(ptr) }; + } + + #[kani::proof_for_contract(Weak::<[u32]>::from_raw)] + pub fn harness_weak_from_raw_unsized_slice_u32() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let strong = Rc::new(slice); + let weak = Rc::downgrade(&strong); + let ptr = weak.into_raw(); + let _recovered = unsafe { Weak::from_raw(ptr) }; + } +} + +#[cfg(kani)] +mod verify_3588 { + use super::kani_rc_harness_helpers::*; + use super::*; + + #[kani::proof_for_contract(Weak::::from_raw_in)] + pub fn harness_weak_from_raw_in_i32_global_live() { + let value: i32 = kani::any(); + let strong: Rc = Rc::new_in(value, Global); + let weak: Weak = Rc::downgrade(&strong); + let (ptr, alloc): (*const i32, Global) = weak.into_raw_with_allocator(); + let _recovered: Weak = unsafe { Weak::from_raw_in(ptr, alloc) }; + } + + #[kani::proof_for_contract(Weak::::from_raw_in)] + pub fn harness_weak_from_raw_in_bool_global_live() { + let value: bool = kani::any(); + let strong: Rc = Rc::new_in(value, Global); + let weak: Weak = Rc::downgrade(&strong); + let (ptr, alloc): (*const bool, Global) = weak.into_raw_with_allocator(); + let _recovered: Weak = unsafe { Weak::from_raw_in(ptr, alloc) }; + } + + #[kani::proof_for_contract(Weak::<(), Global>::from_raw_in)] + pub fn harness_weak_from_raw_in_unit_global_live() { + let value: () = kani::any(); + let strong: Rc<(), Global> = Rc::new_in(value, Global); + let weak: Weak<(), Global> = Rc::downgrade(&strong); + let (ptr, alloc): (*const (), Global) = weak.into_raw_with_allocator(); + let _recovered: Weak<(), Global> = unsafe { Weak::from_raw_in(ptr, alloc) }; + } + + #[kani::proof_for_contract(Weak::<[u8; 4], Global>::from_raw_in)] + pub fn harness_weak_from_raw_in_array4_u8_global_live() { + let value: [u8; 4] = kani::any(); + let strong: Rc<[u8; 4], Global> = Rc::new_in(value, Global); + let weak: Weak<[u8; 4], Global> = Rc::downgrade(&strong); + let (ptr, alloc): (*const [u8; 4], Global) = weak.into_raw_with_allocator(); + let _recovered: Weak<[u8; 4], Global> = unsafe { Weak::from_raw_in(ptr, alloc) }; + } + + #[kani::proof_for_contract(Weak::<[u8], Global>::from_raw_in)] + pub fn harness_weak_from_raw_in_unsized_slice_u8_global_live() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let strong = Rc::new_in(slice, Global); + let weak = Rc::downgrade(&strong); + let (ptr, alloc) = weak.into_raw_with_allocator(); + let _recovered = unsafe { Weak::from_raw_in(ptr, alloc) }; + } + + #[kani::proof_for_contract(Weak::<[u16], Global>::from_raw_in)] + pub fn harness_weak_from_raw_in_unsized_slice_u16_global_live() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let strong = Rc::new_in(slice, Global); + let weak = Rc::downgrade(&strong); + let (ptr, alloc) = weak.into_raw_with_allocator(); + let _recovered = unsafe { Weak::from_raw_in(ptr, alloc) }; + } + + #[kani::proof_for_contract(Weak::<[u32], Global>::from_raw_in)] + pub fn harness_weak_from_raw_in_unsized_slice_u32_global_live() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let strong = Rc::new_in(slice, Global); + let weak = Rc::downgrade(&strong); + let (ptr, alloc) = weak.into_raw_with_allocator(); + let _recovered = unsafe { Weak::from_raw_in(ptr, alloc) }; + } +} + +// === SAFE FUNCTIONS (50 of 54) === + +#[cfg(kani)] +mod verify_1964 { + use super::kani_rc_harness_helpers::*; + use super::*; + use core::any::Any; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + #[kani::proof] + pub fn harness_get_mut_i32_unique_some() { + let value: i32 = kani::any(); + let mut rc: Rc = Rc::new_in(value, Global); + let _ = Rc::::get_mut(&mut rc); + } + + #[kani::proof] + pub fn harness_get_mut_i32_shared_none() { + let value: i32 = kani::any(); + let mut rc: Rc = Rc::new_in(value, Global); + let shared: Rc = Rc::clone(&rc); + let _ = Rc::::get_mut(&mut rc); + drop(shared); + } + + #[kani::proof] + pub fn harness_get_mut_i32_weak_present_none() { + let value: i32 = kani::any(); + let mut rc: Rc = Rc::new_in(value, Global); + let weak: Weak = Rc::downgrade(&rc); + let _ = Rc::::get_mut(&mut rc); + drop(weak); + } + + #[kani::proof] + pub fn harness_get_mut_unit_unique_some() { + let mut rc: Rc<(), Global> = Rc::new_in((), Global); + let _ = Rc::<(), Global>::get_mut(&mut rc); + } + + #[kani::proof] + pub fn harness_get_mut_unit_shared_none() { + let mut rc: Rc<(), Global> = Rc::new_in((), Global); + let shared: Rc<(), Global> = Rc::clone(&rc); + let _ = Rc::<(), Global>::get_mut(&mut rc); + drop(shared); + } + + #[kani::proof] + pub fn harness_get_mut_unit_weak_present_none() { + let mut rc: Rc<(), Global> = Rc::new_in((), Global); + let weak: Weak<(), Global> = Rc::downgrade(&rc); + let _ = Rc::<(), Global>::get_mut(&mut rc); + drop(weak); + } + + #[kani::proof] + pub fn harness_get_mut_drop_sentinel_unique_some() { + let value = DropSentinel(kani::any()); + let mut rc: Rc = Rc::new_in(value, Global); + let _ = Rc::::get_mut(&mut rc); + } + + #[kani::proof] + pub fn harness_get_mut_drop_sentinel_shared_none() { + let value = DropSentinel(kani::any()); + let mut rc: Rc = Rc::new_in(value, Global); + let shared: Rc = Rc::clone(&rc); + let _ = Rc::::get_mut(&mut rc); + drop(shared); + } + + #[kani::proof] + pub fn harness_get_mut_drop_sentinel_weak_present_none() { + let value = DropSentinel(kani::any()); + let mut rc: Rc = Rc::new_in(value, Global); + let weak: Weak = Rc::downgrade(&rc); + let _ = Rc::::get_mut(&mut rc); + drop(weak); + } + + #[kani::proof] + pub fn harness_get_mut_arr3_unique_some() { + let value: [u8; 3] = kani::any(); + let mut rc: Rc<[u8; 3], Global> = Rc::new_in(value, Global); + let _ = Rc::<[u8; 3], Global>::get_mut(&mut rc); + } + + #[kani::proof] + pub fn harness_get_mut_arr3_shared_none() { + let value: [u8; 3] = kani::any(); + let mut rc: Rc<[u8; 3], Global> = Rc::new_in(value, Global); + let shared: Rc<[u8; 3], Global> = Rc::clone(&rc); + let _ = Rc::<[u8; 3], Global>::get_mut(&mut rc); + drop(shared); + } + + #[kani::proof] + pub fn harness_get_mut_arr3_weak_present_none() { + let value: [u8; 3] = kani::any(); + let mut rc: Rc<[u8; 3], Global> = Rc::new_in(value, Global); + let weak: Weak<[u8; 3], Global> = Rc::downgrade(&rc); + let _ = Rc::<[u8; 3], Global>::get_mut(&mut rc); + drop(weak); + } + + #[kani::proof] + pub fn harness_get_mut_slice_u8_unique_some() { + let values: [u8; 3] = kani::any(); + let mut rc: Rc<[u8], Global> = Rc::from(values); + let _ = Rc::<[u8], Global>::get_mut(&mut rc); + } + + #[kani::proof] + pub fn harness_get_mut_slice_u8_shared_none() { + let values: [u8; 3] = kani::any(); + let mut rc: Rc<[u8], Global> = Rc::from(values); + let shared: Rc<[u8], Global> = Rc::clone(&rc); + let _ = Rc::<[u8], Global>::get_mut(&mut rc); + drop(shared); + } + + #[kani::proof] + pub fn harness_get_mut_slice_u8_weak_present_none() { + let values: [u8; 3] = kani::any(); + let mut rc: Rc<[u8], Global> = Rc::from(values); + let weak: Weak<[u8], Global> = Rc::downgrade(&rc); + let _ = Rc::<[u8], Global>::get_mut(&mut rc); + drop(weak); + } + + #[kani::proof] + pub fn harness_get_mut_str_unique_some() { + let mut rc: Rc = Rc::from("seed"); + let _ = Rc::::get_mut(&mut rc); + } + + #[kani::proof] + pub fn harness_get_mut_str_shared_none() { + let mut rc: Rc = Rc::from("seed"); + let shared: Rc = Rc::clone(&rc); + let _ = Rc::::get_mut(&mut rc); + drop(shared); + } + + #[kani::proof] + pub fn harness_get_mut_str_weak_present_none() { + let mut rc: Rc = Rc::from("seed"); + let weak: Weak = Rc::downgrade(&rc); + let _ = Rc::::get_mut(&mut rc); + drop(weak); + } + + #[kani::proof] + pub fn harness_get_mut_dyn_any_i32_unique_some() { + let value: i32 = kani::any(); + let rc_i32: Rc = Rc::new_in(value, Global); + let mut rc: Rc = rc_i32; + let _ = Rc::::get_mut(&mut rc); + } + + #[kani::proof] + pub fn harness_get_mut_dyn_any_i32_shared_none() { + let value: i32 = kani::any(); + let rc_i32: Rc = Rc::new_in(value, Global); + let mut rc: Rc = rc_i32; + let shared: Rc = Rc::clone(&rc); + let _ = Rc::::get_mut(&mut rc); + drop(shared); + } + + #[kani::proof] + pub fn harness_get_mut_dyn_any_i32_weak_present_none() { + let value: i32 = kani::any(); + let rc_i32: Rc = Rc::new_in(value, Global); + let mut rc: Rc = rc_i32; + let weak: Weak = Rc::downgrade(&rc); + let _ = Rc::::get_mut(&mut rc); + drop(weak); + } + + #[kani::proof] + pub fn harness_get_mut_unsized_slice_u8() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let mut rc = Rc::new_in(slice, Global); + let _ = Rc::get_mut(&mut rc); + } + + #[kani::proof] + pub fn harness_get_mut_unsized_slice_u16() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let mut rc = Rc::new_in(slice, Global); + let _ = Rc::get_mut(&mut rc); + } + + #[kani::proof] + pub fn harness_get_mut_unsized_slice_u32() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let mut rc = Rc::new_in(slice, Global); + let _ = Rc::get_mut(&mut rc); + } +} + +#[cfg(kani)] +mod verify_2118 { + use super::kani_rc_harness_helpers::*; + use super::*; + + #[derive(Clone)] + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + #[kani::proof] + pub fn harness_make_mut_i32_unique() { + let value: i32 = kani::any(); + let mut rc: Rc = Rc::new_in(value, Global); + let _ = Rc::::make_mut(&mut rc); + } + + #[kani::proof] + pub fn harness_make_mut_i32_shared() { + let value: i32 = kani::any(); + let mut rc: Rc = Rc::new_in(value, Global); + let shared: Rc = Rc::clone(&rc); + let _ = Rc::::make_mut(&mut rc); + drop(shared); + } + + #[kani::proof] + pub fn harness_make_mut_i32_weak_present() { + let value: i32 = kani::any(); + let mut rc: Rc = Rc::new_in(value, Global); + let weak: Weak = Rc::downgrade(&rc); + let _ = Rc::::make_mut(&mut rc); + drop(weak); + } + + #[kani::proof] + pub fn harness_make_mut_unit_unique() { + let mut rc: Rc<(), Global> = Rc::new_in((), Global); + let _ = Rc::<(), Global>::make_mut(&mut rc); + } + + #[kani::proof] + pub fn harness_make_mut_unit_shared() { + let mut rc: Rc<(), Global> = Rc::new_in((), Global); + let shared: Rc<(), Global> = Rc::clone(&rc); + let _ = Rc::<(), Global>::make_mut(&mut rc); + drop(shared); + } + + #[kani::proof] + pub fn harness_make_mut_unit_weak_present() { + let mut rc: Rc<(), Global> = Rc::new_in((), Global); + let weak: Weak<(), Global> = Rc::downgrade(&rc); + let _ = Rc::<(), Global>::make_mut(&mut rc); + drop(weak); + } + + #[kani::proof] + pub fn harness_make_mut_drop_sentinel_unique() { + let value = DropSentinel(kani::any()); + let mut rc: Rc = Rc::new_in(value, Global); + let _ = Rc::::make_mut(&mut rc); + } + + #[kani::proof] + pub fn harness_make_mut_drop_sentinel_shared() { + let value = DropSentinel(kani::any()); + let mut rc: Rc = Rc::new_in(value, Global); + let shared: Rc = Rc::clone(&rc); + let _ = Rc::::make_mut(&mut rc); + drop(shared); + } + + #[kani::proof] + pub fn harness_make_mut_drop_sentinel_weak_present() { + let value = DropSentinel(kani::any()); + let mut rc: Rc = Rc::new_in(value, Global); + let weak: Weak = Rc::downgrade(&rc); + let _ = Rc::::make_mut(&mut rc); + drop(weak); + } + + #[kani::proof] + pub fn harness_make_mut_arr3_unique() { + let value: [u8; 3] = kani::any(); + let mut rc: Rc<[u8; 3], Global> = Rc::new_in(value, Global); + let _ = Rc::<[u8; 3], Global>::make_mut(&mut rc); + } + + #[kani::proof] + pub fn harness_make_mut_arr3_shared() { + let value: [u8; 3] = kani::any(); + let mut rc: Rc<[u8; 3], Global> = Rc::new_in(value, Global); + let shared: Rc<[u8; 3], Global> = Rc::clone(&rc); + let _ = Rc::<[u8; 3], Global>::make_mut(&mut rc); + drop(shared); + } + + #[kani::proof] + pub fn harness_make_mut_arr3_weak_present() { + let value: [u8; 3] = kani::any(); + let mut rc: Rc<[u8; 3], Global> = Rc::new_in(value, Global); + let weak: Weak<[u8; 3], Global> = Rc::downgrade(&rc); + let _ = Rc::<[u8; 3], Global>::make_mut(&mut rc); + drop(weak); + } + + #[kani::proof] + pub fn harness_make_mut_str_unique() { + let mut rc: Rc = Rc::from("seed"); + let _ = Rc::::make_mut(&mut rc); + } + + #[kani::proof] + pub fn harness_make_mut_str_shared() { + let mut rc: Rc = Rc::from("seed"); + let shared: Rc = Rc::clone(&rc); + let _ = Rc::::make_mut(&mut rc); + drop(shared); + } + + #[kani::proof] + pub fn harness_make_mut_str_weak_present() { + let mut rc: Rc = Rc::from("seed"); + let weak: Weak = Rc::downgrade(&rc); + let _ = Rc::::make_mut(&mut rc); + drop(weak); + } + + #[kani::proof] + pub fn harness_make_mut_unsized_slice_u8() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let mut rc = Rc::new_in(slice, Global); + let _ = Rc::make_mut(&mut rc); + } + + #[kani::proof] + pub fn harness_make_mut_unsized_slice_u16() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let mut rc = Rc::new_in(slice, Global); + let _ = Rc::make_mut(&mut rc); + } + + #[kani::proof] + pub fn harness_make_mut_unsized_slice_u32() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let mut rc = Rc::new_in(slice, Global); + let _ = Rc::make_mut(&mut rc); + } +} + +#[cfg(kani)] +mod verify_2230 { + use super::*; + + #[kani::proof] + pub fn harness_downcast_i32_success() { + let value: i32 = kani::any(); + let rc_i32: Rc = Rc::new_in(value, Global); + let rc_any: Rc = rc_i32; + let _ = Rc::::downcast::(rc_any); + } + + #[kani::proof] + pub fn harness_downcast_i32_failure() { + let value: bool = kani::any(); + let rc_bool: Rc = Rc::new_in(value, Global); + let rc_any: Rc = rc_bool; + let _ = Rc::::downcast::(rc_any); + } + + #[kani::proof] + pub fn harness_downcast_string_success() { + let rc_string: Rc = Rc::new_in(String::from("seed"), Global); + let rc_any: Rc = rc_string; + let result = Rc::::downcast::(rc_any); + core::mem::forget(result); + } + + #[kani::proof] + pub fn harness_downcast_string_failure() { + let value: i32 = kani::any(); + let rc_i32: Rc = Rc::new_in(value, Global); + let rc_any: Rc = rc_i32; + let _ = Rc::::downcast::(rc_any); + } +} + +#[cfg(kani)] +mod verify_2342 { + use super::kani_rc_harness_helpers::*; + use super::*; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + #[kani::proof] + pub fn harness_from_box_in_i32() { + let value: i32 = kani::any(); + let src: Box = Box::new_in(value, Global); + let _ = Rc::::from_box_in(src); + } + + #[kani::proof] + pub fn harness_from_box_in_unit() { + let src: Box<(), Global> = Box::new_in((), Global); + let _ = Rc::<(), Global>::from_box_in(src); + } + + #[kani::proof] + pub fn harness_from_box_in_drop_sentinel() { + let src: Box = Box::new_in(DropSentinel(kani::any()), Global); + let _ = Rc::::from_box_in(src); + } + + #[kani::proof] + pub fn harness_from_box_in_arr3() { + let value: [u8; 3] = kani::any(); + let src: Box<[u8; 3], Global> = Box::new_in(value, Global); + let _ = Rc::<[u8; 3], Global>::from_box_in(src); + } + + #[kani::proof] + pub fn harness_from_box_in_arr0() { + let src: Box<[u8; 0], Global> = Box::new_in([], Global); + let _ = Rc::<[u8; 0], Global>::from_box_in(src); + } + + #[kani::proof] + pub fn harness_from_box_in_dyn_any_i32() { + let value: i32 = kani::any(); + let boxed_i32: Box = Box::new_in(value, Global); + let src: Box = boxed_i32; + let _ = Rc::::from_box_in(src); + } + + #[kani::proof] + pub fn harness_from_box_in_unsized_slice_u8() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let src = Box::new_in(slice, Global); + let _ = Rc::from_box_in(src); + } + + #[kani::proof] + pub fn harness_from_box_in_unsized_slice_u16() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let src = Box::new_in(slice, Global); + let _ = Rc::from_box_in(src); + } + + #[kani::proof] + pub fn harness_from_box_in_unsized_slice_u32() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let src = Box::new_in(slice, Global); + let _ = Rc::from_box_in(src); + } +} + +#[cfg(kani)] +mod verify_3511 { + use crate::vec; + + use super::kani_rc_harness_helpers::*; + use super::*; + use core::any::Any; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + #[kani::proof] + pub fn harness_weak_as_ptr_u8_live_global() { + let value: u8 = kani::any(); + let strong: Rc = Rc::new_in(value, Global); + let weak: Weak = Rc::downgrade(&strong); + let _ptr: *const u8 = Weak::::as_ptr(&weak); + } + + #[kani::proof] + pub fn harness_weak_as_ptr_u8_dangling_global() { + let weak: Weak = Weak::new_in(Global); + let _ptr: *const u8 = Weak::::as_ptr(&weak); + } + + #[kani::proof] + pub fn harness_weak_as_ptr_i32_live_global() { + let value: i32 = kani::any(); + let strong: Rc = Rc::new_in(value, Global); + let weak: Weak = Rc::downgrade(&strong); + let _ptr: *const i32 = Weak::::as_ptr(&weak); + } + + #[kani::proof] + pub fn harness_weak_as_ptr_i32_dangling_global() { + let weak: Weak = Weak::new_in(Global); + let _ptr: *const i32 = Weak::::as_ptr(&weak); + } + + #[kani::proof] + pub fn harness_weak_as_ptr_u64_live_global() { + let value: u64 = kani::any(); + let strong: Rc = Rc::new_in(value, Global); + let weak: Weak = Rc::downgrade(&strong); + let _ptr: *const u64 = Weak::::as_ptr(&weak); + } + + #[kani::proof] + pub fn harness_weak_as_ptr_u64_dangling_global() { + let weak: Weak = Weak::new_in(Global); + let _ptr: *const u64 = Weak::::as_ptr(&weak); + } + + #[kani::proof] + pub fn harness_weak_as_ptr_unit_live_global() { + let strong: Rc<(), Global> = Rc::new_in((), Global); + let weak: Weak<(), Global> = Rc::downgrade(&strong); + let _ptr: *const () = Weak::<(), Global>::as_ptr(&weak); + } + + #[kani::proof] + pub fn harness_weak_as_ptr_unit_dangling_global() { + let weak: Weak<(), Global> = Weak::new_in(Global); + let _ptr: *const () = Weak::<(), Global>::as_ptr(&weak); + } + + #[kani::proof] + pub fn harness_weak_as_ptr_drop_sentinel_live_global() { + let strong: Rc = Rc::new_in(DropSentinel(kani::any()), Global); + let weak: Weak = Rc::downgrade(&strong); + let _ptr: *const DropSentinel = Weak::::as_ptr(&weak); + } + + #[kani::proof] + pub fn harness_weak_as_ptr_drop_sentinel_dangling_global() { + let weak: Weak = Weak::new_in(Global); + let _ptr: *const DropSentinel = Weak::::as_ptr(&weak); + } + + #[kani::proof] + pub fn harness_weak_as_ptr_arr3_live_global() { + let value: [u8; 3] = kani::any(); + let strong: Rc<[u8; 3], Global> = Rc::new_in(value, Global); + let weak: Weak<[u8; 3], Global> = Rc::downgrade(&strong); + let _ptr: *const [u8; 3] = Weak::<[u8; 3], Global>::as_ptr(&weak); + } + + #[kani::proof] + pub fn harness_weak_as_ptr_arr3_dangling_global() { + let weak: Weak<[u8; 3], Global> = Weak::new_in(Global); + let _ptr: *const [u8; 3] = Weak::<[u8; 3], Global>::as_ptr(&weak); + } + + #[kani::proof] + pub fn harness_weak_as_ptr_bool_live_global() { + let value: bool = kani::any(); + let strong: Rc = Rc::new_in(value, Global); + let weak: Weak = Rc::downgrade(&strong); + let _ptr: *const bool = Weak::::as_ptr(&weak); + } + + #[kani::proof] + pub fn harness_weak_as_ptr_bool_dangling_global() { + let weak: Weak = Weak::new_in(Global); + let _ptr: *const bool = Weak::::as_ptr(&weak); + } + + #[kani::proof] + pub fn harness_weak_as_ptr_nested_rc_i32_live_global() { + let nested: Rc = Rc::new(kani::any::()); + let strong: Rc, Global> = Rc::new_in(nested, Global); + let weak: Weak, Global> = Rc::downgrade(&strong); + let _ptr: *const Rc = Weak::, Global>::as_ptr(&weak); + } + + #[kani::proof] + pub fn harness_weak_as_ptr_nested_rc_i32_dangling_global() { + let weak: Weak, Global> = Weak::new_in(Global); + let _ptr: *const Rc = Weak::, Global>::as_ptr(&weak); + } + + #[kani::proof] + pub fn harness_weak_as_ptr_tuple_i32_string_live_global() { + let value: (i32, String) = (kani::any(), String::new()); + let strong: Rc<(i32, String), Global> = Rc::new_in(value, Global); + let weak: Weak<(i32, String), Global> = Rc::downgrade(&strong); + let _ptr: *const (i32, String) = Weak::<(i32, String), Global>::as_ptr(&weak); + } + + #[kani::proof] + pub fn harness_weak_as_ptr_tuple_i32_string_dangling_global() { + let weak: Weak<(i32, String), Global> = Weak::new_in(Global); + let _ptr: *const (i32, String) = Weak::<(i32, String), Global>::as_ptr(&weak); + } + + #[kani::proof] + pub fn harness_weak_as_ptr_option_i32_live_global() { + let value: Option = kani::any(); + let strong: Rc, Global> = Rc::new_in(value, Global); + let weak: Weak, Global> = Rc::downgrade(&strong); + let _ptr: *const Option = Weak::, Global>::as_ptr(&weak); + } + + #[kani::proof] + pub fn harness_weak_as_ptr_option_i32_dangling_global() { + let weak: Weak, Global> = Weak::new_in(Global); + let _ptr: *const Option = Weak::, Global>::as_ptr(&weak); + } + + #[kani::proof] + pub fn harness_weak_as_ptr_dyn_any_i32_live_global() { + let value: i32 = kani::any(); + let strong_i32: Rc = Rc::new_in(value, Global); + let strong: Rc = strong_i32; + let weak: Weak = Rc::downgrade(&strong); + let _ptr: *const dyn Any = Weak::::as_ptr(&weak); + } + + #[kani::proof] + pub fn harness_weak_as_ptr_dyn_any_i32_dangling_global() { + let weak_i32: Weak = Weak::new_in(Global); + let weak: Weak = weak_i32; + let _ptr: *const dyn Any = Weak::::as_ptr(&weak); + } + + #[kani::proof] + pub fn harness_weak_as_ptr_unsized_slice_u8_live_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let strong = Rc::new_in(slice, Global); + let weak = Rc::downgrade(&strong); + let _ptr = Weak::as_ptr(&weak); + } + + #[kani::proof] + pub fn harness_weak_as_ptr_unsized_slice_u16_live_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let strong = Rc::new_in(slice, Global); + let weak = Rc::downgrade(&strong); + let _ptr = Weak::as_ptr(&weak); + } + + #[kani::proof] + pub fn harness_weak_as_ptr_unsized_slice_u32_live_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let strong = Rc::new_in(slice, Global); + let weak = Rc::downgrade(&strong); + let _ptr = Weak::as_ptr(&weak); + } +} + +#[cfg(kani)] +mod verify_3558 { + use super::kani_rc_harness_helpers::*; + use super::*; + use core::any::Any; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + #[kani::proof] + pub fn harness_weak_into_raw_with_allocator_u8_live_global() { + let value: u8 = kani::any(); + let strong: Rc = Rc::new_in(value, Global); + let weak: Weak = Rc::downgrade(&strong); + let (ptr, alloc): (*const u8, Global) = Weak::::into_raw_with_allocator(weak); + let _recovered: Weak = unsafe { Weak::::from_raw_in(ptr, alloc) }; + } + + #[kani::proof] + pub fn harness_weak_into_raw_with_allocator_u8_dangling_global() { + let weak: Weak = Weak::new_in(Global); + let (ptr, alloc): (*const u8, Global) = Weak::::into_raw_with_allocator(weak); + let _recovered: Weak = unsafe { Weak::::from_raw_in(ptr, alloc) }; + } + + #[kani::proof] + pub fn harness_weak_into_raw_with_allocator_i32_live_global() { + let value: i32 = kani::any(); + let strong: Rc = Rc::new_in(value, Global); + let weak: Weak = Rc::downgrade(&strong); + let (ptr, alloc): (*const i32, Global) = Weak::::into_raw_with_allocator(weak); + let _recovered: Weak = unsafe { Weak::::from_raw_in(ptr, alloc) }; + } + + #[kani::proof] + pub fn harness_weak_into_raw_with_allocator_i32_dangling_global() { + let weak: Weak = Weak::new_in(Global); + let (ptr, alloc): (*const i32, Global) = Weak::::into_raw_with_allocator(weak); + let _recovered: Weak = unsafe { Weak::::from_raw_in(ptr, alloc) }; + } + + #[kani::proof] + pub fn harness_weak_into_raw_with_allocator_u64_live_global() { + let value: u64 = kani::any(); + let strong: Rc = Rc::new_in(value, Global); + let weak: Weak = Rc::downgrade(&strong); + let (ptr, alloc): (*const u64, Global) = Weak::::into_raw_with_allocator(weak); + let _recovered: Weak = unsafe { Weak::::from_raw_in(ptr, alloc) }; + } + + #[kani::proof] + pub fn harness_weak_into_raw_with_allocator_u64_dangling_global() { + let weak: Weak = Weak::new_in(Global); + let (ptr, alloc): (*const u64, Global) = Weak::::into_raw_with_allocator(weak); + let _recovered: Weak = unsafe { Weak::::from_raw_in(ptr, alloc) }; + } + + #[kani::proof] + pub fn harness_weak_into_raw_with_allocator_unit_live_global() { + let strong: Rc<(), Global> = Rc::new_in((), Global); + let weak: Weak<(), Global> = Rc::downgrade(&strong); + let (ptr, alloc): (*const (), Global) = Weak::<(), Global>::into_raw_with_allocator(weak); + let _recovered: Weak<(), Global> = unsafe { Weak::<(), Global>::from_raw_in(ptr, alloc) }; + } + + #[kani::proof] + pub fn harness_weak_into_raw_with_allocator_unit_dangling_global() { + let weak: Weak<(), Global> = Weak::new_in(Global); + let (ptr, alloc): (*const (), Global) = Weak::<(), Global>::into_raw_with_allocator(weak); + let _recovered: Weak<(), Global> = unsafe { Weak::<(), Global>::from_raw_in(ptr, alloc) }; + } + + #[kani::proof] + pub fn harness_weak_into_raw_with_allocator_drop_sentinel_live_global() { + let value = DropSentinel(kani::any()); + let strong: Rc = Rc::new_in(value, Global); + let weak: Weak = Rc::downgrade(&strong); + let (ptr, alloc): (*const DropSentinel, Global) = + Weak::::into_raw_with_allocator(weak); + let _recovered: Weak = + unsafe { Weak::::from_raw_in(ptr, alloc) }; + } + + #[kani::proof] + pub fn harness_weak_into_raw_with_allocator_drop_sentinel_dangling_global() { + let weak: Weak = Weak::new_in(Global); + let (ptr, alloc): (*const DropSentinel, Global) = + Weak::::into_raw_with_allocator(weak); + let _recovered: Weak = + unsafe { Weak::::from_raw_in(ptr, alloc) }; + } + + #[kani::proof] + pub fn harness_weak_into_raw_with_allocator_arr3_live_global() { + let value: [u8; 3] = kani::any(); + let strong: Rc<[u8; 3], Global> = Rc::new_in(value, Global); + let weak: Weak<[u8; 3], Global> = Rc::downgrade(&strong); + let (ptr, alloc): (*const [u8; 3], Global) = + Weak::<[u8; 3], Global>::into_raw_with_allocator(weak); + let _recovered: Weak<[u8; 3], Global> = + unsafe { Weak::<[u8; 3], Global>::from_raw_in(ptr, alloc) }; + } + + #[kani::proof] + pub fn harness_weak_into_raw_with_allocator_arr3_dangling_global() { + let weak: Weak<[u8; 3], Global> = Weak::new_in(Global); + let (ptr, alloc): (*const [u8; 3], Global) = + Weak::<[u8; 3], Global>::into_raw_with_allocator(weak); + let _recovered: Weak<[u8; 3], Global> = + unsafe { Weak::<[u8; 3], Global>::from_raw_in(ptr, alloc) }; + } + + #[kani::proof] + pub fn harness_weak_into_raw_with_allocator_str_live_global() { + let strong: Rc = Rc::from("seed"); + let weak: Weak = Rc::downgrade(&strong); + let (ptr, alloc): (*const str, Global) = Weak::::into_raw_with_allocator(weak); + let _recovered: Weak = unsafe { Weak::::from_raw_in(ptr, alloc) }; + } + + #[kani::proof] + pub fn harness_weak_into_raw_with_allocator_str_after_drop_global() { + let strong: Rc = Rc::from("seed"); + let weak: Weak = Rc::downgrade(&strong); + drop(strong); + let (ptr, alloc): (*const str, Global) = Weak::::into_raw_with_allocator(weak); + let recovered: Weak = unsafe { Weak::::from_raw_in(ptr, alloc) }; + assert!(recovered.upgrade().is_none()); + } + + #[kani::proof] + pub fn harness_weak_into_raw_with_allocator_dyn_any_i32_live_global() { + let value: i32 = kani::any(); + let strong_i32: Rc = Rc::new_in(value, Global); + let strong: Rc = strong_i32; + let weak: Weak = Rc::downgrade(&strong); + let (ptr, alloc): (*const dyn Any, Global) = + Weak::::into_raw_with_allocator(weak); + let _recovered: Weak = + unsafe { Weak::::from_raw_in(ptr, alloc) }; + } + + #[kani::proof] + pub fn harness_weak_into_raw_with_allocator_dyn_any_i32_dangling_global() { + let weak_i32: Weak = Weak::new_in(Global); + let weak: Weak = weak_i32; + let (ptr, alloc): (*const dyn Any, Global) = + Weak::::into_raw_with_allocator(weak); + let _recovered: Weak = + unsafe { Weak::::from_raw_in(ptr, alloc) }; + } + + #[kani::proof] + pub fn harness_weak_into_raw_with_allocator_unsized_slice_u8_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let strong = Rc::new_in(slice, Global); + let weak = Rc::downgrade(&strong); + let (ptr, alloc) = Weak::into_raw_with_allocator(weak); + let _recovered = unsafe { Weak::from_raw_in(ptr, alloc) }; + } + + #[kani::proof] + pub fn harness_weak_into_raw_with_allocator_unsized_slice_u16_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let strong = Rc::new_in(slice, Global); + let weak = Rc::downgrade(&strong); + let (ptr, alloc) = Weak::into_raw_with_allocator(weak); + let _recovered = unsafe { Weak::from_raw_in(ptr, alloc) }; + } + + #[kani::proof] + pub fn harness_weak_into_raw_with_allocator_unsized_slice_u32_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let strong = Rc::new_in(slice, Global); + let weak = Rc::downgrade(&strong); + let (ptr, alloc) = Weak::into_raw_with_allocator(weak); + let _recovered = unsafe { Weak::from_raw_in(ptr, alloc) }; + } +} + +#[cfg(kani)] +mod verify_3754 { + use super::kani_rc_harness_helpers::*; + use super::*; + use core::any::Any; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + #[kani::proof] + pub fn harness_weak_inner_u8_some_global() { + let value: u8 = kani::any(); + let strong: Rc = Rc::new_in(value, Global); + let weak: Weak = Rc::downgrade(&strong); + let _inner = Weak::::inner(&weak); + } + + #[kani::proof] + pub fn harness_weak_inner_u8_none_global() { + let weak: Weak = Weak::new_in(Global); + let _inner = Weak::::inner(&weak); + } + + #[kani::proof] + pub fn harness_weak_inner_i32_some_global() { + let value: i32 = kani::any(); + let strong: Rc = Rc::new_in(value, Global); + let weak: Weak = Rc::downgrade(&strong); + let _inner = Weak::::inner(&weak); + } + + #[kani::proof] + pub fn harness_weak_inner_i32_none_global() { + let weak: Weak = Weak::new_in(Global); + let _inner = Weak::::inner(&weak); + } + + #[kani::proof] + pub fn harness_weak_inner_u64_some_global() { + let value: u64 = kani::any(); + let strong: Rc = Rc::new_in(value, Global); + let weak: Weak = Rc::downgrade(&strong); + let _inner = Weak::::inner(&weak); + } + + #[kani::proof] + pub fn harness_weak_inner_u64_none_global() { + let weak: Weak = Weak::new_in(Global); + let _inner = Weak::::inner(&weak); + } + + #[kani::proof] + pub fn harness_weak_inner_unit_some_global() { + let strong: Rc<(), Global> = Rc::new_in((), Global); + let weak: Weak<(), Global> = Rc::downgrade(&strong); + let _inner = Weak::<(), Global>::inner(&weak); + } + + #[kani::proof] + pub fn harness_weak_inner_unit_none_global() { + let weak: Weak<(), Global> = Weak::new_in(Global); + let _inner = Weak::<(), Global>::inner(&weak); + } + + #[kani::proof] + pub fn harness_weak_inner_string_none_global() { + let weak: Weak = Weak::new_in(Global); + let _inner = Weak::::inner(&weak); + } + + #[kani::proof] + pub fn harness_weak_inner_drop_sentinel_some_global() { + let value = DropSentinel(kani::any()); + let strong: Rc = Rc::new_in(value, Global); + let weak: Weak = Rc::downgrade(&strong); + let _inner = Weak::::inner(&weak); + } + + #[kani::proof] + pub fn harness_weak_inner_drop_sentinel_none_global() { + let weak: Weak = Weak::new_in(Global); + let _inner = Weak::::inner(&weak); + } + + #[kani::proof] + pub fn harness_weak_inner_arr3_some_global() { + let value: [u8; 3] = kani::any(); + let strong: Rc<[u8; 3], Global> = Rc::new_in(value, Global); + let weak: Weak<[u8; 3], Global> = Rc::downgrade(&strong); + let _inner = Weak::<[u8; 3], Global>::inner(&weak); + } + + #[kani::proof] + pub fn harness_weak_inner_arr3_none_global() { + let weak: Weak<[u8; 3], Global> = Weak::new_in(Global); + let _inner = Weak::<[u8; 3], Global>::inner(&weak); + } + + #[kani::proof] + pub fn harness_weak_inner_bool_some_global() { + let value: bool = kani::any(); + let strong: Rc = Rc::new_in(value, Global); + let weak: Weak = Rc::downgrade(&strong); + let _inner = Weak::::inner(&weak); + } + + #[kani::proof] + pub fn harness_weak_inner_bool_none_global() { + let weak: Weak = Weak::new_in(Global); + let _inner = Weak::::inner(&weak); + } + + #[kani::proof] + pub fn harness_weak_inner_nested_rc_i32_some_global() { + let nested: Rc = Rc::new(kani::any::()); + let strong: Rc, Global> = Rc::new_in(nested, Global); + let weak: Weak, Global> = Rc::downgrade(&strong); + let _inner = Weak::, Global>::inner(&weak); + } + + #[kani::proof] + pub fn harness_weak_inner_nested_rc_i32_none_global() { + let weak: Weak, Global> = Weak::new_in(Global); + let _inner = Weak::, Global>::inner(&weak); + } + + #[kani::proof] + pub fn harness_weak_inner_tuple_i32_string_some_global() { + let value: (i32, String) = (kani::any(), String::new()); + let strong: Rc<(i32, String), Global> = Rc::new_in(value, Global); + let weak: Weak<(i32, String), Global> = Rc::downgrade(&strong); + let _inner = Weak::<(i32, String), Global>::inner(&weak); + } + + #[kani::proof] + pub fn harness_weak_inner_tuple_i32_string_none_global() { + let weak: Weak<(i32, String), Global> = Weak::new_in(Global); + let _inner = Weak::<(i32, String), Global>::inner(&weak); + } + + #[kani::proof] + pub fn harness_weak_inner_option_i32_some_global() { + let value: Option = kani::any(); + let strong: Rc, Global> = Rc::new_in(value, Global); + let weak: Weak, Global> = Rc::downgrade(&strong); + let _inner = Weak::, Global>::inner(&weak); + } + + #[kani::proof] + pub fn harness_weak_inner_option_i32_none_global() { + let weak: Weak, Global> = Weak::new_in(Global); + let _inner = Weak::, Global>::inner(&weak); + } + + #[kani::proof] + pub fn harness_weak_inner_str_some_global() { + let strong: Rc = Rc::from("seed"); + let weak: Weak = Rc::downgrade(&strong); + let _inner = Weak::::inner(&weak); + } + + #[kani::proof] + pub fn harness_weak_inner_str_after_drop_global() { + let strong: Rc = Rc::from("seed"); + let weak: Weak = Rc::downgrade(&strong); + drop(strong); + let _inner = Weak::::inner(&weak); + } + + #[kani::proof] + pub fn harness_weak_inner_dyn_any_i32_some_global() { + let value: i32 = kani::any(); + let strong_i32: Rc = Rc::new_in(value, Global); + let strong: Rc = strong_i32; + let weak: Weak = Rc::downgrade(&strong); + let _inner = Weak::::inner(&weak); + } + + #[kani::proof] + pub fn harness_weak_inner_dyn_any_i32_none_global() { + let weak_i32: Weak = Weak::new_in(Global); + let weak: Weak = weak_i32; + let _inner = Weak::::inner(&weak); + } + + #[kani::proof] + pub fn harness_weak_inner_unsized_slice_u8_some_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let strong = Rc::new_in(slice, Global); + let weak = Rc::downgrade(&strong); + let _inner = Weak::inner(&weak); + } + + #[kani::proof] + pub fn harness_weak_inner_unsized_slice_u16_some_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let strong = Rc::new_in(slice, Global); + let weak = Rc::downgrade(&strong); + let _inner = Weak::inner(&weak); + } + + #[kani::proof] + pub fn harness_weak_inner_unsized_slice_u32_some_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let strong = Rc::new_in(slice, Global); + let weak = Rc::downgrade(&strong); + let _inner = Weak::inner(&weak); + } +} + +#[cfg(kani)] +mod verify_3844 { + use crate::vec; + + use super::kani_rc_harness_helpers::*; + use super::*; + use core::any::Any; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + fn exercise_weak_drop_unique(rc: Rc) { + let weak: Weak = Rc::downgrade(&rc); + core::mem::drop(weak); + core::mem::drop(rc); + } + + fn exercise_weak_drop_shared(rc: Rc) { + let rc_clone: Rc = Rc::clone(&rc); + let weak: Weak = Rc::downgrade(&rc); + core::mem::drop(weak); + core::mem::drop(rc_clone); + core::mem::drop(rc); + } + + fn exercise_weak_drop_weak_present(rc: Rc) { + let weak: Weak = Rc::downgrade(&rc); + let weak_clone: Weak = Weak::clone(&weak); + core::mem::drop(rc); + core::mem::drop(weak); + core::mem::drop(weak_clone); + } + + #[kani::proof] + pub fn harness_drop_weak_i32_dangling_global() { + let weak: Weak = Weak::new_in(Global); + core::mem::drop(weak); + } + + #[kani::proof] + pub fn harness_drop_weak_u8_unique_global() { + let value: u8 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_weak_drop_unique(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_u8_shared_global() { + let value: u8 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_weak_drop_shared(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_u8_weak_present_global() { + let value: u8 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_weak_drop_weak_present(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_i32_unique_global() { + let value: i32 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_weak_drop_unique(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_i32_shared_global() { + let value: i32 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_weak_drop_shared(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_i32_weak_present_global() { + let value: i32 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_weak_drop_weak_present(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_u64_unique_global() { + let value: u64 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_weak_drop_unique(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_u64_shared_global() { + let value: u64 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_weak_drop_shared(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_u64_weak_present_global() { + let value: u64 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_weak_drop_weak_present(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_unit_unique_global() { + let rc: Rc<(), Global> = Rc::new_in((), Global); + exercise_weak_drop_unique(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_unit_shared_global() { + let rc: Rc<(), Global> = Rc::new_in((), Global); + exercise_weak_drop_shared(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_unit_weak_present_global() { + let rc: Rc<(), Global> = Rc::new_in((), Global); + exercise_weak_drop_weak_present(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_drop_sentinel_unique_global() { + let value = DropSentinel(kani::any()); + let rc: Rc = Rc::new_in(value, Global); + exercise_weak_drop_unique(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_drop_sentinel_shared_global() { + let value = DropSentinel(kani::any()); + let rc: Rc = Rc::new_in(value, Global); + exercise_weak_drop_shared(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_drop_sentinel_weak_present_global() { + let value = DropSentinel(kani::any()); + let rc: Rc = Rc::new_in(value, Global); + exercise_weak_drop_weak_present(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_arr3_unique_global() { + let value: [u8; 3] = kani::any(); + let rc: Rc<[u8; 3], Global> = Rc::new_in(value, Global); + exercise_weak_drop_unique(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_arr3_shared_global() { + let value: [u8; 3] = kani::any(); + let rc: Rc<[u8; 3], Global> = Rc::new_in(value, Global); + exercise_weak_drop_shared(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_arr3_weak_present_global() { + let value: [u8; 3] = kani::any(); + let rc: Rc<[u8; 3], Global> = Rc::new_in(value, Global); + exercise_weak_drop_weak_present(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_unsized_slice_u8_unique_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + exercise_weak_drop_unique(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_unsized_slice_u8_shared_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + exercise_weak_drop_shared(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_unsized_slice_u8_weak_present_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + exercise_weak_drop_weak_present(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_unsized_slice_u16_unique_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + exercise_weak_drop_unique(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_unsized_slice_u16_shared_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + exercise_weak_drop_shared(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_unsized_slice_u16_weak_present_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + exercise_weak_drop_weak_present(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_unsized_slice_u32_unique_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + exercise_weak_drop_unique(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_unsized_slice_u32_shared_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + exercise_weak_drop_shared(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_unsized_slice_u32_weak_present_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + exercise_weak_drop_weak_present(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_dyn_any_i32_unique_global() { + let value: i32 = kani::any(); + let rc_i32: Rc = Rc::new_in(value, Global); + let rc: Rc = rc_i32; + exercise_weak_drop_unique(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_dyn_any_i32_shared_global() { + let value: i32 = kani::any(); + let rc_i32: Rc = Rc::new_in(value, Global); + let rc: Rc = rc_i32; + exercise_weak_drop_shared(rc); + } + + #[kani::proof] + pub fn harness_drop_weak_dyn_any_i32_weak_present_global() { + let value: i32 = kani::any(); + let rc_i32: Rc = Rc::new_in(value, Global); + let rc: Rc = rc_i32; + exercise_weak_drop_weak_present(rc); + } +} + +#[cfg(kani)] +mod verify_3939 { + use super::kani_rc_harness_helpers::*; + use super::*; + use core::any::Any; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + fn exercise_inc_strong_unique(rc: Rc) { + let inner = rc.inner(); + inner.inc_strong(); + inner.dec_strong(); + drop(rc); + } + + fn exercise_inc_strong_shared(rc: Rc) { + let rc_clone: Rc = Rc::clone(&rc); + let inner = rc.inner(); + inner.inc_strong(); + inner.dec_strong(); + drop(rc_clone); + drop(rc); + } + + fn exercise_inc_strong_weak_present(rc: Rc) { + let weak: Weak = Rc::downgrade(&rc); + let inner = rc.inner(); + inner.inc_strong(); + inner.dec_strong(); + drop(rc); + drop(weak); + } + + #[kani::proof] + pub fn harness_inc_strong_u8_unique() { + let value: u8 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_inc_strong_unique(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_u8_shared() { + let value: u8 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_inc_strong_shared(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_u8_weak_present() { + let value: u8 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_inc_strong_weak_present(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_i32_unique() { + let value: i32 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_inc_strong_unique(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_i32_shared() { + let value: i32 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_inc_strong_shared(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_i32_weak_present() { + let value: i32 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_inc_strong_weak_present(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_u64_unique() { + let value: u64 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_inc_strong_unique(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_u64_shared() { + let value: u64 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_inc_strong_shared(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_u64_weak_present() { + let value: u64 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_inc_strong_weak_present(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_unit_unique() { + let rc: Rc<(), Global> = Rc::new_in((), Global); + exercise_inc_strong_unique(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_unit_shared() { + let rc: Rc<(), Global> = Rc::new_in((), Global); + exercise_inc_strong_shared(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_unit_weak_present() { + let rc: Rc<(), Global> = Rc::new_in((), Global); + exercise_inc_strong_weak_present(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_drop_sentinel_unique() { + let value = DropSentinel(kani::any()); + let rc: Rc = Rc::new_in(value, Global); + exercise_inc_strong_unique(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_drop_sentinel_shared() { + let value = DropSentinel(kani::any()); + let rc: Rc = Rc::new_in(value, Global); + exercise_inc_strong_shared(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_drop_sentinel_weak_present() { + let value = DropSentinel(kani::any()); + let rc: Rc = Rc::new_in(value, Global); + exercise_inc_strong_weak_present(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_arr3_unique() { + let value: [u8; 3] = kani::any(); + let rc: Rc<[u8; 3], Global> = Rc::new_in(value, Global); + exercise_inc_strong_unique(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_arr3_shared() { + let value: [u8; 3] = kani::any(); + let rc: Rc<[u8; 3], Global> = Rc::new_in(value, Global); + exercise_inc_strong_shared(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_arr3_weak_present() { + let value: [u8; 3] = kani::any(); + let rc: Rc<[u8; 3], Global> = Rc::new_in(value, Global); + exercise_inc_strong_weak_present(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_unsized_slice_u8_unique() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + exercise_inc_strong_unique(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_unsized_slice_u8_shared() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + exercise_inc_strong_shared(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_unsized_slice_u8_weak_present() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + exercise_inc_strong_weak_present(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_unsized_slice_u16_unique() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + exercise_inc_strong_unique(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_unsized_slice_u16_shared() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + exercise_inc_strong_shared(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_unsized_slice_u16_weak_present() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + exercise_inc_strong_weak_present(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_unsized_slice_u32_unique() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + exercise_inc_strong_unique(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_unsized_slice_u32_shared() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + exercise_inc_strong_shared(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_unsized_slice_u32_weak_present() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + exercise_inc_strong_weak_present(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_str_unique() { + let rc: Rc = Rc::from("kani"); + exercise_inc_strong_unique(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_str_shared() { + let rc: Rc = Rc::from("kani"); + exercise_inc_strong_shared(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_str_weak_present() { + let rc: Rc = Rc::from("kani"); + exercise_inc_strong_weak_present(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_dyn_any_i32_unique() { + let value: i32 = kani::any(); + let rc_i32: Rc = Rc::new_in(value, Global); + let rc: Rc = rc_i32; + exercise_inc_strong_unique(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_dyn_any_i32_shared() { + let value: i32 = kani::any(); + let rc_i32: Rc = Rc::new_in(value, Global); + let rc: Rc = rc_i32; + exercise_inc_strong_shared(rc); + } + + #[kani::proof] + pub fn harness_inc_strong_dyn_any_i32_weak_present() { + let value: i32 = kani::any(); + let rc_i32: Rc = Rc::new_in(value, Global); + let rc: Rc = rc_i32; + exercise_inc_strong_weak_present(rc); + } +} + +#[cfg(kani)] +mod verify_3972 { + use super::kani_rc_harness_helpers::*; + use super::*; + use core::any::Any; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + fn exercise_inc_weak_unique(rc: Rc) { + let inner = rc.inner(); + inner.inc_weak(); + inner.dec_weak(); + drop(rc); + } + + fn exercise_inc_weak_shared(rc: Rc) { + let rc_clone: Rc = Rc::clone(&rc); + let inner = rc.inner(); + inner.inc_weak(); + inner.dec_weak(); + drop(rc_clone); + drop(rc); + } + + fn exercise_inc_weak_weak_present(rc: Rc) { + let weak: Weak = Rc::downgrade(&rc); + let inner = rc.inner(); + inner.inc_weak(); + inner.dec_weak(); + drop(rc); + drop(weak); + } + + #[kani::proof] + pub fn harness_inc_weak_u8_unique() { + let value: u8 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_inc_weak_unique(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_u8_shared() { + let value: u8 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_inc_weak_shared(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_u8_weak_present() { + let value: u8 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_inc_weak_weak_present(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_i32_unique() { + let value: i32 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_inc_weak_unique(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_i32_shared() { + let value: i32 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_inc_weak_shared(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_i32_weak_present() { + let value: i32 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_inc_weak_weak_present(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_u64_unique() { + let value: u64 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_inc_weak_unique(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_u64_shared() { + let value: u64 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_inc_weak_shared(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_u64_weak_present() { + let value: u64 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_inc_weak_weak_present(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_unit_unique() { + let rc: Rc<(), Global> = Rc::new_in((), Global); + exercise_inc_weak_unique(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_unit_shared() { + let rc: Rc<(), Global> = Rc::new_in((), Global); + exercise_inc_weak_shared(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_unit_weak_present() { + let rc: Rc<(), Global> = Rc::new_in((), Global); + exercise_inc_weak_weak_present(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_drop_sentinel_unique() { + let value = DropSentinel(kani::any()); + let rc: Rc = Rc::new_in(value, Global); + exercise_inc_weak_unique(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_drop_sentinel_shared() { + let value = DropSentinel(kani::any()); + let rc: Rc = Rc::new_in(value, Global); + exercise_inc_weak_shared(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_drop_sentinel_weak_present() { + let value = DropSentinel(kani::any()); + let rc: Rc = Rc::new_in(value, Global); + exercise_inc_weak_weak_present(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_arr3_unique() { + let value: [u8; 3] = kani::any(); + let rc: Rc<[u8; 3], Global> = Rc::new_in(value, Global); + exercise_inc_weak_unique(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_arr3_shared() { + let value: [u8; 3] = kani::any(); + let rc: Rc<[u8; 3], Global> = Rc::new_in(value, Global); + exercise_inc_weak_shared(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_arr3_weak_present() { + let value: [u8; 3] = kani::any(); + let rc: Rc<[u8; 3], Global> = Rc::new_in(value, Global); + exercise_inc_weak_weak_present(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_slice_unsized_u8_unique() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + exercise_inc_weak_unique(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_slice_unsized_u8_shared() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + exercise_inc_weak_shared(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_slice_unsized_u8_weak_present() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + exercise_inc_weak_weak_present(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_slice_unsized_u16_unique() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + exercise_inc_weak_unique(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_slice_unsized_u16_shared() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + exercise_inc_weak_shared(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_slice_unsized_u16_weak_present() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + exercise_inc_weak_weak_present(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_slice_unsized_u32_unique() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + exercise_inc_weak_unique(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_slice_unsized_u32_shared() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + exercise_inc_weak_shared(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_slice_unsized_u32_weak_present() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + let rc = Rc::new_in(slice, Global); + exercise_inc_weak_weak_present(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_dyn_any_i32_unique() { + let value: i32 = kani::any(); + let rc_i32: Rc = Rc::new_in(value, Global); + let rc: Rc = rc_i32; + exercise_inc_weak_unique(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_dyn_any_i32_shared() { + let value: i32 = kani::any(); + let rc_i32: Rc = Rc::new_in(value, Global); + let rc: Rc = rc_i32; + exercise_inc_weak_shared(rc); + } + + #[kani::proof] + pub fn harness_inc_weak_dyn_any_i32_weak_present() { + let value: i32 = kani::any(); + let rc_i32: Rc = Rc::new_in(value, Global); + let rc: Rc = rc_i32; + exercise_inc_weak_weak_present(rc); + } +} + +#[cfg(kani)] +mod verify_4413 { + use super::kani_rc_harness_helpers::*; + use super::*; + use core::any::Any; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + #[kani::proof] + pub fn harness_into_rc_u8_global() { + let unique: UniqueRc = UniqueRc::new_in(kani::any(), Global); + let rc: Rc = UniqueRc::into_rc(unique); + drop(rc); + } + + #[kani::proof] + pub fn harness_into_rc_i32_global() { + let unique: UniqueRc = UniqueRc::new_in(kani::any(), Global); + let rc: Rc = UniqueRc::into_rc(unique); + drop(rc); + } + + #[kani::proof] + pub fn harness_into_rc_u64_global() { + let unique: UniqueRc = UniqueRc::new_in(kani::any(), Global); + let rc: Rc = UniqueRc::into_rc(unique); + drop(rc); + } + + #[kani::proof] + pub fn harness_into_rc_bool_global() { + let unique: UniqueRc = UniqueRc::new_in(kani::any(), Global); + let rc: Rc = UniqueRc::into_rc(unique); + drop(rc); + } + + #[kani::proof] + pub fn harness_into_rc_unit_global() { + let unique: UniqueRc<(), Global> = UniqueRc::new_in((), Global); + let rc: Rc<(), Global> = UniqueRc::into_rc(unique); + drop(rc); + } + + #[kani::proof] + pub fn harness_into_rc_drop_sentinel_global() { + let unique: UniqueRc = + UniqueRc::new_in(DropSentinel(kani::any()), Global); + let rc: Rc = UniqueRc::into_rc(unique); + drop(rc); + } + + #[kani::proof] + pub fn harness_into_rc_arr3_global() { + let unique: UniqueRc<[u8; 3], Global> = UniqueRc::new_in(kani::any(), Global); + let rc: Rc<[u8; 3], Global> = UniqueRc::into_rc(unique); + drop(rc); + } + + #[kani::proof] + pub fn harness_into_rc_arr0_global() { + let unique: UniqueRc<[u8; 0], Global> = UniqueRc::new_in([], Global); + let rc: Rc<[u8; 0], Global> = UniqueRc::into_rc(unique); + drop(rc); + } + + #[kani::proof] + pub fn harness_into_rc_tuple_i32_string_global() { + let value = (kani::any::(), String::new()); + let unique: UniqueRc<(i32, String), Global> = UniqueRc::new_in(value, Global); + let rc: Rc<(i32, String), Global> = UniqueRc::into_rc(unique); + drop(rc); + } + + #[kani::proof] + pub fn harness_into_rc_option_i32_global() { + let unique: UniqueRc, Global> = UniqueRc::new_in(kani::any(), Global); + let rc: Rc, Global> = UniqueRc::into_rc(unique); + drop(rc); + } + + #[kani::proof] + pub fn harness_into_rc_unsized_slice_u8_global() { + let vec = verifier_nondet_vec::(); + let unique_slice = UniqueRc::new_in(nondet_rc_slice(&vec), Global); + let rc = UniqueRc::into_rc(unique_slice); + drop(rc); + } + + #[kani::proof] + pub fn harness_into_rc_unsized_slice_u16_global() { + let vec = verifier_nondet_vec::(); + let unique_slice = UniqueRc::new_in(nondet_rc_slice(&vec), Global); + let rc = UniqueRc::into_rc(unique_slice); + drop(rc); + } + + #[kani::proof] + pub fn harness_into_rc_unsized_slice_u32_global() { + let vec = verifier_nondet_vec::(); + let unique_slice = UniqueRc::new_in(nondet_rc_slice(&vec), Global); + let rc = UniqueRc::into_rc(unique_slice); + drop(rc); + } + + #[kani::proof] + pub fn harness_into_rc_dyn_any_i32_global() { + let unique_i32: UniqueRc = UniqueRc::new_in(kani::any(), Global); + let unique_dyn: UniqueRc = unique_i32; + let rc: Rc = UniqueRc::into_rc(unique_dyn); + drop(rc); + } + + #[kani::proof] + pub fn harness_into_rc_dyn_debug_i32_global() { + let unique_i32: UniqueRc = UniqueRc::new_in(kani::any(), Global); + let rc: Rc = UniqueRc::into_rc(unique_i32); + drop(rc); + } +} + +#[cfg(kani)] +mod verify_4436 { + use super::kani_rc_harness_helpers::*; + use super::*; + use core::any::Any; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + fn exercise_downgrade_unique(unique: &UniqueRc) { + let weak = UniqueRc::downgrade(unique); + drop(weak); + } + + fn exercise_downgrade_weak_present(unique: &UniqueRc) { + let weak1 = UniqueRc::downgrade(unique); + let weak2 = UniqueRc::downgrade(unique); + drop((weak1, weak2)); + } + + #[kani::proof] + pub fn harness_downgrade_u8_unique_global() { + let unique: UniqueRc = UniqueRc::new_in(kani::any(), Global); + exercise_downgrade_unique(&unique); + } + + #[kani::proof] + pub fn harness_downgrade_u8_weak_present_global() { + let unique: UniqueRc = UniqueRc::new_in(kani::any(), Global); + exercise_downgrade_weak_present(&unique); + } + + #[kani::proof] + pub fn harness_downgrade_i32_unique_global() { + let unique: UniqueRc = UniqueRc::new_in(kani::any(), Global); + exercise_downgrade_unique(&unique); + } + + #[kani::proof] + pub fn harness_downgrade_i32_weak_present_global() { + let unique: UniqueRc = UniqueRc::new_in(kani::any(), Global); + exercise_downgrade_weak_present(&unique); + } + + #[kani::proof] + pub fn harness_downgrade_u64_unique_global() { + let unique: UniqueRc = UniqueRc::new_in(kani::any(), Global); + exercise_downgrade_unique(&unique); + } + + #[kani::proof] + pub fn harness_downgrade_u64_weak_present_global() { + let unique: UniqueRc = UniqueRc::new_in(kani::any(), Global); + exercise_downgrade_weak_present(&unique); + } + + #[kani::proof] + pub fn harness_downgrade_unit_unique_global() { + let unique: UniqueRc<(), Global> = UniqueRc::new_in((), Global); + exercise_downgrade_unique(&unique); + } + + #[kani::proof] + pub fn harness_downgrade_unit_weak_present_global() { + let unique: UniqueRc<(), Global> = UniqueRc::new_in((), Global); + exercise_downgrade_weak_present(&unique); + } + + #[kani::proof] + pub fn harness_downgrade_drop_sentinel_unique_global() { + let unique: UniqueRc = + UniqueRc::new_in(DropSentinel(kani::any()), Global); + exercise_downgrade_unique(&unique); + } + + #[kani::proof] + pub fn harness_downgrade_drop_sentinel_weak_present_global() { + let unique: UniqueRc = + UniqueRc::new_in(DropSentinel(kani::any()), Global); + exercise_downgrade_weak_present(&unique); + } + + #[kani::proof] + pub fn harness_downgrade_arr3_unique_global() { + let unique: UniqueRc<[u8; 3], Global> = UniqueRc::new_in(kani::any(), Global); + exercise_downgrade_unique(&unique); + } + + #[kani::proof] + pub fn harness_downgrade_arr3_weak_present_global() { + let unique: UniqueRc<[u8; 3], Global> = UniqueRc::new_in(kani::any(), Global); + exercise_downgrade_weak_present(&unique); + } + + #[kani::proof] + pub fn harness_downgrade_unsized_slice_u8_unique_global() { + let vec = verifier_nondet_vec::(); + let unique_slice = UniqueRc::new_in(nondet_rc_slice(&vec), Global); + exercise_downgrade_unique(&unique_slice); + } + + #[kani::proof] + pub fn harness_downgrade_unsized_slice_u8_weak_present_global() { + let vec = verifier_nondet_vec::(); + let unique_slice = UniqueRc::new_in(nondet_rc_slice(&vec), Global); + exercise_downgrade_weak_present(&unique_slice); + } + + #[kani::proof] + pub fn harness_downgrade_unsized_slice_u16_unique_global() { + let vec = verifier_nondet_vec::(); + let unique_slice = UniqueRc::new_in(nondet_rc_slice(&vec), Global); + exercise_downgrade_unique(&unique_slice); + } + + #[kani::proof] + pub fn harness_downgrade_unsized_slice_u16_weak_present_global() { + let vec = verifier_nondet_vec::(); + let unique_slice = UniqueRc::new_in(nondet_rc_slice(&vec), Global); + exercise_downgrade_weak_present(&unique_slice); + } + + #[kani::proof] + pub fn harness_downgrade_unsized_slice_u32_unique_global() { + let vec = verifier_nondet_vec::(); + let unique_slice = UniqueRc::new_in(nondet_rc_slice(&vec), Global); + exercise_downgrade_unique(&unique_slice); + } + + #[kani::proof] + pub fn harness_downgrade_unsized_slice_u32_weak_present_global() { + let vec = verifier_nondet_vec::(); + let unique_slice = UniqueRc::new_in(nondet_rc_slice(&vec), Global); + exercise_downgrade_weak_present(&unique_slice); + } + + #[kani::proof] + pub fn harness_downgrade_dyn_any_i32_unique_global() { + let unique_i32: UniqueRc = UniqueRc::new_in(kani::any(), Global); + let unique_dyn: UniqueRc = unique_i32; + exercise_downgrade_unique(&unique_dyn); + } + + #[kani::proof] + pub fn harness_downgrade_dyn_any_i32_weak_present_global() { + let unique_i32: UniqueRc = UniqueRc::new_in(kani::any(), Global); + let unique_dyn: UniqueRc = unique_i32; + exercise_downgrade_weak_present(&unique_dyn); + } +} + +#[cfg(kani)] +mod verify_4461 { + use super::kani_rc_harness_helpers::*; + use super::*; + use core::{any::Any, ops::DerefMut}; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + fn exercise_deref_mut(unique: &mut UniqueRc) { + let _: &mut T = DerefMut::deref_mut(unique); + } + + #[kani::proof] + pub fn harness_deref_mut_u8_global() { + let mut unique: UniqueRc = UniqueRc::new_in(kani::any(), Global); + exercise_deref_mut(&mut unique); + } + + #[kani::proof] + pub fn harness_deref_mut_i32_global() { + let mut unique: UniqueRc = UniqueRc::new_in(kani::any(), Global); + exercise_deref_mut(&mut unique); + } + + #[kani::proof] + pub fn harness_deref_mut_u64_global() { + let mut unique: UniqueRc = UniqueRc::new_in(kani::any(), Global); + exercise_deref_mut(&mut unique); + } + + #[kani::proof] + pub fn harness_deref_mut_bool_global() { + let mut unique: UniqueRc = UniqueRc::new_in(kani::any(), Global); + exercise_deref_mut(&mut unique); + } + + #[kani::proof] + pub fn harness_deref_mut_unit_global() { + let mut unique: UniqueRc<(), Global> = UniqueRc::new_in((), Global); + exercise_deref_mut(&mut unique); + } + + #[kani::proof] + pub fn harness_deref_mut_drop_sentinel_global() { + let mut unique: UniqueRc = + UniqueRc::new_in(DropSentinel(kani::any()), Global); + exercise_deref_mut(&mut unique); + } + + #[kani::proof] + pub fn harness_deref_mut_arr3_global() { + let mut unique: UniqueRc<[u8; 3], Global> = UniqueRc::new_in(kani::any(), Global); + exercise_deref_mut(&mut unique); + } + + #[kani::proof] + pub fn harness_deref_mut_arr0_global() { + let mut unique: UniqueRc<[u8; 0], Global> = UniqueRc::new_in([], Global); + exercise_deref_mut(&mut unique); + } + + #[kani::proof] + pub fn harness_deref_mut_tuple_i32_string_global() { + let mut unique: UniqueRc<(i32, String), Global> = + UniqueRc::new_in((kani::any::(), String::new()), Global); + exercise_deref_mut(&mut unique); + } + + #[kani::proof] + pub fn harness_deref_mut_option_i32_global() { + let mut unique: UniqueRc, Global> = UniqueRc::new_in(kani::any(), Global); + exercise_deref_mut(&mut unique); + } + + #[kani::proof] + pub fn harness_deref_mut_unsized_slice_u8_global() { + let vec = verifier_nondet_vec::(); + let mut unique_slice = UniqueRc::new_in(nondet_rc_slice(&vec), Global); + exercise_deref_mut(&mut unique_slice); + } + + #[kani::proof] + pub fn harness_deref_mut_unsized_slice_u16_global() { + let vec = verifier_nondet_vec::(); + let mut unique_slice = UniqueRc::new_in(nondet_rc_slice(&vec), Global); + exercise_deref_mut(&mut unique_slice); + } + + #[kani::proof] + pub fn harness_deref_mut_unsized_slice_u32_global() { + let vec = verifier_nondet_vec::(); + let mut unique_slice = UniqueRc::new_in(nondet_rc_slice(&vec), Global); + exercise_deref_mut(&mut unique_slice); + } + + #[kani::proof] + pub fn harness_deref_mut_dyn_any_i32_global() { + let unique_i32: UniqueRc = UniqueRc::new_in(kani::any(), Global); + let mut unique_dyn: UniqueRc = unique_i32; + exercise_deref_mut(&mut unique_dyn); + } +} + +#[cfg(kani)] +mod verify_4453 { + use super::kani_rc_harness_helpers::*; + use super::*; + use core::{any::Any, ops::Deref}; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + fn exercise_deref(unique: &UniqueRc) { + let _: &T = Deref::deref(unique); + } + + #[kani::proof] + pub fn harness_deref_u8_global() { + let unique: UniqueRc = UniqueRc::new_in(kani::any(), Global); + exercise_deref(&unique); + } + + #[kani::proof] + pub fn harness_deref_i32_global() { + let unique: UniqueRc = UniqueRc::new_in(kani::any(), Global); + exercise_deref(&unique); + } + + #[kani::proof] + pub fn harness_deref_u64_global() { + let unique: UniqueRc = UniqueRc::new_in(kani::any(), Global); + exercise_deref(&unique); + } + + #[kani::proof] + pub fn harness_deref_bool_global() { + let unique: UniqueRc = UniqueRc::new_in(kani::any(), Global); + exercise_deref(&unique); + } + + #[kani::proof] + pub fn harness_deref_unit_global() { + let unique: UniqueRc<(), Global> = UniqueRc::new_in((), Global); + exercise_deref(&unique); + } + + #[kani::proof] + pub fn harness_deref_drop_sentinel_global() { + let unique: UniqueRc = + UniqueRc::new_in(DropSentinel(kani::any()), Global); + exercise_deref(&unique); + } + + #[kani::proof] + pub fn harness_deref_arr3_global() { + let unique: UniqueRc<[u8; 3], Global> = UniqueRc::new_in(kani::any(), Global); + exercise_deref(&unique); + } + + #[kani::proof] + pub fn harness_deref_arr0_global() { + let unique: UniqueRc<[u8; 0], Global> = UniqueRc::new_in([], Global); + exercise_deref(&unique); + } + + #[kani::proof] + pub fn harness_deref_tuple_i32_string_global() { + let unique: UniqueRc<(i32, String), Global> = + UniqueRc::new_in((kani::any::(), String::new()), Global); + exercise_deref(&unique); + } + + #[kani::proof] + pub fn harness_deref_option_i32_global() { + let unique: UniqueRc, Global> = UniqueRc::new_in(kani::any(), Global); + exercise_deref(&unique); + } + + #[kani::proof] + pub fn harness_deref_unsized_slice_u8_global() { + let vec = verifier_nondet_vec::(); + let unique_slice = UniqueRc::new_in(nondet_rc_slice(&vec), Global); + exercise_deref(&unique_slice); + } + + #[kani::proof] + pub fn harness_deref_unsized_slice_u16_global() { + let vec = verifier_nondet_vec::(); + let unique_slice = UniqueRc::new_in(nondet_rc_slice(&vec), Global); + exercise_deref(&unique_slice); + } + + #[kani::proof] + pub fn harness_deref_unsized_slice_u32_global() { + let vec = verifier_nondet_vec::(); + let unique_slice = UniqueRc::new_in(nondet_rc_slice(&vec), Global); + exercise_deref(&unique_slice); + } +} + +#[cfg(kani)] +mod verify_4471 { + use super::kani_rc_harness_helpers::*; + use super::*; + use core::any::Any; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + fn exercise_drop_unique(unique: UniqueRc) { + core::mem::drop(unique); + } + + fn exercise_drop_weak_present(unique: UniqueRc) { + let weak: Weak = UniqueRc::downgrade(&unique); + core::mem::drop(unique); + core::mem::drop(weak); + } + + #[kani::proof] + pub fn harness_drop_unique_rc_u8_unique_global() { + let unique: UniqueRc = UniqueRc::new_in(kani::any(), Global); + exercise_drop_unique(unique); + } + + #[kani::proof] + pub fn harness_drop_unique_rc_u8_weak_present_global() { + let unique: UniqueRc = UniqueRc::new_in(kani::any(), Global); + exercise_drop_weak_present(unique); + } + + #[kani::proof] + pub fn harness_drop_unique_rc_i32_unique_global() { + let unique: UniqueRc = UniqueRc::new_in(kani::any(), Global); + exercise_drop_unique(unique); + } + + #[kani::proof] + pub fn harness_drop_unique_rc_i32_weak_present_global() { + let unique: UniqueRc = UniqueRc::new_in(kani::any(), Global); + exercise_drop_weak_present(unique); + } + + #[kani::proof] + pub fn harness_drop_unique_rc_u64_unique_global() { + let unique: UniqueRc = UniqueRc::new_in(kani::any(), Global); + exercise_drop_unique(unique); + } + + #[kani::proof] + pub fn harness_drop_unique_rc_u64_weak_present_global() { + let unique: UniqueRc = UniqueRc::new_in(kani::any(), Global); + exercise_drop_weak_present(unique); + } + + #[kani::proof] + pub fn harness_drop_unique_rc_unit_unique_global() { + let unique: UniqueRc<(), Global> = UniqueRc::new_in((), Global); + exercise_drop_unique(unique); + } + + #[kani::proof] + pub fn harness_drop_unique_rc_unit_weak_present_global() { + let unique: UniqueRc<(), Global> = UniqueRc::new_in((), Global); + exercise_drop_weak_present(unique); + } + + #[kani::proof] + pub fn harness_drop_unique_rc_drop_sentinel_unique_global() { + let unique: UniqueRc = + UniqueRc::new_in(DropSentinel(kani::any()), Global); + exercise_drop_unique(unique); + } + + #[kani::proof] + pub fn harness_drop_unique_rc_drop_sentinel_weak_present_global() { + let unique: UniqueRc = + UniqueRc::new_in(DropSentinel(kani::any()), Global); + exercise_drop_weak_present(unique); + } + + #[kani::proof] + pub fn harness_drop_unique_rc_arr3_unique_global() { + let unique: UniqueRc<[u8; 3], Global> = UniqueRc::new_in(kani::any(), Global); + exercise_drop_unique(unique); + } + + #[kani::proof] + pub fn harness_drop_unique_rc_arr3_weak_present_global() { + let unique: UniqueRc<[u8; 3], Global> = UniqueRc::new_in(kani::any(), Global); + exercise_drop_weak_present(unique); + } + + #[kani::proof] + pub fn harness_drop_unique_rc_unsized_slice_u8_unique_global() { + let vec = verifier_nondet_vec::(); + let unique_slice = UniqueRc::new_in(nondet_rc_slice(&vec), Global); + exercise_drop_unique(unique_slice); + } + + #[kani::proof] + pub fn harness_drop_unique_rc_unsized_slice_u8_weak_present_global() { + let vec = verifier_nondet_vec::(); + let unique_slice = UniqueRc::new_in(nondet_rc_slice(&vec), Global); + exercise_drop_weak_present(unique_slice); + } + + #[kani::proof] + pub fn harness_drop_unique_rc_unsized_slice_u16_unique_global() { + let vec = verifier_nondet_vec::(); + let unique_slice = UniqueRc::new_in(nondet_rc_slice(&vec), Global); + exercise_drop_unique(unique_slice); + } + + #[kani::proof] + pub fn harness_drop_unique_rc_unsized_slice_u16_weak_present_global() { + let vec = verifier_nondet_vec::(); + let unique_slice = UniqueRc::new_in(nondet_rc_slice(&vec), Global); + exercise_drop_weak_present(unique_slice); + } + + #[kani::proof] + pub fn harness_drop_unique_rc_unsized_slice_u32_unique_global() { + let vec = verifier_nondet_vec::(); + let unique_slice = UniqueRc::new_in(nondet_rc_slice(&vec), Global); + exercise_drop_unique(unique_slice); + } + + #[kani::proof] + pub fn harness_drop_unique_rc_unsized_slice_u32_weak_present_global() { + let vec = verifier_nondet_vec::(); + let unique_slice = UniqueRc::new_in(nondet_rc_slice(&vec), Global); + exercise_drop_weak_present(unique_slice); + } + + #[kani::proof] + pub fn harness_drop_unique_rc_dyn_any_i32_unique_global() { + let unique_i32: UniqueRc = UniqueRc::new_in(kani::any(), Global); + let unique_dyn: UniqueRc = unique_i32; + exercise_drop_unique(unique_dyn); + } + + #[kani::proof] + pub fn harness_drop_unique_rc_dyn_any_i32_weak_present_global() { + let unique_i32: UniqueRc = UniqueRc::new_in(kani::any(), Global); + let unique_dyn: UniqueRc = unique_i32; + exercise_drop_weak_present(unique_dyn); + } + + #[kani::proof] + pub fn harness_drop_unique_rc_bool_unique_global() { + let unique: UniqueRc = UniqueRc::new_in(kani::any(), Global); + exercise_drop_unique(unique); + } + + #[kani::proof] + pub fn harness_drop_unique_rc_bool_weak_present_global() { + let unique: UniqueRc = UniqueRc::new_in(kani::any(), Global); + exercise_drop_weak_present(unique); + } + + #[kani::proof] + pub fn harness_drop_unique_rc_tuple_i32_string_unique_global() { + let unique: UniqueRc<(i32, String), Global> = + UniqueRc::new_in((kani::any::(), String::new()), Global); + exercise_drop_unique(unique); + } + + #[kani::proof] + pub fn harness_drop_unique_rc_tuple_i32_string_weak_present_global() { + let unique: UniqueRc<(i32, String), Global> = + UniqueRc::new_in((kani::any::(), String::new()), Global); + exercise_drop_weak_present(unique); + } + + #[kani::proof] + pub fn harness_drop_unique_rc_option_i32_unique_global() { + let unique: UniqueRc, Global> = UniqueRc::new_in(kani::any(), Global); + exercise_drop_unique(unique); + } + + #[kani::proof] + pub fn harness_drop_unique_rc_option_i32_weak_present_global() { + let unique: UniqueRc, Global> = UniqueRc::new_in(kani::any(), Global); + exercise_drop_weak_present(unique); + } +} + +#[cfg(kani)] +mod verify_4503 { + use crate::vec; + + use super::kani_rc_harness_helpers::*; + use super::*; + use core::any::Any; + use core::cell::Cell; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + fn exercise_new(for_value: &T) { + let uninit: UniqueRcUninit = UniqueRcUninit::new(for_value, Global); + core::mem::drop(uninit); + } + + #[kani::proof] + pub fn harness_new_u8_global() { + let value: u8 = kani::any(); + exercise_new(&value); + } + + #[kani::proof] + pub fn harness_new_i32_global() { + let value: i32 = kani::any(); + exercise_new(&value); + } + + #[kani::proof] + pub fn harness_new_u64_global() { + let value: u64 = kani::any(); + exercise_new(&value); + } + + #[kani::proof] + pub fn harness_new_unit_global() { + let value = (); + exercise_new(&value); + } + + #[kani::proof] + pub fn harness_new_drop_sentinel_global() { + let value = DropSentinel(kani::any()); + exercise_new(&value); + } + + #[kani::proof] + pub fn harness_new_array_u8_3_global() { + let value: [u8; 3] = kani::any(); + exercise_new(&value); + } + + #[kani::proof] + pub fn harness_new_unsized_slice_u8_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + exercise_new(slice); + } + + #[kani::proof] + pub fn harness_new_unsized_slice_u16_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + exercise_new(slice); + } + + #[kani::proof] + pub fn harness_new_unsized_slice_u32_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + exercise_new(slice); + } + + #[kani::proof] + pub fn harness_new_dyn_any_i32_global() { + let value: i32 = kani::any(); + let trait_obj: &dyn Any = &value; + exercise_new(trait_obj); + } + + #[kani::proof] + pub fn harness_new_bool_global() { + let value: bool = kani::any(); + exercise_new(&value); + } + + #[kani::proof] + pub fn harness_new_nested_rc_i32_global() { + let value: Rc = Rc::new_in(kani::any::(), Global); + exercise_new(&value); + } + + #[kani::proof] + pub fn harness_new_tuple_i32_string_global() { + let value: (i32, String) = (kani::any::(), String::new()); + exercise_new(&value); + } + + #[kani::proof] + pub fn harness_new_option_i32_global() { + let value: Option = kani::any(); + exercise_new(&value); + } + + #[kani::proof] + pub fn harness_new_cell_i32_global() { + let value = Cell::new(kani::any::()); + exercise_new(&value); + } +} + +#[cfg(kani)] +mod verify_4520 { + use super::kani_rc_harness_helpers::*; + use super::*; + use core::any::Any; + use core::cell::Cell; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + fn exercise_data_ptr(for_value: &T) { + let mut uninit: UniqueRcUninit = UniqueRcUninit::new(for_value, Global); + let _ptr: *mut T = uninit.data_ptr(); + core::mem::drop(uninit); + } + + #[kani::proof] + pub fn harness_data_ptr_u8_global() { + let value: u8 = kani::any(); + exercise_data_ptr(&value); + } + + #[kani::proof] + pub fn harness_data_ptr_i32_global() { + let value: i32 = kani::any(); + exercise_data_ptr(&value); + } + + #[kani::proof] + pub fn harness_data_ptr_u64_global() { + let value: u64 = kani::any(); + exercise_data_ptr(&value); + } + + #[kani::proof] + pub fn harness_data_ptr_unit_global() { + let value = (); + exercise_data_ptr(&value); + } + + #[kani::proof] + pub fn harness_data_ptr_drop_sentinel_global() { + let value = DropSentinel(kani::any()); + exercise_data_ptr(&value); + } + + #[kani::proof] + pub fn harness_data_ptr_array_u8_3_global() { + let value: [u8; 3] = kani::any(); + exercise_data_ptr(&value); + } + + #[kani::proof] + pub fn harness_data_ptr_unsized_slice_u8_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + exercise_data_ptr(slice); + } + + #[kani::proof] + pub fn harness_data_ptr_unsized_slice_u16_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + exercise_data_ptr(slice); + } + + #[kani::proof] + pub fn harness_data_ptr_unsized_slice_u32_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + exercise_data_ptr(slice); + } + + #[kani::proof] + pub fn harness_data_ptr_dyn_any_i32_global() { + let value: i32 = kani::any(); + let trait_obj: &dyn Any = &value; + exercise_data_ptr(trait_obj); + } + + #[kani::proof] + pub fn harness_data_ptr_bool_global() { + let value: bool = kani::any(); + exercise_data_ptr(&value); + } + + #[kani::proof] + pub fn harness_data_ptr_nested_rc_i32_global() { + let value: Rc = Rc::new_in(kani::any::(), Global); + exercise_data_ptr(&value); + } + + #[kani::proof] + pub fn harness_data_ptr_tuple_i32_string_global() { + let value: (i32, String) = (kani::any::(), String::new()); + exercise_data_ptr(&value); + } + + #[kani::proof] + pub fn harness_data_ptr_option_i32_global() { + let value: Option = kani::any(); + exercise_data_ptr(&value); + } + + #[kani::proof] + pub fn harness_data_ptr_cell_i32_global() { + let value = Cell::new(kani::any::()); + exercise_data_ptr(&value); + } +} + +#[cfg(kani)] +mod verify_4543 { + use super::kani_rc_harness_helpers::*; + use super::*; + use core::any::Any; + use core::cell::Cell; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + fn exercise_drop(for_value: &T) { + let uninit: UniqueRcUninit = UniqueRcUninit::new(for_value, Global); + core::mem::drop(uninit); + } + + #[kani::proof] + pub fn harness_drop_u8_global() { + let value: u8 = kani::any(); + exercise_drop(&value); + } + + #[kani::proof] + pub fn harness_drop_i32_global() { + let value: i32 = kani::any(); + exercise_drop(&value); + } + + #[kani::proof] + pub fn harness_drop_u64_global() { + let value: u64 = kani::any(); + exercise_drop(&value); + } + + #[kani::proof] + pub fn harness_drop_unit_global() { + let value = (); + exercise_drop(&value); + } + + #[kani::proof] + pub fn harness_drop_drop_sentinel_global() { + let value = DropSentinel(kani::any()); + exercise_drop(&value); + } + + #[kani::proof] + pub fn harness_drop_array_u8_3_global() { + let value: [u8; 3] = kani::any(); + exercise_drop(&value); + } + + #[kani::proof] + pub fn harness_drop_unsized_slice_u8_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + exercise_drop(slice); + } + + #[kani::proof] + pub fn harness_drop_unsized_slice_u16_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + exercise_drop(slice); + } + + #[kani::proof] + pub fn harness_drop_unsized_slice_u32_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice(&vec); + exercise_drop(slice); + } + + #[kani::proof] + pub fn harness_drop_dyn_any_i32_global() { + let value: i32 = kani::any(); + let trait_obj: &dyn Any = &value; + exercise_drop(trait_obj); + } + + #[kani::proof] + pub fn harness_drop_bool_global() { + let value: bool = kani::any(); + exercise_drop(&value); + } + + #[kani::proof] + pub fn harness_drop_nested_rc_i32_global() { + let value: Rc = Rc::new_in(kani::any::(), Global); + exercise_drop(&value); + } + + #[kani::proof] + pub fn harness_drop_tuple_i32_string_global() { + let value: (i32, String) = (kani::any::(), String::from("test")); + exercise_drop(&value); + } + + #[kani::proof] + pub fn harness_drop_option_i32_global() { + let value: Option = kani::any(); + exercise_drop(&value); + } + + #[kani::proof] + pub fn harness_drop_cell_i32_global() { + let value = Cell::new(kani::any::()); + exercise_drop(&value); + } +} + +#[cfg(kani)] +mod verify_368 { + use super::kani_rc_harness_helpers::*; + use super::*; + use core::any::Any; + use core::cell::Cell; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + fn exercise_inner(value: Rc) { + let _ = value.inner(); + } + + #[kani::proof] + pub fn harness_inner_u8_global() { + let value: u8 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_inner(rc); + } + + #[kani::proof] + pub fn harness_inner_i32_global() { + let value: i32 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_inner(rc); + } + + #[kani::proof] + pub fn harness_inner_u64_global() { + let value: u64 = kani::any(); + let rc: Rc = Rc::new_in(value, Global); + exercise_inner(rc); + } + + #[kani::proof] + pub fn harness_inner_unit_global() { + let rc: Rc<(), Global> = Rc::new_in((), Global); + exercise_inner(rc); + } + + #[kani::proof] + pub fn harness_inner_drop_sentinel_global() { + let rc: Rc = Rc::new_in(DropSentinel(kani::any()), Global); + exercise_inner(rc); + } + + #[kani::proof] + pub fn harness_inner_array_u8_3_global() { + let value: [u8; 3] = kani::any(); + let rc: Rc<[u8; 3], Global> = Rc::new_in(value, Global); + exercise_inner(rc); + } + + #[kani::proof] + pub fn harness_inner_unsized_slice_u8_global() { + let vec = verifier_nondet_vec::(); + let rc = nondet_rc_slice(&vec); + let _ = Rc::new(&rc).inner(); + } + + #[kani::proof] + pub fn harness_inner_unsized_slice_u16_global() { + let vec = verifier_nondet_vec::(); + let rc = nondet_rc_slice(&vec); + let _ = Rc::new(&rc).inner(); + } + + #[kani::proof] + pub fn harness_inner_unsized_slice_u32_global() { + let vec = verifier_nondet_vec::(); + let rc = nondet_rc_slice(&vec); + let _ = Rc::new(&rc).inner(); + } + + #[kani::proof] + pub fn harness_inner_dyn_any_i32_global() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_inner(rc); + } + + #[kani::proof] + pub fn harness_inner_bool_global() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_inner(rc); + } + + #[kani::proof] + pub fn harness_inner_tuple_i32_string_global() { + let value: (i32, String) = (kani::any::(), String::from("test")); + let rc: Rc<(i32, String), Global> = Rc::new_in(value, Global); + exercise_inner(rc); + } + + #[kani::proof] + pub fn harness_inner_option_i32_global() { + let rc: Rc, Global> = Rc::new_in(kani::any::>(), Global); + exercise_inner(rc); + } + + #[kani::proof] + pub fn harness_inner_cell_i32_global() { + let rc: Rc, Global> = Rc::new_in(Cell::new(kani::any::()), Global); + exercise_inner(rc); + } +} + +#[cfg(kani)] +mod verify_375 { + use super::kani_rc_harness_helpers::*; + use super::*; + use core::any::Any; + use core::slice; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + fn exercise_into_inner_with_allocator(rc: Rc) { + let (ptr, alloc) = Rc::::into_inner_with_allocator(rc); + let recovered: Rc = unsafe { Rc::::from_inner_in(ptr, alloc) }; + } + + #[kani::proof] + pub fn harness_into_inner_with_allocator_u8_global() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_into_inner_with_allocator(rc); + } + + #[kani::proof] + pub fn harness_into_inner_with_allocator_i32_global() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_into_inner_with_allocator(rc); + } + + #[kani::proof] + pub fn harness_into_inner_with_allocator_u64_global() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_into_inner_with_allocator(rc); + } + + #[kani::proof] + pub fn harness_into_inner_with_allocator_unit_global() { + let rc: Rc<(), Global> = Rc::new_in((), Global); + exercise_into_inner_with_allocator(rc); + } + + #[kani::proof] + // pub fn harness_into_inner_with_allocator_string_global() { + pub fn harness_into_inner_with_allocator_vec_u8() { + // let s = String::from("test"); + let v = verifier_nondet_vec::(); + let v = core::mem::forget(v); + let rc: Rc<_, Global> = Rc::new_in(v, Global); + exercise_into_inner_with_allocator(rc); + } + + #[kani::proof] + pub fn harness_into_inner_with_allocator_drop_sentinel_global() { + let rc: Rc = Rc::new_in(DropSentinel(kani::any()), Global); + exercise_into_inner_with_allocator(rc); + } + + #[kani::proof] + pub fn harness_into_inner_with_allocator_array_u8_3_global() { + let rc: Rc<[u8; 3], Global> = Rc::new_in(kani::any::<[u8; 3]>(), Global); + exercise_into_inner_with_allocator(rc); + } + + #[kani::proof] + pub fn harness_into_inner_with_allocator_slice_u8_global() { + let value: [u8; 3] = kani::any(); + let rc: Rc<[u8], Global> = Rc::from(value); + exercise_into_inner_with_allocator(rc); + } + + #[kani::proof] + pub fn harness_into_inner_with_allocator_slice_string_global() { + let value: [String; 2] = [String::from("test"), String::from("test2")]; + let rc: Rc<[String], Global> = Rc::from(value); + exercise_into_inner_with_allocator(rc); + } + + #[kani::proof] + pub fn harness_into_inner_with_allocator_str_global() { + let rc: Rc = Rc::from("test"); + exercise_into_inner_with_allocator(rc); + } + + #[kani::proof] + pub fn harness_into_inner_with_allocator_dyn_any_i32_global() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_into_inner_with_allocator(rc); + } + + #[kani::proof] + pub fn harness_into_inner_with_allocator_bool_global() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_into_inner_with_allocator(rc); + } + + #[kani::proof] + pub fn harness_into_inner_with_allocator_array_u8_0_global() { + let rc: Rc<[u8; 0], Global> = Rc::new_in([], Global); + exercise_into_inner_with_allocator(rc); + } + + #[kani::proof] + pub fn harness_into_inner_with_allocator_tuple_i32_string_global() { + let rc: Rc<(i32, String), Global> = + Rc::new_in((kani::any::(), String::from("test")), Global); + exercise_into_inner_with_allocator(rc); + } + + #[kani::proof] + pub fn harness_into_inner_with_allocator_option_i32_global() { + let rc: Rc, Global> = Rc::new_in(kani::any::>(), Global); + exercise_into_inner_with_allocator(rc); + } + + #[kani::proof] + pub fn harness_into_inner_with_allocator_slice_unit_global() { + let value: [(); 1] = [()]; + let rc: Rc<[()], Global> = Rc::from(value); + exercise_into_inner_with_allocator(rc); + } + + #[kani::proof] + pub fn harness_into_inner_with_allocator_unsized_slice_u8_global() { + let value = verifier_nondet_vec::(); + let slice = nondet_rc_slice::(&value); + let rc: Rc<[u8], Global> = Rc::from(slice); + exercise_into_inner_with_allocator(rc); + } + + #[kani::proof] + pub fn harness_into_inner_with_allocator_unsized_slice_u16_global() { + let value = verifier_nondet_vec::(); + let slice = nondet_rc_slice::(&value); + let rc: Rc<[u16], Global> = Rc::from(slice); + exercise_into_inner_with_allocator(rc); + } +} + +#[cfg(kani)] +mod verify_425 { + use super::*; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + #[kani::proof] + pub fn harness_rc_new_u8() { + let value: u8 = kani::any(); + let rc: Rc = Rc::new(value); + drop(rc); + } + + #[kani::proof] + pub fn harness_rc_new_i32() { + let value: i32 = kani::any(); + let rc: Rc = Rc::new(value); + drop(rc); + } + + #[kani::proof] + pub fn harness_rc_new_u64() { + let value: u64 = kani::any(); + let rc: Rc = Rc::new(value); + drop(rc); + } + + #[kani::proof] + pub fn harness_rc_new_unit() { + let rc: Rc<()> = Rc::new(()); + drop(rc); + } + + #[kani::proof] + pub fn harness_rc_new_drop_sentinel() { + let rc: Rc = Rc::new(DropSentinel(kani::any())); + drop(rc); + } + + #[kani::proof] + pub fn harness_rc_new_array_u8_3() { + let value: [u8; 3] = kani::any(); + let rc: Rc<[u8; 3]> = Rc::new(value); + drop(rc); + } + + #[kani::proof] + pub fn harness_rc_new_bool() { + let value: bool = kani::any(); + let rc: Rc = Rc::new(value); + drop(rc); + } + + #[kani::proof] + pub fn harness_rc_new_option_i32() { + let value: Option = kani::any(); + let rc: Rc> = Rc::new(value); + drop(rc); + } +} + +#[cfg(kani)] +mod verify_521 { + use super::*; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + #[kani::proof] + pub fn harness_rc_new_uninit_u8() { + let rc: Rc> = Rc::::new_uninit(); + drop(rc); + } + + #[kani::proof] + pub fn harness_rc_new_uninit_i32() { + let rc: Rc> = Rc::::new_uninit(); + drop(rc); + } + + #[kani::proof] + pub fn harness_rc_new_uninit_u64() { + let rc: Rc> = Rc::::new_uninit(); + drop(rc); + } + + #[kani::proof] + pub fn harness_rc_new_uninit_unit() { + let rc: Rc> = Rc::<()>::new_uninit(); + drop(rc); + } + + #[kani::proof] + pub fn harness_rc_new_uninit_string() { + let rc: Rc> = Rc::::new_uninit(); + drop(rc); + } + + #[kani::proof] + pub fn harness_rc_new_uninit_drop_sentinel() { + let rc: Rc> = Rc::::new_uninit(); + drop(rc); + } + + #[kani::proof] + pub fn harness_rc_new_uninit_array_u8_3() { + let rc: Rc> = Rc::<[u8; 3]>::new_uninit(); + drop(rc); + } + + #[kani::proof] + pub fn harness_rc_new_uninit_bool() { + let rc: Rc> = Rc::::new_uninit(); + drop(rc); + } + + #[kani::proof] + pub fn harness_rc_new_uninit_nested_rc_i32() { + let rc: Rc>> = Rc::>::new_uninit(); + drop(rc); + } + + #[kani::proof] + pub fn harness_rc_new_uninit_tuple_i32_string() { + let rc: Rc> = Rc::<(i32, String)>::new_uninit(); + drop(rc); + } + + #[kani::proof] + pub fn harness_rc_new_uninit_option_i32() { + let rc: Rc>> = Rc::>::new_uninit(); + drop(rc); + } +} + +#[cfg(kani)] +mod verify_552 { + use super::*; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + #[kani::proof] + pub fn harness_rc_new_zeroed_u8() { + let rc: Rc> = Rc::::new_zeroed(); + drop(rc); + } + + #[kani::proof] + pub fn harness_rc_new_zeroed_i32() { + let rc: Rc> = Rc::::new_zeroed(); + drop(rc); + } + + #[kani::proof] + pub fn harness_rc_new_zeroed_u64() { + let rc: Rc> = Rc::::new_zeroed(); + drop(rc); + } + + #[kani::proof] + pub fn harness_rc_new_zeroed_unit() { + let rc: Rc> = Rc::<()>::new_zeroed(); + drop(rc); + } + + #[kani::proof] + pub fn harness_rc_new_zeroed_string() { + let rc: Rc> = Rc::::new_zeroed(); + drop(rc); + } + + #[kani::proof] + pub fn harness_rc_new_zeroed_drop_sentinel() { + let rc: Rc> = Rc::::new_zeroed(); + drop(rc); + } + + #[kani::proof] + pub fn harness_rc_new_zeroed_array_u8_3() { + let rc: Rc> = Rc::<[u8; 3]>::new_zeroed(); + drop(rc); + } + + #[kani::proof] + pub fn harness_rc_new_zeroed_bool() { + let rc: Rc> = Rc::::new_zeroed(); + drop(rc); + } + + #[kani::proof] + pub fn harness_rc_new_zeroed_nested_rc_i32() { + let rc: Rc>> = Rc::>::new_zeroed(); + drop(rc); + } + + #[kani::proof] + pub fn harness_rc_new_zeroed_tuple_i32_string() { + let rc: Rc> = Rc::<(i32, String)>::new_zeroed(); + drop(rc); + } + + #[kani::proof] + pub fn harness_rc_new_zeroed_option_i32() { + let rc: Rc>> = Rc::>::new_zeroed(); + drop(rc); + } +} + +#[cfg(kani)] +mod verify_711 { + use super::*; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + #[kani::proof] + pub fn harness_new_uninit_in_u8_single_path_global() { + let rc: Rc, Global> = Rc::::new_uninit_in(Global); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_uninit_in_i32_single_path_global() { + let rc: Rc, Global> = Rc::::new_uninit_in(Global); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_uninit_in_u64_single_path_global() { + let rc: Rc, Global> = Rc::::new_uninit_in(Global); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_uninit_in_unit_single_path_global() { + let rc: Rc, Global> = Rc::<(), Global>::new_uninit_in(Global); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_uninit_in_string_single_path_global() { + let rc: Rc, Global> = Rc::::new_uninit_in(Global); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_uninit_in_drop_sentinel_single_path_global() { + let rc: Rc, Global> = + Rc::::new_uninit_in(Global); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_uninit_in_array_u8_3_single_path_global() { + let rc: Rc, Global> = + Rc::<[u8; 3], Global>::new_uninit_in(Global); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_uninit_in_bool_single_path_global() { + let rc: Rc, Global> = Rc::::new_uninit_in(Global); + // drop(rc); + } + + #[kani::proof] + pub fn harness_new_uninit_in_nested_rc_i32_single_path_global() { + let rc: Rc>, Global> = + Rc::, Global>::new_uninit_in(Global); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_uninit_in_tuple_i32_string_single_path_global() { + let rc: Rc, Global> = + Rc::<(i32, String), Global>::new_uninit_in(Global); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_uninit_in_option_i32_single_path_global() { + let rc: Rc>, Global> = + Rc::, Global>::new_uninit_in(Global); + drop(rc); + } +} + +#[cfg(kani)] +mod verify_748 { + use super::*; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + #[kani::proof] + pub fn harness_new_zeroed_in_u8_single_path_global() { + let rc: Rc, Global> = Rc::::new_zeroed_in(Global); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_zeroed_in_i32_single_path_global() { + let rc: Rc, Global> = Rc::::new_zeroed_in(Global); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_zeroed_in_u64_single_path_global() { + let rc: Rc, Global> = Rc::::new_zeroed_in(Global); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_zeroed_in_unit_single_path_global() { + let rc: Rc, Global> = Rc::<(), Global>::new_zeroed_in(Global); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_zeroed_in_string_single_path_global() { + let rc: Rc, Global> = Rc::::new_zeroed_in(Global); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_zeroed_in_drop_sentinel_single_path_global() { + let rc: Rc, Global> = + Rc::::new_zeroed_in(Global); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_zeroed_in_array_u8_3_single_path_global() { + let rc: Rc, Global> = + Rc::<[u8; 3], Global>::new_zeroed_in(Global); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_zeroed_in_bool_single_path_global() { + let rc: Rc, Global> = Rc::::new_zeroed_in(Global); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_zeroed_in_nested_rc_i32_single_path_global() { + let rc: Rc>, Global> = + Rc::, Global>::new_zeroed_in(Global); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_zeroed_in_tuple_i32_string_single_path_global() { + let rc: Rc, Global> = + Rc::<(i32, String), Global>::new_zeroed_in(Global); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_zeroed_in_option_i32_single_path_global() { + let rc: Rc>, Global> = + Rc::, Global>::new_zeroed_in(Global); + drop(rc); + } +} + +#[cfg(kani)] +mod verify_792 { + use super::*; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + #[kani::proof] + pub fn harness_new_cyclic_in_u8_single_path_global() { + let rc: Rc = Rc::::new_cyclic_in( + |weak: &Weak| { + let _ = weak.upgrade(); + kani::any::() + }, + Global, + ); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_cyclic_in_i32_single_path_global() { + let rc: Rc = Rc::::new_cyclic_in( + |weak: &Weak| { + let _ = weak.upgrade(); + kani::any::() + }, + Global, + ); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_cyclic_in_u64_single_path_global() { + let rc: Rc = Rc::::new_cyclic_in( + |weak: &Weak| { + let _ = weak.upgrade(); + kani::any::() + }, + Global, + ); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_cyclic_in_unit_single_path_global() { + let rc: Rc<(), Global> = Rc::<(), Global>::new_cyclic_in( + |weak: &Weak<(), Global>| { + let _ = weak.upgrade(); + }, + Global, + ); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_cyclic_in_string_single_path_global() { + let rc: Rc = Rc::::new_cyclic_in( + |weak: &Weak| { + let _ = weak.upgrade(); + String::from("test") + }, + Global, + ); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_cyclic_in_drop_sentinel_single_path_global() { + let rc: Rc = Rc::::new_cyclic_in( + |weak: &Weak| { + let _ = weak.upgrade(); + DropSentinel(kani::any()) + }, + Global, + ); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_cyclic_in_array_u8_3_single_path_global() { + let rc: Rc<[u8; 3], Global> = Rc::<[u8; 3], Global>::new_cyclic_in( + |weak: &Weak<[u8; 3], Global>| { + let _ = weak.upgrade(); + kani::any::<[u8; 3]>() + }, + Global, + ); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_cyclic_in_bool_single_path_global() { + let rc: Rc = Rc::::new_cyclic_in( + |weak: &Weak| { + let _ = weak.upgrade(); + kani::any::() + }, + Global, + ); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_cyclic_in_nested_rc_i32_single_path_global() { + let rc: Rc, Global> = Rc::, Global>::new_cyclic_in( + |weak: &Weak, Global>| { + let _ = weak.upgrade(); + Rc::new_in(kani::any::(), Global) + }, + Global, + ); + core::mem::forget(rc); + } + + #[kani::proof] + pub fn harness_new_cyclic_in_tuple_i32_string_single_path_global() { + let rc: Rc<(i32, String), Global> = Rc::<(i32, String), Global>::new_cyclic_in( + |weak: &Weak<(i32, String), Global>| { + let _ = weak.upgrade(); + (kani::any::(), String::new()) + }, + Global, + ); + drop(rc); + } + + #[kani::proof] + pub fn harness_new_cyclic_in_option_i32_single_path_global() { + let rc: Rc, Global> = Rc::, Global>::new_cyclic_in( + |weak: &Weak, Global>| { + let _ = weak.upgrade(); + kani::any::>() + }, + Global, + ); + drop(rc); + } +} + +#[cfg(kani)] +mod verify_857 { + use super::*; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + #[kani::proof] + pub fn harness_try_new_in_u8_single_path_global() { + let value: u8 = kani::any(); + let result = Rc::::try_new_in(value, Global); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_in_i32_single_path_global() { + let value: i32 = kani::any(); + let result = Rc::::try_new_in(value, Global); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_in_u64_single_path_global() { + let value: u64 = kani::any(); + let result = Rc::::try_new_in(value, Global); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_in_unit_single_path_global() { + let result = Rc::<(), Global>::try_new_in((), Global); + drop(result); + } + + #[kani::proof] + // pub fn harness_try_new_in_string_single_path_global() { + pub fn harness_try_new_in_vec_u8() { + use crate::rc::kani_rc_harness_helpers::*; + let vec = verifier_nondet_vec::(); + let _ = Rc::<_, Global>::try_new_in(vec, Global); + // let result = Rc::::try_new_in(String::from("test"), Global); + // drop(result); + } + + #[kani::proof] + pub fn harness_try_new_in_drop_sentinel_single_path_global() { + let value = DropSentinel(kani::any()); + let result = Rc::::try_new_in(value, Global); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_in_array_u8_3_single_path_global() { + let value: [u8; 3] = kani::any(); + let result = Rc::<[u8; 3], Global>::try_new_in(value, Global); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_in_bool_single_path_global() { + let value: bool = kani::any(); + let result = Rc::::try_new_in(value, Global); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_in_nested_rc_i32_single_path_global() { + let inner: Rc = Rc::new_in(kani::any::(), Global); + let result = Rc::, Global>::try_new_in(inner, Global); + if let Ok(rc) = result { + core::mem::forget(rc); + } + } + + #[kani::proof] + pub fn harness_try_new_in_tuple_i32_string_single_path_global() { + let value: (i32, String) = (kani::any::(), String::from("test")); + let result = Rc::<(i32, String), Global>::try_new_in(value, Global); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_in_option_i32_single_path_global() { + let value: Option = kani::any(); + let result = Rc::, Global>::try_new_in(value, Global); + drop(result); + } +} + +#[cfg(kani)] +mod verify_899 { + use super::*; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + #[kani::proof] + pub fn harness_try_new_uninit_in_u8_single_path_global() { + let result = Rc::::try_new_uninit_in(Global); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_uninit_in_i32_single_path_global() { + let result = Rc::::try_new_uninit_in(Global); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_uninit_in_u64_single_path_global() { + let result = Rc::::try_new_uninit_in(Global); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_uninit_in_unit_single_path_global() { + let result = Rc::<(), Global>::try_new_uninit_in(Global); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_uninit_in_string_single_path_global() { + let result = Rc::::try_new_uninit_in(Global); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_uninit_in_drop_sentinel_single_path_global() { + let result = Rc::::try_new_uninit_in(Global); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_uninit_in_array_u8_3_single_path_global() { + let result = Rc::<[u8; 3], Global>::try_new_uninit_in(Global); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_uninit_in_bool_single_path_global() { + let result = Rc::::try_new_uninit_in(Global); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_uninit_in_nested_rc_i32_single_path_global() { + let result = Rc::, Global>::try_new_uninit_in(Global); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_uninit_in_tuple_i32_string_single_path_global() { + let result = Rc::<(i32, String), Global>::try_new_uninit_in(Global); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_uninit_in_option_i32_single_path_global() { + let result = Rc::, Global>::try_new_uninit_in(Global); + drop(result); + } +} + +#[cfg(kani)] +mod verify_937 { + use super::*; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + #[kani::proof] + pub fn harness_try_new_zeroed_in_u8_single_path_global() { + let result = Rc::::try_new_zeroed_in(Global); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_zeroed_in_i32_single_path_global() { + let result = Rc::::try_new_zeroed_in(Global); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_zeroed_in_u64_single_path_global() { + let result = Rc::::try_new_zeroed_in(Global); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_zeroed_in_unit_single_path_global() { + let result = Rc::<(), Global>::try_new_zeroed_in(Global); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_zeroed_in_string_single_path_global() { + let result = Rc::::try_new_zeroed_in(Global); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_zeroed_in_drop_sentinel_single_path_global() { + let result = Rc::::try_new_zeroed_in(Global); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_zeroed_in_array_u8_3_single_path_global() { + let result = Rc::<[u8; 3], Global>::try_new_zeroed_in(Global); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_zeroed_in_bool_single_path_global() { + let result = Rc::::try_new_zeroed_in(Global); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_zeroed_in_nested_rc_i32_single_path_global() { + let result = Rc::, Global>::try_new_zeroed_in(Global); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_zeroed_in_tuple_i32_string_single_path_global() { + let result = Rc::<(i32, String), Global>::try_new_zeroed_in(Global); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_zeroed_in_option_i32_single_path_global() { + let result = Rc::, Global>::try_new_zeroed_in(Global); + drop(result); + } +} + +#[cfg(kani)] +mod verify_955 { + use super::*; + use core::marker::PhantomPinned; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + struct NotUnpinSentinel(u8, PhantomPinned); + + #[kani::proof] + pub fn harness_pin_in_u8_single_path_global() { + let value: u8 = kani::any(); + let pinned = Rc::::pin_in(value, Global); + drop(pinned); + } + + #[kani::proof] + pub fn harness_pin_in_i32_single_path_global() { + let value: i32 = kani::any(); + let pinned = Rc::::pin_in(value, Global); + drop(pinned); + } + + #[kani::proof] + pub fn harness_pin_in_u64_single_path_global() { + let value: u64 = kani::any(); + let pinned = Rc::::pin_in(value, Global); + drop(pinned); + } + + #[kani::proof] + pub fn harness_pin_in_unit_single_path_global() { + let pinned = Rc::<(), Global>::pin_in((), Global); + drop(pinned); + } + + #[kani::proof] + // pub fn harness_pin_in_string_single_path_global() { + pub fn harness_pin_in_vec_u8() { + use crate::rc::kani_rc_harness_helpers::*; + let v = verifier_nondet_vec::(); + let _ = Rc::<_, Global>::pin_in(v, Global); + // let pinned = Rc::::pin_in(String::from("test"), Global); + // drop(pinned); + } + + #[kani::proof] + pub fn harness_pin_in_drop_sentinel_single_path_global() { + let value = DropSentinel(kani::any()); + let pinned = Rc::::pin_in(value, Global); + drop(pinned); + } + + #[kani::proof] + pub fn harness_pin_in_array_u8_3_single_path_global() { + let value: [u8; 3] = kani::any(); + let pinned = Rc::<[u8; 3], Global>::pin_in(value, Global); + drop(pinned); + } + + #[kani::proof] + pub fn harness_pin_in_not_unpin_sentinel_single_path_global() { + let value = NotUnpinSentinel(kani::any(), PhantomPinned); + let pinned = Rc::::pin_in(value, Global); + drop(pinned); + } + + #[kani::proof] + pub fn harness_pin_in_bool_single_path_global() { + let value: bool = kani::any(); + let pinned = Rc::::pin_in(value, Global); + drop(pinned); + } + + #[kani::proof] + pub fn harness_pin_in_tuple_i32_string_single_path_global() { + let value = (kani::any::(), String::from("test")); + let pinned = Rc::<(i32, String), Global>::pin_in(value, Global); + drop(pinned); + } + + #[kani::proof] + pub fn harness_pin_in_option_i32_single_path_global() { + let value: Option = kani::any(); + let pinned = Rc::, Global>::pin_in(value, Global); + drop(pinned); + } +} + +#[cfg(kani)] +mod verify_1065 { + use super::kani_rc_harness_helpers::*; + use super::*; + + macro_rules! gen_new_uninit_slice_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + type T = $ty; + let len = kani::any_where(|l: &usize| rc_slice_layout_ok::(*l)); + let _rc: Rc<[mem::MaybeUninit]> = Rc::<[T]>::new_uninit_slice(len); + } + }; + } + + gen_new_uninit_slice_harness!(harness_new_uninit_slice_i8, i8); + gen_new_uninit_slice_harness!(harness_new_uninit_slice_i16, i16); + gen_new_uninit_slice_harness!(harness_new_uninit_slice_i32, i32); + gen_new_uninit_slice_harness!(harness_new_uninit_slice_i64, i64); + gen_new_uninit_slice_harness!(harness_new_uninit_slice_i128, i128); + gen_new_uninit_slice_harness!(harness_new_uninit_slice_u8, u8); + gen_new_uninit_slice_harness!(harness_new_uninit_slice_u16, u16); + gen_new_uninit_slice_harness!(harness_new_uninit_slice_u32, u32); + gen_new_uninit_slice_harness!(harness_new_uninit_slice_u64, u64); + gen_new_uninit_slice_harness!(harness_new_uninit_slice_u128, u128); + gen_new_uninit_slice_harness!(harness_new_uninit_slice_unit, ()); + gen_new_uninit_slice_harness!(harness_new_uninit_slice_bool, bool); + gen_new_uninit_slice_harness!(harness_new_uninit_slice_string, String); + gen_new_uninit_slice_harness!(harness_new_uninit_slice_array_u8_arr, [u8; 4]); +} + +#[cfg(kani)] +mod verify_1090 { + use super::*; + use crate::rc::kani_rc_harness_helpers::*; + + macro_rules! gen_new_zeroed_slice_harness { + ($name:ident, $elem_ty:ty) => { + #[kani::proof] + pub fn $name() { + let len = kani::any_where(|l: &usize| rc_slice_layout_ok::<$elem_ty>(*l)); + let _rc: Rc<[mem::MaybeUninit<$elem_ty>]> = Rc::<[$elem_ty]>::new_zeroed_slice(len); + } + }; + } + + gen_new_zeroed_slice_harness!(harness_new_zeroed_slice_i8, i8); + gen_new_zeroed_slice_harness!(harness_new_zeroed_slice_i16, i16); + gen_new_zeroed_slice_harness!(harness_new_zeroed_slice_i32, i32); + gen_new_zeroed_slice_harness!(harness_new_zeroed_slice_i64, i64); + gen_new_zeroed_slice_harness!(harness_new_zeroed_slice_i128, i128); + gen_new_zeroed_slice_harness!(harness_new_zeroed_slice_u8, u8); + gen_new_zeroed_slice_harness!(harness_new_zeroed_slice_u16, u16); + gen_new_zeroed_slice_harness!(harness_new_zeroed_slice_u32, u32); + gen_new_zeroed_slice_harness!(harness_new_zeroed_slice_u64, u64); + gen_new_zeroed_slice_harness!(harness_new_zeroed_slice_u128, u128); + gen_new_zeroed_slice_harness!(harness_new_zeroed_slice_unit, ()); + gen_new_zeroed_slice_harness!(harness_new_zeroed_slice_bool, bool); + gen_new_zeroed_slice_harness!(harness_new_zeroed_slice_string, String); + gen_new_zeroed_slice_harness!(harness_new_zeroed_slice_array_u8_4, [u8; 4]); +} + +#[cfg(kani)] +mod verify_1111 { + use super::*; + use crate::rc::kani_rc_harness_helpers::*; + + fn exercise_into_array(rc: Rc<[T]>) { + let _: Option> = rc.into_array::(); + } + + macro_rules! gen_into_array_nondet_vec_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + type T = $ty; + let vec = verifier_nondet_vec_rc::(); + let slice = Rc::from(vec); + + const N: usize = 100; + exercise_into_array::(slice); + } + }; + } + + gen_into_array_nondet_vec_harness!(harness_into_array_nondet_i8, i8); + gen_into_array_nondet_vec_harness!(harness_into_array_nondet_i16, i16); + gen_into_array_nondet_vec_harness!(harness_into_array_nondet_i32, i32); + gen_into_array_nondet_vec_harness!(harness_into_array_nondet_i64, i64); + gen_into_array_nondet_vec_harness!(harness_into_array_nondet_i128, i128); + gen_into_array_nondet_vec_harness!(harness_into_array_nondet_u8, u8); + gen_into_array_nondet_vec_harness!(harness_into_array_nondet_u16, u16); + gen_into_array_nondet_vec_harness!(harness_into_array_nondet_u32, u32); + gen_into_array_nondet_vec_harness!(harness_into_array_nondet_u64, u64); + gen_into_array_nondet_vec_harness!(harness_into_array_nondet_u128, u128); + gen_into_array_nondet_vec_harness!(harness_into_array_nondet_unit, ()); + gen_into_array_nondet_vec_harness!(harness_into_array_nondet_bool, bool); + gen_into_array_nondet_vec_harness!(harness_into_array_nondet_array_u8_4, [u8; 4]); +} + +#[cfg(kani)] +mod verify_657 { + use super::*; + use crate::rc::kani_rc_harness_helpers::*; + + macro_rules! gen_pin_in_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + let value: $ty = kani::any(); + let _pinned = Rc::pin_in(value, Global); + } + }; + } + + gen_pin_in_harness!(harness_pin_in_i8, i8); + gen_pin_in_harness!(harness_pin_in_i16, i16); + gen_pin_in_harness!(harness_pin_in_i32, i32); + gen_pin_in_harness!(harness_pin_in_i64, i64); + gen_pin_in_harness!(harness_pin_in_i128, i128); + gen_pin_in_harness!(harness_pin_in_u8, u8); + gen_pin_in_harness!(harness_pin_in_u16, u16); + gen_pin_in_harness!(harness_pin_in_u32, u32); + gen_pin_in_harness!(harness_pin_in_u64, u64); + gen_pin_in_harness!(harness_pin_in_u128, u128); + gen_pin_in_harness!(harness_pin_in_unit, ()); + gen_pin_in_harness!(harness_pin_in_bool, bool); + gen_pin_in_harness!(harness_pin_in_array_u8_4, [u8; 4]); +} + +#[cfg(kani)] +mod verify_1152 { + use super::*; + use crate::rc::kani_rc_harness_helpers::*; + + macro_rules! gen_new_uninit_slice_in_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + type T = $ty; + let len = kani::any_where(|l: &usize| rc_slice_layout_ok::(*l)); + let _rc: Rc<[mem::MaybeUninit]> = Rc::<[T]>::new_uninit_slice_in(len, Global); + } + }; + } + + gen_new_uninit_slice_in_harness!(harness_new_uninit_slice_in_i8, i8); + gen_new_uninit_slice_in_harness!(harness_new_uninit_slice_in_i16, i16); + gen_new_uninit_slice_in_harness!(harness_new_uninit_slice_in_i32, i32); + gen_new_uninit_slice_in_harness!(harness_new_uninit_slice_in_i64, i64); + gen_new_uninit_slice_in_harness!(harness_new_uninit_slice_in_i128, i128); + gen_new_uninit_slice_in_harness!(harness_new_uninit_slice_in_u8, u8); + gen_new_uninit_slice_in_harness!(harness_new_uninit_slice_in_u16, u16); + gen_new_uninit_slice_in_harness!(harness_new_uninit_slice_in_u32, u32); + gen_new_uninit_slice_in_harness!(harness_new_uninit_slice_in_u64, u64); + gen_new_uninit_slice_in_harness!(harness_new_uninit_slice_in_u128, u128); + gen_new_uninit_slice_in_harness!(harness_new_uninit_slice_in_unit, ()); + gen_new_uninit_slice_in_harness!(harness_new_uninit_slice_in_bool, bool); + gen_new_uninit_slice_in_harness!(harness_new_uninit_slice_in_array_u8_4, [u8; 4]); + + // #[kani::proof] + // pub fn harness_new_uninit_slice_in_i32_single_path_global() { + // let len: usize = kani::any::() as usize; + // let rc = Rc::<[i32], Global>::new_uninit_slice_in(len, Global); + // drop(rc); + // } + + // #[kani::proof] + // pub fn harness_new_uninit_slice_in_unit_single_path_global() { + // let len: usize = kani::any::() as usize; + // let rc = Rc::<[()], Global>::new_uninit_slice_in(len, Global); + // drop(rc); + // } + + // #[kani::proof] + // pub fn harness_new_uninit_slice_in_string_single_path_global() { + // let len: usize = kani::any::() as usize; + // let rc = Rc::<[String], Global>::new_uninit_slice_in(len, Global); + // drop(rc); + // } + + // #[kani::proof] + // pub fn harness_new_uninit_slice_in_array_u8_3_single_path_global() { + // let len: usize = kani::any::() as usize; + // let rc = Rc::<[[u8; 3]], Global>::new_uninit_slice_in(len, Global); + // drop(rc); + // } + + // #[kani::proof] + // pub fn harness_new_uninit_slice_in_u8_single_path_global() { + // let len: usize = kani::any::() as usize; + // let rc = Rc::<[u8], Global>::new_uninit_slice_in(len, Global); + // drop(rc); + // } + + // #[kani::proof] + // pub fn harness_new_uninit_slice_in_drop_sentinel_single_path_global() { + // let len: usize = kani::any::() as usize; + // let rc = Rc::<[DropSentinel], Global>::new_uninit_slice_in(len, Global); + // drop(rc); + // } + + // #[kani::proof] + // pub fn harness_new_uninit_slice_in_nested_rc_i32_single_path_global() { + // let len: usize = kani::any::() as usize; + // let rc = Rc::<[Rc], Global>::new_uninit_slice_in(len, Global); + // drop(rc); + // } +} + +#[cfg(kani)] +mod verify_574 { + use super::*; + use crate::rc::kani_rc_harness_helpers::*; + + macro_rules! gen_try_new_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + let _result = Rc::<$ty>::try_new(kani::any::<$ty>()); + } + }; + } + + gen_try_new_harness!(harness_try_new_i8, i8); + gen_try_new_harness!(harness_try_new_i16, i16); + gen_try_new_harness!(harness_try_new_i32, i32); + gen_try_new_harness!(harness_try_new_i64, i64); + gen_try_new_harness!(harness_try_new_i128, i128); + gen_try_new_harness!(harness_try_new_u8, u8); + gen_try_new_harness!(harness_try_new_u16, u16); + gen_try_new_harness!(harness_try_new_u32, u32); + gen_try_new_harness!(harness_try_new_u64, u64); + gen_try_new_harness!(harness_try_new_u128, u128); + gen_try_new_harness!(harness_try_new_unit, ()); + gen_try_new_harness!(harness_try_new_bool, bool); + gen_try_new_harness!(harness_try_new_tuple, (u8, i32)); + gen_try_new_harness!(harness_try_new_array_u8, [u8; 4]); + + #[kani::proof] + pub fn harness_try_new_vec_u8() { + type T = u8; + let vec = verifier_nondet_vec::(); + let _ = Rc::>::try_new(vec); + } +} + +#[cfg(kani)] +mod verify_611 { + use super::*; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + #[kani::proof] + pub fn harness_try_new_uninit_u8_single_path_global() { + let result = Rc::::try_new_uninit(); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_uninit_i32_single_path_global() { + let result = Rc::::try_new_uninit(); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_uninit_u64_single_path_global() { + let result = Rc::::try_new_uninit(); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_uninit_unit_single_path_global() { + let result = Rc::<()>::try_new_uninit(); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_uninit_string_single_path_global() { + let result = Rc::::try_new_uninit(); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_uninit_drop_sentinel_single_path_global() { + let result = Rc::::try_new_uninit(); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_uninit_array_u8_3_single_path_global() { + let result = Rc::<[u8; 3]>::try_new_uninit(); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_uninit_bool_single_path_global() { + let result = Rc::::try_new_uninit(); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_uninit_nested_rc_i32_single_path_global() { + let result = Rc::>::try_new_uninit(); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_uninit_tuple_i32_string_single_path_global() { + let result = Rc::<(i32, String)>::try_new_uninit(); + drop(result); + } + + #[kani::proof] + pub fn harness_try_new_uninit_option_i32_single_path_global() { + let result = Rc::>::try_new_uninit(); + drop(result); + } +} + +#[cfg(kani)] +mod verify_643 { + use super::*; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + #[kani::proof] + pub fn harness_try_new_zeroed_u8_single_path_global() { + let _ = Rc::::try_new_zeroed(); + } + + #[kani::proof] + pub fn harness_try_new_zeroed_i32_single_path_global() { + let _ = Rc::::try_new_zeroed(); + } + + #[kani::proof] + pub fn harness_try_new_zeroed_u64_single_path_global() { + let _ = Rc::::try_new_zeroed(); + } + + #[kani::proof] + pub fn harness_try_new_zeroed_unit_single_path_global() { + let _ = Rc::<()>::try_new_zeroed(); + } + + #[kani::proof] + pub fn harness_try_new_zeroed_string_single_path_global() { + let _ = Rc::::try_new_zeroed(); + } + + #[kani::proof] + pub fn harness_try_new_zeroed_drop_sentinel_single_path_global() { + let _ = Rc::::try_new_zeroed(); + } + + #[kani::proof] + pub fn harness_try_new_zeroed_array_u8_3_single_path_global() { + let _ = Rc::<[u8; 3]>::try_new_zeroed(); + } + + #[kani::proof] + pub fn harness_try_new_zeroed_bool_single_path_global() { + let _ = Rc::::try_new_zeroed(); + } + + #[kani::proof] + pub fn harness_try_new_zeroed_nested_rc_i32_single_path_global() { + let _ = Rc::>::try_new_zeroed(); + } + + #[kani::proof] + pub fn harness_try_new_zeroed_tuple_i32_string_single_path_global() { + let _ = Rc::<(i32, String)>::try_new_zeroed(); + } + + #[kani::proof] + pub fn harness_try_new_zeroed_option_i32_single_path_global() { + let _ = Rc::>::try_new_zeroed(); + } +} + +#[cfg(kani)] +mod verify_983 { + use super::*; + use crate::rc::kani_rc_harness_helpers::*; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + fn assert_try_unwrap_unique(value: T) { + let rc = Rc::::new_in(value, Global); + let result = Rc::::try_unwrap(rc); + assert!(result.is_ok()); + } + + fn assert_try_unwrap_shared(value: T) { + let rc = Rc::::new_in(value, Global); + let shared = Rc::clone(&rc); + let result = Rc::::try_unwrap(rc); + assert!(result.is_err()); + drop(result); + drop(shared); + } + + fn assert_try_unwrap_weak_present(value: T) { + let rc = Rc::::new_in(value, Global); + let weak = Rc::downgrade(&rc); + let result = Rc::::try_unwrap(rc); + assert!(result.is_ok()); + drop(result); + drop(weak); + } + + #[kani::proof] + pub fn harness_try_unwrap_u8_unique_global() { + assert_try_unwrap_unique(kani::any::()); + } + + #[kani::proof] + pub fn harness_try_unwrap_u8_shared_global() { + assert_try_unwrap_shared(kani::any::()); + } + + #[kani::proof] + pub fn harness_try_unwrap_u8_weak_present_global() { + assert_try_unwrap_weak_present(kani::any::()); + } + + #[kani::proof] + pub fn harness_try_unwrap_i32_unique_global() { + assert_try_unwrap_unique(kani::any::()); + } + + #[kani::proof] + pub fn harness_try_unwrap_i32_shared_global() { + assert_try_unwrap_shared(kani::any::()); + } + + #[kani::proof] + pub fn harness_try_unwrap_i32_weak_present_global() { + assert_try_unwrap_weak_present(kani::any::()); + } + + #[kani::proof] + pub fn harness_try_unwrap_u64_unique_global() { + assert_try_unwrap_unique(kani::any::()); + } + + #[kani::proof] + pub fn harness_try_unwrap_u64_shared_global() { + assert_try_unwrap_shared(kani::any::()); + } + + #[kani::proof] + pub fn harness_try_unwrap_u64_weak_present_global() { + assert_try_unwrap_weak_present(kani::any::()); + } + + #[kani::proof] + pub fn harness_try_unwrap_unit_unique_global() { + assert_try_unwrap_unique(()); + } + + #[kani::proof] + pub fn harness_try_unwrap_unit_shared_global() { + assert_try_unwrap_shared(()); + } + + #[kani::proof] + pub fn harness_try_unwrap_unit_weak_present_global() { + assert_try_unwrap_weak_present(()); + } + + #[kani::proof] + // pub fn harness_try_unwrap_string_unique_global() { + pub fn harness_try_unwrap_unique_vec_u8() { + let vec = verifier_nondet_vec::(); + assert_try_unwrap_unique(vec); + } + + #[kani::proof] + // pub fn harness_try_unwrap_string_shared_global() { + pub fn harness_try_unwrap_shared_global_vec_u8() { + let vec = verifier_nondet_vec::(); + // assert_try_unwrap_shared(String::from("test")); + assert_try_unwrap_shared(vec); + } + + #[kani::proof] + pub fn harness_try_unwrap_string_weak_present_global() { + let vec = verifier_nondet_vec::(); + // assert_try_unwrap_weak_present(String::from("test")); + assert_try_unwrap_weak_present(vec); + } + + #[kani::proof] + pub fn harness_try_unwrap_drop_sentinel_unique_global() { + assert_try_unwrap_unique(DropSentinel(kani::any::())); + } + + #[kani::proof] + pub fn harness_try_unwrap_drop_sentinel_shared_global() { + assert_try_unwrap_shared(DropSentinel(kani::any::())); + } + + #[kani::proof] + pub fn harness_try_unwrap_drop_sentinel_weak_present_global() { + assert_try_unwrap_weak_present(DropSentinel(kani::any::())); + } + + #[kani::proof] + pub fn harness_try_unwrap_array_u8_3_unique_global() { + assert_try_unwrap_unique(kani::any::<[u8; 3]>()); + } + + #[kani::proof] + pub fn harness_try_unwrap_array_u8_3_shared_global() { + assert_try_unwrap_shared(kani::any::<[u8; 3]>()); + } + + #[kani::proof] + pub fn harness_try_unwrap_array_u8_3_weak_present_global() { + assert_try_unwrap_weak_present(kani::any::<[u8; 3]>()); + } + + #[kani::proof] + pub fn harness_try_unwrap_bool_unique_global() { + assert_try_unwrap_unique(kani::any::()); + } + + #[kani::proof] + pub fn harness_try_unwrap_bool_shared_global() { + assert_try_unwrap_shared(kani::any::()); + } + + #[kani::proof] + pub fn harness_try_unwrap_bool_weak_present_global() { + assert_try_unwrap_weak_present(kani::any::()); + } + + #[kani::proof] + pub fn harness_try_unwrap_nested_rc_i32_shared_global() { + let value = Rc::::new_in(kani::any::(), Global); + assert_try_unwrap_shared(value); + } + + #[kani::proof] + pub fn harness_try_unwrap_tuple_i32_string_unique_global() { + let value = (kani::any::(), String::from("test")); + assert_try_unwrap_unique(value); + } + + #[kani::proof] + pub fn harness_try_unwrap_tuple_i32_string_shared_global() { + let value = (kani::any::(), String::from("test")); + assert_try_unwrap_shared(value); + } + + #[kani::proof] + pub fn harness_try_unwrap_tuple_i32_string_weak_present_global() { + let value = (kani::any::(), String::from("test")); + assert_try_unwrap_weak_present(value); + } + + #[kani::proof] + pub fn harness_try_unwrap_option_i32_unique_global() { + assert_try_unwrap_unique(kani::any::>()); + } + + #[kani::proof] + pub fn harness_try_unwrap_option_i32_shared_global() { + assert_try_unwrap_shared(kani::any::>()); + } + + #[kani::proof] + pub fn harness_try_unwrap_option_i32_weak_present_global() { + assert_try_unwrap_weak_present(kani::any::>()); + } +} + +#[cfg(kani)] +mod verify_1180 { + use super::*; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + fn any_bounded_len() -> usize { + kani::any::() as usize + } + + #[kani::proof] + pub fn harness_new_zeroed_slice_in_u8_single_path_global() { + let len = any_bounded_len(); + let _ = Rc::<[u8], Global>::new_zeroed_slice_in(len, Global); + } + + #[kani::proof] + pub fn harness_new_zeroed_slice_in_i32_single_path_global() { + let len = any_bounded_len(); + let _ = Rc::<[i32], Global>::new_zeroed_slice_in(len, Global); + } + + #[kani::proof] + pub fn harness_new_zeroed_slice_in_u64_single_path_global() { + let len = any_bounded_len(); + let _ = Rc::<[u64], Global>::new_zeroed_slice_in(len, Global); + } + + #[kani::proof] + pub fn harness_new_zeroed_slice_in_string_single_path_global() { + let len = any_bounded_len(); + let _ = Rc::<[String], Global>::new_zeroed_slice_in(len, Global); + } + + #[kani::proof] + pub fn harness_new_zeroed_slice_in_drop_sentinel_single_path_global() { + let len = any_bounded_len(); + let _ = Rc::<[DropSentinel], Global>::new_zeroed_slice_in(len, Global); + } + + #[kani::proof] + pub fn harness_new_zeroed_slice_in_array_u8_3_single_path_global() { + let len = any_bounded_len(); + let _ = Rc::<[[u8; 3]], Global>::new_zeroed_slice_in(len, Global); + } + + #[kani::proof] + pub fn harness_new_zeroed_slice_in_bool_single_path_global() { + let len = any_bounded_len(); + let _ = Rc::<[bool], Global>::new_zeroed_slice_in(len, Global); + } + + #[kani::proof] + pub fn harness_new_zeroed_slice_in_nested_rc_i32_single_path_global() { + let len = any_bounded_len(); + let _ = Rc::<[Rc], Global>::new_zeroed_slice_in(len, Global); + } + + #[kani::proof] + pub fn harness_new_zeroed_slice_in_tuple_i32_string_single_path_global() { + let len = any_bounded_len(); + let _ = Rc::<[(i32, String)], Global>::new_zeroed_slice_in(len, Global); + } + + #[kani::proof] + pub fn harness_new_zeroed_slice_in_option_i32_single_path_global() { + let len = any_bounded_len(); + let _ = Rc::<[Option], Global>::new_zeroed_slice_in(len, Global); + } + + #[kani::proof] + pub fn harness_new_zeroed_slice_in_cell_i32_single_path_global() { + let len = any_bounded_len(); + let _ = Rc::<[core::cell::Cell], Global>::new_zeroed_slice_in(len, Global); + } +} + +#[cfg(kani)] +mod verify_1594 { + use super::kani_rc_harness_helpers::*; + use super::*; + use core::any::Any; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + #[kani::proof] + pub fn harness_rc_as_ptr_u8_single_path_global() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + let _ = Rc::::as_ptr(&rc); + } + + #[kani::proof] + pub fn harness_rc_as_ptr_i32_single_path_global() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + let _ = Rc::::as_ptr(&rc); + } + + #[kani::proof] + pub fn harness_rc_as_ptr_u64_single_path_global() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + let _ = Rc::::as_ptr(&rc); + } + + #[kani::proof] + pub fn harness_rc_as_ptr_unit_single_path_global() { + let rc: Rc<(), Global> = Rc::new_in((), Global); + let _ = Rc::<(), Global>::as_ptr(&rc); + } + + #[kani::proof] + pub fn harness_rc_as_ptr_drop_sentinel_single_path_global() { + let rc: Rc = Rc::new_in(DropSentinel(kani::any::()), Global); + let _ = Rc::::as_ptr(&rc); + } + + #[kani::proof] + pub fn harness_rc_as_ptr_array_u8_3_single_path_global() { + let rc: Rc<[u8; 3], Global> = Rc::new_in(kani::any::<[u8; 3]>(), Global); + let _ = Rc::<[u8; 3], Global>::as_ptr(&rc); + } + + #[kani::proof] + pub fn harness_rc_as_ptr_slice_u8_single_path_global() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice::(&vec); + + let rc: Rc<[u8], Global> = Rc::from(slice); + let _ = Rc::<[u8], Global>::as_ptr(&rc); + } + + #[kani::proof] + pub fn harness_rc_as_ptr_str_single_path_global() { + let rc: Rc = Rc::from("seed"); + let _ = Rc::::as_ptr(&rc); + } + + #[kani::proof] + pub fn harness_rc_as_ptr_dyn_any_i32_single_path_global() { + let rc_i32: Rc = Rc::new_in(kani::any::(), Global); + let rc: Rc = rc_i32; + let _ = Rc::::as_ptr(&rc); + } + + #[kani::proof] + pub fn harness_rc_as_ptr_bool_single_path_global() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + let _ = Rc::::as_ptr(&rc); + } + + #[kani::proof] + pub fn harness_rc_as_ptr_array_u8_0_single_path_global() { + let rc: Rc<[u8; 0], Global> = Rc::new_in(kani::any::<[u8; 0]>(), Global); + let _ = Rc::<[u8; 0], Global>::as_ptr(&rc); + } + + #[kani::proof] + pub fn harness_rc_as_ptr_option_i32_single_path_global() { + let rc: Rc, Global> = Rc::new_in(kani::any::>(), Global); + let _ = Rc::, Global>::as_ptr(&rc); + } + + #[kani::proof] + pub fn harness_rc_as_ptr_slice_global() { + let v = verifier_nondet_vec::(); + let slice = nondet_rc_slice::(&v); + let _ = Rc::<[u8], Global>::as_ptr(&Rc::from(slice)); + } +} + +#[cfg(kani)] +mod verify_2467 { + use super::*; + + fn nondet_vec_copy() -> crate::vec::Vec { + let mut v: crate::vec::Vec = crate::vec::Vec::new(); + if kani::any() { + v.push(kani::any::()); + } + if kani::any() { + v.push(kani::any::()); + } + if kani::any() { + v.push(kani::any::()); + } + v + } + + #[kani::proof] + pub fn harness_from_slice_copy_u8_single_path() { + let v = nondet_vec_copy::(); + let _ = as RcFromSlice>::from_slice(v.as_slice()); + } + + #[kani::proof] + pub fn harness_from_slice_copy_i32_single_path() { + let v = nondet_vec_copy::(); + let _ = as RcFromSlice>::from_slice(v.as_slice()); + } + + #[kani::proof] + pub fn harness_from_slice_copy_u64_single_path() { + let v = nondet_vec_copy::(); + let _ = as RcFromSlice>::from_slice(v.as_slice()); + } + + #[kani::proof] + pub fn harness_from_slice_copy_unit_single_path() { + let v = nondet_vec_copy::<()>(); + let _ = as RcFromSlice<()>>::from_slice(v.as_slice()); + } + + #[kani::proof] + pub fn harness_from_slice_copy_array_u8_3_single_path() { + let v = nondet_vec_copy::<[u8; 3]>(); + let _ = as RcFromSlice<[u8; 3]>>::from_slice(v.as_slice()); + } + + #[kani::proof] + pub fn harness_from_slice_copy_bool_single_path() { + let v = nondet_vec_copy::(); + let _ = as RcFromSlice>::from_slice(v.as_slice()); + } + + #[kani::proof] + pub fn harness_from_slice_copy_option_i32_single_path() { + let v = nondet_vec_copy::>(); + let _ = ]> as RcFromSlice>>::from_slice(v.as_slice()); + } +} + +#[cfg(kani)] +mod verify_2530 { + use crate::vec; + + use super::kani_rc_harness_helpers::*; + use super::*; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + fn exercise_drop_unique(rc: Rc) { + let _ = rc; + } + + fn exercise_drop_shared(rc: Rc) { + let rc_clone = Rc::clone(&rc); + drop(rc); + let _ = rc_clone; + } + + fn exercise_drop_weak_present(rc: Rc) { + let weak = Rc::downgrade(&rc); + drop(rc); + let _ = weak; + } + + #[kani::proof] + pub fn harness_drop_rc_u8_unique() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_drop_unique(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_u8_shared() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_drop_shared(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_u8_weak_present() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_drop_weak_present(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_i32_unique() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_drop_unique(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_i32_shared() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_drop_shared(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_i32_weak_present() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_drop_weak_present(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_u64_unique() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_drop_unique(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_u64_shared() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_drop_shared(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_u64_weak_present() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_drop_weak_present(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_unit_unique() { + let rc: Rc<(), Global> = Rc::new_in((), Global); + exercise_drop_unique(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_unit_shared() { + let rc: Rc<(), Global> = Rc::new_in((), Global); + exercise_drop_shared(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_unit_weak_present() { + let rc: Rc<(), Global> = Rc::new_in((), Global); + exercise_drop_weak_present(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_drop_sentinel_unique() { + let rc: Rc = Rc::new_in(DropSentinel(kani::any::()), Global); + exercise_drop_unique(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_drop_sentinel_shared() { + let rc: Rc = Rc::new_in(DropSentinel(kani::any::()), Global); + exercise_drop_shared(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_drop_sentinel_weak_present() { + let rc: Rc = Rc::new_in(DropSentinel(kani::any::()), Global); + exercise_drop_weak_present(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_array_u8_3_unique() { + let rc: Rc<[u8; 3], Global> = Rc::new_in(kani::any::<[u8; 3]>(), Global); + exercise_drop_unique(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_array_u8_3_shared() { + let rc: Rc<[u8; 3], Global> = Rc::new_in(kani::any::<[u8; 3]>(), Global); + exercise_drop_shared(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_array_u8_3_weak_present() { + let rc: Rc<[u8; 3], Global> = Rc::new_in(kani::any::<[u8; 3]>(), Global); + exercise_drop_weak_present(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_unsized_slice_u8_unique() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice::(&vec); + let rc: Rc<[u8], Global> = Rc::from(slice); + exercise_drop_unique(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_unsized_slice_u8_shared() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice::(&vec); + let rc: Rc<[u8], Global> = Rc::from(slice); + exercise_drop_shared(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_unsized_slice_u8_weak_present() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice::(&vec); + let rc: Rc<[u8], Global> = Rc::from(slice); + exercise_drop_weak_present(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_unsized_slice_u16_unique() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice::(&vec); + let rc: Rc<[u16], Global> = Rc::from(slice); + exercise_drop_unique(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_unsized_slice_u16_shared() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice::(&vec); + let rc: Rc<[u16], Global> = Rc::from(slice); + exercise_drop_shared(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_unsized_slice_u16_weak_present() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice::(&vec); + let rc: Rc<[u16], Global> = Rc::from(slice); + exercise_drop_weak_present(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_unsized_slice_u32_unique() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice::(&vec); + let rc: Rc<[u32], Global> = Rc::from(slice); + exercise_drop_unique(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_unsized_slice_u32_shared() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice::(&vec); + let rc: Rc<[u32], Global> = Rc::from(slice); + exercise_drop_shared(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_unsized_slice_u32_weak_present() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice::(&vec); + let rc: Rc<[u32], Global> = Rc::from(slice); + exercise_drop_weak_present(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_str_unique() { + let rc: Rc = Rc::from("seed"); + exercise_drop_unique(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_str_shared() { + let rc: Rc = Rc::from("seed"); + exercise_drop_shared(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_str_weak_present() { + let rc: Rc = Rc::from("seed"); + exercise_drop_weak_present(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_dyn_any_i32_unique() { + let rc_i32: Rc = Rc::new_in(kani::any::(), Global); + let rc: Rc = rc_i32; + exercise_drop_unique(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_dyn_any_i32_shared() { + let rc_i32: Rc = Rc::new_in(kani::any::(), Global); + let rc: Rc = rc_i32; + exercise_drop_shared(rc); + } + + #[kani::proof] + pub fn harness_drop_rc_dyn_any_i32_weak_present() { + let rc_i32: Rc = Rc::new_in(kani::any::(), Global); + let rc: Rc = rc_i32; + exercise_drop_weak_present(rc); + } +} + +#[cfg(kani)] +mod verify_2557 { + use super::kani_rc_harness_helpers::*; + use super::*; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + fn exercise_clone_unique(rc: Rc) { + let _ = Rc::clone(&rc); + } + + fn exercise_clone_shared(rc: Rc) { + let _preexisting = Rc::clone(&rc); + let _ = Rc::clone(&rc); + } + + fn exercise_clone_weak_present(rc: Rc) { + let weak = Rc::downgrade(&rc); + let _ = Rc::clone(&rc); + let _ = weak; + } + + #[kani::proof] + pub fn harness_clone_rc_u8_unique() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_clone_unique(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_u8_shared() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_clone_shared(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_u8_weak_present() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_clone_weak_present(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_i32_unique() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_clone_unique(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_i32_shared() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_clone_shared(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_i32_weak_present() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_clone_weak_present(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_u64_unique() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_clone_unique(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_u64_shared() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_clone_shared(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_u64_weak_present() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_clone_weak_present(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_unit_unique() { + let rc: Rc<(), Global> = Rc::new_in((), Global); + exercise_clone_unique(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_unit_shared() { + let rc: Rc<(), Global> = Rc::new_in((), Global); + exercise_clone_shared(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_unit_weak_present() { + let rc: Rc<(), Global> = Rc::new_in((), Global); + exercise_clone_weak_present(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_drop_sentinel_unique() { + let rc: Rc = Rc::new_in(DropSentinel(kani::any::()), Global); + exercise_clone_unique(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_drop_sentinel_shared() { + let rc: Rc = Rc::new_in(DropSentinel(kani::any::()), Global); + exercise_clone_shared(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_drop_sentinel_weak_present() { + let rc: Rc = Rc::new_in(DropSentinel(kani::any::()), Global); + exercise_clone_weak_present(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_array_u8_3_unique() { + let rc: Rc<[u8; 3], Global> = Rc::new_in(kani::any::<[u8; 3]>(), Global); + exercise_clone_unique(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_array_u8_3_shared() { + let rc: Rc<[u8; 3], Global> = Rc::new_in(kani::any::<[u8; 3]>(), Global); + exercise_clone_shared(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_array_u8_3_weak_present() { + let rc: Rc<[u8; 3], Global> = Rc::new_in(kani::any::<[u8; 3]>(), Global); + exercise_clone_weak_present(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_unsized_slice_u8_unique() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice::(&vec); + let rc: Rc<[u8], Global> = Rc::from(slice); + exercise_clone_unique(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_unsized_slice_u8_shared() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice::(&vec); + let rc: Rc<[u8], Global> = Rc::from(slice); + exercise_clone_shared(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_unsized_slice_u8_weak_present() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice::(&vec); + let rc: Rc<[u8], Global> = Rc::from(slice); + exercise_clone_weak_present(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_unsized_slice_u16_unique() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice::(&vec); + let rc: Rc<[u16], Global> = Rc::from(slice); + exercise_clone_unique(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_unsized_slice_u16_shared() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice::(&vec); + let rc: Rc<[u16], Global> = Rc::from(slice); + exercise_clone_shared(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_unsized_slice_u16_weak_present() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice::(&vec); + let rc: Rc<[u16], Global> = Rc::from(slice); + exercise_clone_weak_present(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_unsized_slice_u32_unique() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice::(&vec); + let rc: Rc<[u32], Global> = Rc::from(slice); + exercise_clone_unique(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_unsized_slice_u32_shared() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice::(&vec); + let rc: Rc<[u32], Global> = Rc::from(slice); + exercise_clone_shared(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_unsized_slice_u32_weak_present() { + let vec = verifier_nondet_vec::(); + let slice = nondet_rc_slice::(&vec); + let rc: Rc<[u32], Global> = Rc::from(slice); + exercise_clone_weak_present(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_str_unique() { + let rc: Rc = Rc::from("seed"); + exercise_clone_unique(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_str_shared() { + let rc: Rc = Rc::from("seed"); + exercise_clone_shared(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_str_weak_present() { + let rc: Rc = Rc::from("seed"); + exercise_clone_weak_present(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_dyn_any_i32_unique() { + let rc_i32: Rc = Rc::new_in(kani::any::(), Global); + let rc: Rc = rc_i32; + exercise_clone_unique(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_dyn_any_i32_shared() { + let rc_i32: Rc = Rc::new_in(kani::any::(), Global); + let rc: Rc = rc_i32; + exercise_clone_shared(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_dyn_any_i32_weak_present() { + let rc_i32: Rc = Rc::new_in(kani::any::(), Global); + let rc: Rc = rc_i32; + exercise_clone_weak_present(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_bool_unique() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_clone_unique(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_bool_shared() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_clone_shared(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_bool_weak_present() { + let rc: Rc = Rc::new_in(kani::any::(), Global); + exercise_clone_weak_present(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_tuple_i32_string_unique() { + let rc: Rc<(i32, String), Global> = Rc::new_in((kani::any::(), String::new()), Global); + exercise_clone_unique(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_tuple_i32_string_shared() { + let rc: Rc<(i32, String), Global> = Rc::new_in((kani::any::(), String::new()), Global); + exercise_clone_shared(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_tuple_i32_string_weak_present() { + let rc: Rc<(i32, String), Global> = Rc::new_in((kani::any::(), String::new()), Global); + exercise_clone_weak_present(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_option_i32_unique() { + let rc: Rc, Global> = Rc::new_in(kani::any::>(), Global); + exercise_clone_unique(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_option_i32_shared() { + let rc: Rc, Global> = Rc::new_in(kani::any::>(), Global); + exercise_clone_shared(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_option_i32_weak_present() { + let rc: Rc, Global> = Rc::new_in(kani::any::>(), Global); + exercise_clone_weak_present(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_cell_i32_unique() { + let rc: Rc, Global> = + Rc::new_in(core::cell::Cell::new(kani::any::()), Global); + exercise_clone_unique(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_cell_i32_shared() { + let rc: Rc, Global> = + Rc::new_in(core::cell::Cell::new(kani::any::()), Global); + exercise_clone_shared(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_cell_i32_weak_present() { + let rc: Rc, Global> = + Rc::new_in(core::cell::Cell::new(kani::any::()), Global); + exercise_clone_weak_present(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_dyn_debug_i32_unique() { + let rc_i32: Rc = Rc::new_in(kani::any::(), Global); + let rc: Rc = rc_i32; + exercise_clone_unique(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_dyn_debug_i32_shared() { + let rc_i32: Rc = Rc::new_in(kani::any::(), Global); + let rc: Rc = rc_i32; + exercise_clone_shared(rc); + } + + #[kani::proof] + pub fn harness_clone_rc_dyn_debug_i32_weak_present() { + let rc_i32: Rc = Rc::new_in(kani::any::(), Global); + let rc: Rc = rc_i32; + exercise_clone_weak_present(rc); + } +} + +#[cfg(kani)] +mod verify_2582 { + use super::*; + + struct DropSentinel(u8); + + impl Default for DropSentinel { + fn default() -> Self { + Self(0) + } + } + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + #[kani::proof] + pub fn harness_rc_default_u8() { + let _ = Rc::::default(); + } + + #[kani::proof] + pub fn harness_rc_default_i32() { + let _ = Rc::::default(); + } + + #[kani::proof] + pub fn harness_rc_default_u64() { + let _ = Rc::::default(); + } + + #[kani::proof] + pub fn harness_rc_default_unit() { + let _ = Rc::<()>::default(); + } + + #[kani::proof] + pub fn harness_rc_default_string() { + let _ = Rc::::default(); + } + + #[kani::proof] + pub fn harness_rc_default_drop_sentinel() { + let _ = Rc::::default(); + } + + #[kani::proof] + pub fn harness_rc_default_array_u8_3() { + let _ = Rc::<[u8; 3]>::default(); + } + + #[kani::proof] + pub fn harness_rc_default_bool() { + let _ = Rc::::default(); + } + + #[kani::proof] + pub fn harness_rc_default_tuple_i32_string() { + let _ = Rc::<(i32, String)>::default(); + } + + #[kani::proof] + pub fn harness_rc_default_option_i32() { + let _ = Rc::>::default(); + } +} + +#[cfg(kani)] +mod verify_2606 { + use super::*; + + #[kani::proof] + pub fn harness_rc_default_str() { + let _ = Rc::::default(); + } +} + +#[cfg(kani)] +mod verify_2973 { + use super::*; + + #[kani::proof] + pub fn harness_from_ref_str_rc_str() { + let _ = Rc::::from("seed"); + } +} + +#[cfg(kani)] +mod verify_3051 { + use super::*; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + fn exercise_from_vec_single_path(v: Vec) { + let _ = Rc::<[T], Global>::from(v); + } + + #[kani::proof] + pub fn harness_from_vec_i32_len0_single_path_global() { + let v: Vec = vec![]; + exercise_from_vec_single_path(v); + } + + #[kani::proof] + pub fn harness_from_vec_i32_len1_single_path_global() { + let v: Vec = vec![kani::any::()]; + exercise_from_vec_single_path(v); + } + + #[kani::proof] + pub fn harness_from_vec_i32_len3_single_path_global() { + let v: Vec = vec![kani::any::(), kani::any::(), kani::any::()]; + exercise_from_vec_single_path(v); + } + + #[kani::proof] + pub fn harness_from_vec_unit_len0_single_path_global() { + let v: Vec<(), Global> = vec![]; + exercise_from_vec_single_path(v); + } + + #[kani::proof] + pub fn harness_from_vec_unit_len1_single_path_global() { + let v: Vec<(), Global> = vec![()]; + exercise_from_vec_single_path(v); + } + + #[kani::proof] + pub fn harness_from_vec_unit_len3_single_path_global() { + let v: Vec<(), Global> = vec![(), (), ()]; + exercise_from_vec_single_path(v); + } + + #[kani::proof] + pub fn harness_from_vec_string_len0_single_path_global() { + let v: Vec = vec![]; + exercise_from_vec_single_path(v); + } + + #[kani::proof] + pub fn harness_from_vec_string_len1_single_path_global() { + let v: Vec = vec![String::new()]; + exercise_from_vec_single_path(v); + } + + #[kani::proof] + pub fn harness_from_vec_string_len3_single_path_global() { + let v: Vec = vec![String::new(), String::new(), String::new()]; + exercise_from_vec_single_path(v); + } + + #[kani::proof] + pub fn harness_from_vec_arr3_len0_single_path_global() { + let v: Vec<[u8; 3], Global> = vec![]; + exercise_from_vec_single_path(v); + } + + #[kani::proof] + pub fn harness_from_vec_arr3_len1_single_path_global() { + let v: Vec<[u8; 3], Global> = vec![kani::any::<[u8; 3]>()]; + exercise_from_vec_single_path(v); + } + + #[kani::proof] + pub fn harness_from_vec_arr3_len3_single_path_global() { + let v: Vec<[u8; 3], Global> = vec![ + kani::any::<[u8; 3]>(), + kani::any::<[u8; 3]>(), + kani::any::<[u8; 3]>(), + ]; + exercise_from_vec_single_path(v); + } + + #[kani::proof] + pub fn harness_from_vec_u8_len0_single_path_global() { + let v: Vec = vec![]; + exercise_from_vec_single_path(v); + } + + #[kani::proof] + pub fn harness_from_vec_u8_len1_single_path_global() { + let v: Vec = vec![kani::any::()]; + exercise_from_vec_single_path(v); + } + + #[kani::proof] + pub fn harness_from_vec_u8_len3_single_path_global() { + let v: Vec = vec![kani::any::(), kani::any::(), kani::any::()]; + exercise_from_vec_single_path(v); + } + + #[kani::proof] + pub fn harness_from_vec_drop_sentinel_len0_single_path_global() { + let v: Vec = vec![]; + exercise_from_vec_single_path(v); + } + + #[kani::proof] + pub fn harness_from_vec_drop_sentinel_len1_single_path_global() { + let v: Vec = vec![DropSentinel(kani::any())]; + exercise_from_vec_single_path(v); + } + + #[kani::proof] + pub fn harness_from_vec_drop_sentinel_len3_single_path_global() { + let v: Vec = vec![ + DropSentinel(kani::any()), + DropSentinel(kani::any()), + DropSentinel(kani::any()), + ]; + exercise_from_vec_single_path(v); + } + + #[kani::proof] + pub fn harness_from_vec_nested_rc_i32_len0_single_path_global() { + let v: Vec, Global> = vec![]; + exercise_from_vec_single_path(v); + } + + #[kani::proof] + pub fn harness_from_vec_nested_rc_i32_len1_single_path_global() { + let v: Vec, Global> = vec![Rc::new(kani::any::())]; + exercise_from_vec_single_path(v); + } + + #[kani::proof] + pub fn harness_from_vec_nested_rc_i32_len3_single_path_global() { + let v: Vec, Global> = vec![ + Rc::new(kani::any::()), + Rc::new(kani::any::()), + Rc::new(kani::any::()), + ]; + exercise_from_vec_single_path(v); + } +} + +#[cfg(kani)] +mod verify_3181 { + use super::*; + + struct DropSentinel(u8); + + impl Drop for DropSentinel { + fn drop(&mut self) {} + } + + struct NonTrustedIter(I); + + impl Iterator for NonTrustedIter { + type Item = I::Item; + + fn next(&mut self) -> Option { + self.0.next() + } + + fn size_hint(&self) -> (usize, Option) { + self.0.size_hint() + } + } + + fn exercise_to_rc_slice_non_trusted(iter: I) + where + I: Iterator, + { + let non_trusted = NonTrustedIter(iter); + let _rc: Rc<[T]> = as ToRcSlice>::to_rc_slice(non_trusted); + } + + #[kani::proof] + pub fn harness_to_rc_slice_u8_non_trusted_len() { + exercise_to_rc_slice_non_trusted( + [kani::any::(), kani::any::(), kani::any::()].into_iter(), + ); + } + + #[kani::proof] + pub fn harness_to_rc_slice_i32_non_trusted_len() { + exercise_to_rc_slice_non_trusted( + [kani::any::(), kani::any::(), kani::any::()].into_iter(), + ); + } + + #[kani::proof] + pub fn harness_to_rc_slice_u64_non_trusted_len() { + exercise_to_rc_slice_non_trusted( + [kani::any::(), kani::any::(), kani::any::()].into_iter(), + ); + } + + #[kani::proof] + pub fn harness_to_rc_slice_unit_non_trusted_len() { + exercise_to_rc_slice_non_trusted([(), (), ()].into_iter()); + } + + #[kani::proof] + pub fn harness_to_rc_slice_string_non_trusted_len() { + let items: [String; 0] = []; + exercise_to_rc_slice_non_trusted(items.into_iter()); + } + + #[kani::proof] + pub fn harness_to_rc_slice_drop_sentinel_non_trusted_len() { + exercise_to_rc_slice_non_trusted( + [ + DropSentinel(kani::any()), + DropSentinel(kani::any()), + DropSentinel(kani::any()), + ] + .into_iter(), + ); + } + + #[kani::proof] + pub fn harness_to_rc_slice_arr3_non_trusted_len() { + exercise_to_rc_slice_non_trusted( + [ + kani::any::<[u8; 3]>(), + kani::any::<[u8; 3]>(), + kani::any::<[u8; 3]>(), + ] + .into_iter(), + ); + } + + #[kani::proof] + pub fn harness_to_rc_slice_bool_non_trusted_len() { + exercise_to_rc_slice_non_trusted( + [ + kani::any::(), + kani::any::(), + kani::any::(), + ] + .into_iter(), + ); + } + + #[kani::proof] + pub fn harness_to_rc_slice_nested_rc_i32_non_trusted_len() { + exercise_to_rc_slice_non_trusted( + [ + Rc::new(kani::any::()), + Rc::new(kani::any::()), + Rc::new(kani::any::()), + ] + .into_iter(), + ); + } + + #[kani::proof] + pub fn harness_to_rc_slice_tuple_i32_string_non_trusted_len() { + exercise_to_rc_slice_non_trusted( + [ + (kani::any::(), String::from("seed")), + (kani::any::(), String::from("seed")), + (kani::any::(), String::from("seed")), + ] + .into_iter(), + ); + } + + #[kani::proof] + pub fn harness_to_rc_slice_option_i32_non_trusted_len() { + exercise_to_rc_slice_non_trusted( + [ + kani::any::>(), + kani::any::>(), + kani::any::>(), + ] + .into_iter(), + ); + } +} + +#[cfg(kani)] +mod verify_3107 { + use super::*; + + #[kani::proof] + pub fn harness_from_rc_str_to_rc_u8_slice_single_path_empty() { + let rc: Rc = Rc::from(""); + let _ = >::from(rc); + } + + #[kani::proof] + pub fn harness_from_rc_str_to_rc_u8_slice_single_path_nonempty() { + let rc: Rc = Rc::from("seed"); + let _ = >::from(rc); + } +}