extern_spec_std_string_String_from_utf8_unchecked

creusot_contracts::std::string

Function extern_spec_std_string_String_from_utf8_unchecked 

Source 
pub unsafe fn extern_spec_std_string_String_from_utf8_unchecked(
    bytes: Vec<u8>,
) -> String
Expand description

extern spec for ::std::string::String::from_utf8_unchecked

This is not a real function: its only use is for documentation.

terminates

ghost

requires 

exists<s: Seq<char>> s.to_bytes() == bytes@

ensures 

result@.to_bytes() == bytes@