Function pre::alloc::vec::Vec__impl__set_len__

pub fn Vec__impl__set_len__()

A stub for the preconditions of the alloc_lib::vec::Vec<T>::set_len function.

What is this function?

This function was generated by an impl block inside a extern_crate attribute that looked like this:

impl< T > Vec < T >  {
    unsafe fn set_len(& mut self, new_len : usize);
    /* other items omitted */
}

Preconditions on external functions inside of an impl block are attached to empty functions like this one. When the preconditions should be checked, a call to this function is inserted, which triggers checking the preconditions.

This function has preconditions

This function has the following preconditions generated by pre attributes:

• new_len <= self.capacity()
• the elements at old_len..new_len are initialized

To call the function you need to assure that the preconditions hold:

#[forward(impl pre::alloc::vec::Vec)]
#[assure(
    new_len <= self.capacity(),
    reason = "<specify the reason why you can assure this here>"
)]
#[assure(
    "the elements at `old_len..new_len` are initialized",
    reason = "<specify the reason why you can assure this here>"
)]
x.set_len(/* parameters omitted */);