Function extern_spec_Clone_Box_str_clone 

pub fn extern_spec_Clone_Box_str_clone(self_: &Box<str>) -> Box<str>

extern spec for Box<str>::clone

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

terminates

ghost

ensures

(*result)@ == (**self)@