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_skip_verusfmt;
6verus_skip_verusfmt! {
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
51pub assume_specification<T>[ MaybeUninit::<T>::assume_init_mut ](m: &mut MaybeUninit<T>) -> (ret: &mut T)
52    requires m.mem_contents().is_init(),
53    ensures *ret == old(m).mem_contents().value(),
54        final(m).mem_contents().is_init(),
55        final(m).mem_contents().value() == *final(ret),
56    opens_invariants none
57    no_unwind;
58
59pub assume_specification<T>[ MaybeUninit::<T>::write ](m: &mut MaybeUninit<T>, val: T) -> (ret: &mut T)
60    ensures *ret == val,
61        final(m).mem_contents().is_init(),
62        final(m).mem_contents().value() == *final(ret),
63    opens_invariants none
64    no_unwind;
65
66pub assume_specification<T, const N: usize>[ MaybeUninit::<T>::array_assume_init ](
67    array: [MaybeUninit<T>; N],
68) -> (ret: [T; N])
69    requires
70        forall|i: int| #![auto] 0 <= i < N ==> array@[i].mem_contents().is_init(),
71    ensures
72        forall|i: int| #![auto] 0 <= i < N ==> ret@[i] == array@[i].mem_contents().value(),
73    opens_invariants none
74    no_unwind;
75
76}
vstd/std_specs/maybe_uninit.rs

vstd/std_specs/
maybe_uninit.rs
