Function vstd::pcm_lib::update_mut

source · 
pub proof fn update_mut<P: PCM>(tracked r: &mut Resource<P>, new_value: P)
Expand description
requires
frame_preserving_update(old(r).value(), new_value),
ensures
r.loc() == old(r).loc(),
r.value() == new_value,

Updates r to have new value new_value. This must be a frame-preserving update. That is, new_value must be compatible with all frames old(r).value() was compatible with.