Skip to main content

rw_fallible

ostd::mm::io

Function rw_fallible 

Source 
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<'_>>,
requires
old(reader).inv(),
old(writer).inv(),
old(owner_r).inv(),
old(owner_w).inv(),
old(reader).wf(*old(owner_r)),
old(writer).wf(*old(owner_w)),
old(owner_r).is_fallible && old(owner_w).is_fallible,
ensures
final(reader).inv(),
final(writer).inv(),
final(owner_r).inv(),
final(owner_w).inv(),
final(reader).wf(*final(owner_r)),
final(writer).wf(*final(owner_w)),
final(owner_r).params_eq(*old(owner_r)),
final(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_eq are preserved for both sides.