vstd_extra/
ptr_extra.rs

1use vstd::prelude::*;
2
3use vstd::simple_pptr::*;
4
5verus! {
6
7#[macro_export]
8macro_rules! borrow_field {
9    ($ptr:expr) => { $ptr };
10    ($ptr:expr => $field:tt, $perm:expr) => {
11        verus_exec_expr!(
12            $ptr.borrow(Tracked($perm)).$field
13    )};
14}
15
16#[macro_export]
17macro_rules! update_field {
18    ($ptr:expr => $field:tt <- $val:expr; $set:expr , $idx:expr) => {
19        verus_exec_expr!(
20        {
21            let tracked mut __own = $set.tracked_remove($idx);
22            let mut __tmp = $ptr.take(Tracked(&mut __own));
23            __tmp.$field = $val;
24            $ptr.put(Tracked(&mut __own), __tmp);
25            proof { $set.tracked_insert($idx, __own); }
26        })
27    };
28    ($ptr:expr => $field:tt <- $val:expr; $perm:expr) => {
29        verus_exec_expr!(
30        {
31            let mut __tmp = $ptr.take(Tracked(&mut $perm));
32            __tmp.$field = $val;
33            $ptr.put(Tracked(&mut $perm), __tmp);
34        })
35    };
36    ($ptr:expr => $field:tt += $val:expr; $perm:expr) => {
37        verus_exec_expr!(
38        {
39            let mut __tmp = $ptr.take(Tracked(&mut $perm));
40            __tmp.$field = __tmp.$field + $val;
41            $ptr.put(Tracked(&mut $perm), __tmp);
42        })
43    };
44    ($ptr:expr => $field:tt -= $val:expr; $perm:expr) => {
45        verus_exec_expr!(
46        {
47            let mut __tmp = $ptr.take(Tracked(&mut $perm));
48            __tmp.$field = __tmp.$field - $val;
49            $ptr.put(Tracked(&mut $perm), __tmp);
50        })
51    }
52}
53
54} // verus!
55pub use {borrow_field, update_field};
vstd_extra/ptr_extra.rs

vstd_extra/
ptr_extra.rs
