vstd/std_specs/
maybe_uninit.rs

1use super::super::prelude::*;
2use super::super::raw_ptr::MemContents;
3use core::mem::MaybeUninit;
4
5use verus as verus_;
6verus_! {
7
8#[verifier::external_type_specification]
9#[verifier::external_body]
10#[verifier::accept_recursive_types(T)]
11pub struct ExMaybeUninit<T>(MaybeUninit<T>);
12
13pub trait MaybeUninitAdditionalSpecFns<T> {
14    spec fn mem_contents(self) -> MemContents<T>;
15    spec fn as_option(self) -> Option<T>;
16}
17
18impl<T> MaybeUninitAdditionalSpecFns<T> for MaybeUninit<T> {
19    uninterp spec fn mem_contents(self) -> MemContents<T>;
20
21    open spec fn as_option(self) -> Option<T> {
22        match self.mem_contents() {
23            MemContents::Init(v) => Some(v),
24            MemContents::Uninit => None,
25        }
26    }
27}
28
29pub assume_specification<T>[ MaybeUninit::<T>::new ](val: T) -> (res: MaybeUninit<T>)
30    ensures res.mem_contents() == MemContents::Init(val),
31    opens_invariants none
32    no_unwind;
33
34pub assume_specification<T>[ MaybeUninit::<T>::uninit ]() -> (res: MaybeUninit<T>)
35    ensures res.mem_contents() === MemContents::Uninit,
36    opens_invariants none
37    no_unwind;
38
39pub assume_specification<T>[ MaybeUninit::<T>::assume_init ](m: MaybeUninit<T>) -> T
40    requires m.mem_contents().is_init(),
41    returns m.mem_contents().value(),
42    opens_invariants none
43    no_unwind;
44
45pub assume_specification<T>[ MaybeUninit::<T>::assume_init_ref ](m: &MaybeUninit<T>) -> (ret: &T)
46    requires m.mem_contents().is_init(),
47    ensures ret == m.mem_contents().value(),
48    opens_invariants none
49    no_unwind;
50
51}
vstd/std_specs/maybe_uninit.rs

vstd/std_specs/
maybe_uninit.rs
