vstd_extra/external/
manually_drop.rs

1use core::mem::ManuallyDrop;
2use core::ops::Deref;
3use vstd::prelude::*;
4
5verus! {
6
7pub uninterp spec fn manually_drop_deref_spec<T: ?Sized>(v: &ManuallyDrop<T>) -> &T;
8
9pub uninterp spec fn manually_drop_new_spec<T>(v: T) -> ManuallyDrop<T>;
10
11pub open spec fn manually_drop_unwrap<T>(v: ManuallyDrop<T>) -> T {
12    *manually_drop_deref_spec(&v)
13}
14
15} // verus!