vstd/std_specs/
ptr.rs

1use super::super::prelude::*;
2use core::ptr::NonNull;
3
4use verus as verus_skip_verusfmt;
5verus_skip_verusfmt! {
6
7#[verifier::external_type_specification]
8#[verifier::external_body]
9#[verifier::accept_recursive_types(T)]
10pub struct ExNonNull<T: core::marker::PointeeSized>(NonNull<T>);
11
12pub uninterp spec fn spec_nonnull_as_ptr<T: core::marker::PointeeSized>(p: NonNull<T>) -> *mut T;
13
14/// The wrapped pointer "must always be non-null, even if the pointer is never dereferenced"
15/// ([Reference](https://doc.rust-lang.org/std/ptr/struct.NonNull.html)).
16pub broadcast axiom fn axiom_nonnull_addr_nonzero<T: core::marker::PointeeSized>(p: NonNull<T>)
17    ensures (#[trigger] spec_nonnull_as_ptr(p))@.addr != 0;
18
19#[verifier::when_used_as_spec(spec_nonnull_as_ptr)]
20pub assume_specification<T: core::marker::PointeeSized>[ NonNull::<T>::as_ptr ](p: NonNull<T>) -> (ret: *mut T)
21    ensures ret == spec_nonnull_as_ptr(p),
22    opens_invariants none
23    no_unwind;
24
25pub assume_specification<T: core::marker::PointeeSized>[ NonNull::<T>::new_unchecked ](ptr: *mut T) -> (ret: NonNull<T>)
26    requires ptr@.addr != 0,
27    ensures spec_nonnull_as_ptr(ret) == ptr,
28    opens_invariants none
29    no_unwind;
30
31pub assume_specification<T: core::marker::PointeeSized>[ NonNull::<T>::new ](ptr: *mut T) -> (ret: Option<NonNull<T>>)
32    ensures match ret {
33        Some(nn) => spec_nonnull_as_ptr(nn) == ptr && ptr@.addr != 0,
34        None => ptr@.addr == 0,
35    },
36    opens_invariants none
37    no_unwind;
38
39} // verus!
vstd/std_specs/ptr.rs

vstd/std_specs/
ptr.rs
