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(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,
ensures
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)),