axiom_nonull_from_ptr_mut_eq

vstd_extra::external::nonnull

Function axiom_nonull_from_ptr_mut_eq 

Source 
pub broadcast proof fn axiom_nonull_from_ptr_mut_eq<T: PointeeSized>(ptr: *mut T)
Expand description
requires
ptr@.addr != 0,
ensures
ptr_mut_from_nonull(#[trigger] nonnull_from_ptr_mut(ptr)) == ptr,