vstd/std_specs/
alloc.rs

1use super::super::prelude::*;
2use super::super::raw_ptr::MemContents;
3
4verus! {
5
6// this is a bit of a hack; verus treats Global specially already,
7// but putting this here helps Verus pick up all the trait impls for Global
8#[cfg(feature = "alloc")]
9#[verifier::external_type_specification]
10#[verifier::external_body]
11pub struct ExGlobal(alloc::alloc::Global);
12
13#[cfg(feature = "alloc")]
14#[feature(liballoc_internals)]
15pub assume_specification<T, const N: usize>[ alloc::boxed::box_assume_init_into_vec_unsafe ](
16    vals: alloc::boxed::Box<core::mem::MaybeUninit<[T; N]>>,
17) -> (result: alloc::vec::Vec<T>)
18    requires
19        vals.mem_contents() is Init,
20    ensures
21        vals.mem_contents() matches MemContents::Init(array) && result@ == array@,
22;
23
24#[cfg(feature = "alloc")]
25#[feature(liballoc_internals)]
26pub assume_specification<T>[ alloc::intrinsics::write_box_via_move ](
27    _0: alloc::boxed::Box<core::mem::MaybeUninit<T>>,
28    v: T,
29) -> (result: alloc::boxed::Box<core::mem::MaybeUninit<T>>)
30    ensures
31        result.mem_contents() == MemContents::Init(v),
32;
33
34#[cfg(feature = "alloc")]
35#[feature(liballoc_internals)]
36pub assume_specification<T>[ alloc::boxed::Box::<T>::new_uninit ]() -> alloc::boxed::Box<
37    core::mem::MaybeUninit<T>,
38>
39;
40
41} // verus!
vstd/std_specs/alloc.rs

vstd/std_specs/
alloc.rs
