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        *a == *old(b),
12        *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 axiom fn tracked_static_ref<V>(tracked v: V) -> (tracked res: &'static V)
20    ensures
21        res == v,
22;
23
24} // verus!
vstd/modes.rs

vstd/
modes.rs
