vstd_extra/
auxiliary.rs

1use vstd::prelude::*;
2
3verus! {
4
5// Produces an arbitrary PointsTo permission for type T, this is sound because one can not use
6// such a permission to access memory.
7#[verifier(external_body)]
8pub proof fn arbitrary_cell_pointsto<T>() -> (tracked res: vstd::cell::pcell::PointsTo<T>) {
9    unimplemented!();
10}
11
12} // verus!