vstd/
modes.rs

1#[allow(unused_imports)]
2use super::pervasive::*;
3#[allow(unused_imports)]
4use super::prelude::*;
5
6verus! {
7
8#[verifier::tracked_swap_primitive]
9pub axiom fn tracked_swap<V>(tracked a: &mut V, tracked b: &mut V)
10    ensures
11        *final(a) == *old(b),
12        *final(b) == *old(a),
13;
14
15/// Make any tracked object permanently shared and get a reference to it.
16///
17/// Tip: If you try to use this and run into problems relating to the introduction
18/// of a lifetime variable, you want to try [`Shared`](crate::shared::Shared) instead.
19pub proof fn tracked_static_ref<V>(tracked v: V) -> (tracked res: &'static V)
20    ensures
21        res == v,
22{
23    tracked_static_mut_ref(v)
24}
25
26/// Make any tracked object permanently mutably borrowed.
27pub axiom fn tracked_static_mut_ref<V>(tracked v: V) -> (tracked res: &'static mut V)
28    ensures
29        *res == v,
30;
31
32} // verus!
vstd/modes.rs

vstd/
modes.rs
