partial_valid_partial_invalid_utf8

vstd::utf8

Function partial_valid_partial_invalid_utf8 

Source 
pub proof fn partial_valid_partial_invalid_utf8(bytes: Seq<u8>, i: int)
Expand description
requires
0 <= i <= bytes.len(),
valid_utf8(bytes.subrange(0, i)),
!valid_utf8(bytes.subrange(i, bytes.len() as int)),
ensures
!valid_utf8(bytes),

Ensures that a byte sequence is not a valid UTF-8 byte sequence when it has a suffix that is not a valid UTF-8 byte sequence.