pub exec fn rw_fallible(
reader: &mut VmReader<'_>,
writer: &mut VmWriter<'_>,
) -> r : Result<usize, (Error, usize)>Expand description
with
Tracked(owner_r): Tracked<&mut VmIoOwner<'_>>,
Tracked(owner_w): Tracked<&mut VmIoOwner<'_>>,old(reader).inv(),old(writer).inv(),old(owner_r).inv(),old(owner_w).inv(),old(owner_r).inv_with_reader(*old(reader)),old(owner_w).inv_with_writer(*old(writer)),old(owner_r).is_fallible && old(owner_w).is_fallible,reader.inv(),writer.inv(),owner_r.inv(),owner_w.inv(),owner_r.inv_with_reader(*reader),owner_w.inv_with_writer(*writer),owner_r.params_eq(*old(owner_r)),owner_w.params_eq(*old(owner_w)),Performs a fallible transfer from reader to writer.
§Verified Properties
§Preconditions
reader,writer, and their associated owners must satisfy their invariants.- Each owner must match the corresponding reader or writer.
- Both owners must be marked fallible.
§Postconditions
- The reader, writer, and both owners still satisfy their invariants.
- The owner parameters tracked by
VmIoOwner::params_eqare preserved for both sides.