Function extern_spec_std_slice_from_mut 

pub fn extern_spec_std_slice_from_mut<T>(s: &mut T) -> &mut [T]

extern spec for ::std::slice::from_mut<T>

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

terminates

ghost

ensures

result@.len() == 1

ensures

result@[0] == *s

ensures

(^result)@.len() == 1

ensures

(^result)@[0] == ^s