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#[inline(always)]
31pub open spec fn ptr_cast_spec<T: PointeeSized, U>(ptr: *const T) -> *const U {
32    ptr as *const U
33}
34
35#[inline(always)]
36pub open spec fn ptr_mut_cast_spec<T: PointeeSized, U>(ptr: *mut T) -> *mut U {
37    ptr as *mut U
38}
39
40#[inline(always)]
41pub open spec fn ptr_mut_cast_const_spec<T: PointeeSized>(ptr: *mut T) -> *const T {
42    ptr as *const T
43}
44
45#[inline(always)]
46pub open spec fn ptr_cast_mut_spec<T: PointeeSized>(ptr: *const T) -> *mut T {
47    ptr as *mut T
48}
49
50#[verifier::when_used_as_spec(ptr_cast_spec)]
51pub assume_specification<T: PointeeSized, U>[ <*const T>::cast::<U> ](ptr: *const T) -> *const U
52    returns
53        ptr as *const U,
54    opens_invariants none
55    no_unwind
56;
57
58#[verifier::when_used_as_spec(ptr_mut_cast_spec)]
59pub assume_specification<T: PointeeSized, U>[ <*mut T>::cast::<U> ](ptr: *mut T) -> *mut U
60    returns
61        ptr as *mut U,
62    opens_invariants none
63    no_unwind
64;
65
66#[verifier::when_used_as_spec(ptr_mut_cast_const_spec)]
67pub assume_specification<T: PointeeSized>[ <*mut T>::cast_const ](ptr: *mut T) -> *const T
68    returns
69        ptr as *const T,
70    opens_invariants none
71    no_unwind
72;
73
74#[verifier::when_used_as_spec(ptr_cast_mut_spec)]
75pub assume_specification<T: PointeeSized>[ <*const T>::cast_mut ](ptr: *const T) -> *mut T
76    returns
77        ptr as *mut T,
78    opens_invariants none
79    no_unwind
80;
81
82} // verus!
vstd_extra/external/ptr.rs

vstd_extra/external/
ptr.rs
