Function extern_spec_str_as_bytes 

pub fn extern_spec_str_as_bytes(self_: &str) -> &[u8] 

extern spec for str::as_bytes

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

ghost

ensures

self