Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142use super::super::prelude::*;use super::super::raw_ptr::MemContents;
verus! {
// this is a bit of a hack; verus treats Global specially already,// but putting this here helps Verus pick up all the trait impls for Global#[cfg(feature = "alloc")]#[verifier::external_type_specification]#[verifier::external_body]pub struct ExGlobal(alloc::alloc::Global);
#[cfg(feature = "alloc")]#[feature(liballoc_internals)]pub assume_specification<T, const N: usize>[ alloc::boxed::box_assume_init_into_vec_unsafe ]( vals: alloc::boxed::Box<core::mem::MaybeUninit<[T; N]>>,) -> (result: alloc::vec::Vec<T>) requires vals.mem_contents() is Init, ensures vals.mem_contents() matches MemContents::Init(array) && result@ == array@,;
#[cfg(feature = "alloc")]#[feature(liballoc_internals)]pub assume_specification<T>[ alloc::intrinsics::write_box_via_move ]( _0: alloc::boxed::Box<core::mem::MaybeUninit<T>>, v: T,) -> (result: alloc::boxed::Box<core::mem::MaybeUninit<T>>) ensures result.mem_contents() == MemContents::Init(v),;
#[cfg(feature = "alloc")]#[feature(liballoc_internals)]pub assume_specification<T>[ alloc::boxed::Box::<T>::new_uninit ]() -> alloc::boxed::Box< core::mem::MaybeUninit<T>,>;
} // verus!