Function extern_spec_From__refmut_str_String_from 

pub fn extern_spec_From__refmut_str_String_from(s: &mut String) -> String

extern spec for String::from

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

ghost

ensures

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