vstd/std_specs/
manually_drop.rs

1#![allow(unused_imports)]
2
3use super::super::prelude::*;
4use core::mem::ManuallyDrop;
5use core::ops::Deref;
6
7verus! {
8
9#[verifier::external_type_specification]
10#[verifier::external_body]
11#[verifier::reject_recursive_types_in_ground_variants(V)]
12pub struct ExManuallyDrop<V: ?Sized>(ManuallyDrop<V>);
13
14pub trait ManuallyDropAdditionalFns<T: ?Sized> {
15    spec fn view_ref(&self) -> &T;
16}
17
18impl<T: ?Sized> ManuallyDropAdditionalFns<T> for ManuallyDrop<T> {
19    uninterp spec fn view_ref(&self) -> &T;
20}
21
22impl<T> View for ManuallyDrop<T> {
23    type V = T;
24
25    open spec fn view(&self) -> Self::V {
26        *self.view_ref()
27    }
28}
29
30pub assume_specification<T>[ ManuallyDrop::<T>::new ](value: T) -> (res: ManuallyDrop<T>)
31    ensures
32        res@ === value,
33;
34
35pub assume_specification<T>[ ManuallyDrop::<T>::into_inner ](m: ManuallyDrop<T>) -> T
36    returns
37        m@,
38;
39
40pub assume_specification<T: Clone + ?Sized>[ <ManuallyDrop<T> as Clone>::clone ](
41    m: &ManuallyDrop<T>,
42) -> (res: ManuallyDrop<T>)
43    ensures
44        cloned(m@, res@),
45;
46
47pub assume_specification<T: ?Sized>[ <ManuallyDrop<T> as Deref>::deref ](
48    m: &ManuallyDrop<T>,
49) -> (res: &T)
50    returns
51        m.view_ref(),
52;
53
54} // verus!
vstd/std_specs/manually_drop.rs

vstd/std_specs/
manually_drop.rs
