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.