ptr_ref

vstd_extra::array_ptr

Function ptr_ref 

Source 
pub exec fn ptr_ref<V, const N: usize>(
    ptr: *mut [V; N],
    verus_tmp_perm: Tracked<&PointsToArray<V, N>>,
) -> res : &[V; N]
Expand description
requires
perm.ptr() == ptr,
perm.is_init_all(),
ensures
forall |i: int| 0 <= i < N ==> #[trigger] res[i] == perm.opt_value()[i].value(),

Get the immutable reference of the entire array