read_bytes
io.buffered.read_bytes
Postcondition
post debug: {
match result
error => true
s Sequence u8 => s.count <= n
}0.095dev (GIT hash 09dff08de289bbb6f7136c7e2f8c66dcc1856bba)
post debug: {
match result
error => true
s Sequence u8 => s.count <= n
}
if the returned sequence is empty or count is less than n, end of file has been reached.