vstd_extra/external/
ptr.rs

1use core::marker::PointeeSized;
2use vstd::prelude::*;
3
4verus! {
5
6pub assume_specification<T: PointeeSized>[ <*const T>::map_addr ](
7    ptr: *const T,
8    f: impl FnOnce(usize) -> usize,
9) -> (ret: *const T)
10    requires
11        f.requires((ptr@.addr,)),
12    ensures
13        ret@.metadata == ptr@.metadata,
14        ret@.provenance == ptr@.provenance,
15        f.ensures((ptr@.addr,), ret@.addr),
16;
17
18pub assume_specification<T: PointeeSized>[ <*mut T>::map_addr ](
19    ptr: *mut T,
20    f: impl FnOnce(usize) -> usize,
21) -> (ret: *mut T)
22    requires
23        f.requires((ptr@.addr,)),
24    ensures
25        ret@.metadata == ptr@.metadata,
26        ret@.provenance == ptr@.provenance,
27        f.ensures((ptr@.addr,), ret@.addr),
28;
29
30#[verifier::inline]
31pub open spec fn ptr_cast_spec<T: PointeeSized, U>(ptr: *const T) -> *const U {
32    ptr as *const U
33}
34
35#[verifier::inline]
36pub open spec fn ptr_mut_cast_spec<T: PointeeSized, U>(ptr: *mut T) -> *mut U {
37    ptr as *mut U
38}
39
40#[verifier::inline]
41pub open spec fn ptr_mut_cast_const_spec<T: PointeeSized>(ptr: *mut T) -> *const T {
42    ptr as *const T
43}
44
45#[verifier::inline]
46pub open spec fn ptr_cast_mut_spec<T: PointeeSized>(ptr: *const T) -> *mut T {
47    ptr as *mut T
48}
49
50#[verifier::inline]
51pub open spec fn ptr_is_null_spec<T: PointeeSized>(ptr: *const T) -> bool {
52    ptr.addr() == 0
53}
54
55#[verifier::inline]
56pub open spec fn ptr_mut_is_null_spec<T: PointeeSized>(ptr: *mut T) -> bool {
57    ptr.addr() == 0
58}
59
60#[verifier::when_used_as_spec(ptr_cast_spec)]
61pub assume_specification<T: PointeeSized, U>[ <*const T>::cast::<U> ](ptr: *const T) -> *const U
62    returns
63        ptr as *const U,
64    opens_invariants none
65    no_unwind
66;
67
68#[verifier::when_used_as_spec(ptr_mut_cast_spec)]
69pub assume_specification<T: PointeeSized, U>[ <*mut T>::cast::<U> ](ptr: *mut T) -> *mut U
70    returns
71        ptr as *mut U,
72    opens_invariants none
73    no_unwind
74;
75
76#[verifier::when_used_as_spec(ptr_mut_cast_const_spec)]
77pub assume_specification<T: PointeeSized>[ <*mut T>::cast_const ](ptr: *mut T) -> *const T
78    returns
79        ptr as *const T,
80    opens_invariants none
81    no_unwind
82;
83
84#[verifier::when_used_as_spec(ptr_cast_mut_spec)]
85pub assume_specification<T: PointeeSized>[ <*const T>::cast_mut ](ptr: *const T) -> *mut T
86    returns
87        ptr as *mut T,
88    opens_invariants none
89    no_unwind
90;
91
92/// [<*const T>::is_null](https://doc.rust-lang.org/std/primitive.pointer.html#method.is_null) only checks the raw data pointer.
93#[verifier::when_used_as_spec(ptr_is_null_spec)]
94pub assume_specification<T: PointeeSized>[ <*const T>::is_null ](ptr: *const T) -> bool
95    returns
96        ptr.addr() == 0,
97    opens_invariants none
98    no_unwind
99;
100
101/// [<*mut T>::is_null](https://doc.rust-lang.org/std/primitive.pointer.html#method.is_null) only checks the raw data pointer.
102#[verifier::when_used_as_spec(ptr_mut_is_null_spec)]
103pub assume_specification<T: PointeeSized>[ <*mut T>::is_null ](ptr: *mut T) -> bool
104    returns
105        ptr.addr() == 0,
106    opens_invariants none
107    no_unwind
108;
109
110} // verus!
vstd_extra/external/ptr.rs

vstd_extra/external/
ptr.rs
