Function extern_spec_From__refmut_str_Box_str_from 

pub fn extern_spec_From__refmut_str_Box_str_from(s: &mut str) -> Box<str>

extern spec for Box<str>::from

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

ghost

ensures

result@ == s@ && ^s == *s