vstd/std_specs/
alloc.rs

1use super::super::prelude::*;
2
3verus! {
4
5// this is a bit of a hack; verus treats Global specially already,
6// but putting this here helps Verus pick up all the trait impls for Global
7#[cfg(feature = "alloc")]
8#[verifier::external_type_specification]
9#[verifier::external_body]
10pub struct ExGlobal(alloc::alloc::Global);
11
12#[cfg(feature = "alloc")]
13#[feature(liballoc_internals)]
14pub assume_specification<T>[ alloc::boxed::box_new ](x: T) -> (result: alloc::boxed::Box<T>)
15    ensures
16        *result == x,
17;
18
19} // verus!