CBMC's default assumption for a function that receives a pointer is that no modification of the pointer or its target is performed. This means that for functions that receive (and mutate) &mut T we need to specify an assigns clause in addition to requires and ensures.

In the first iteration we propose to add a simple kani::assigns macro which takes a list of lvalues that are lowered the usual way and passed onto CBMC as a __CPROVER_assigns clause.

In addition to add some basic support for arrays we propose using slice syntax [..] to denote that an entire array or the pointed-to range of a pointer might be assigned to.

Here is an example of what this looks like

#[post(self.len() == 0)]
#[kani::assigns((*self).keys.buf.ptr.pointer.pointer[..], (*self).keys.buf.cap, (*self).keys.len)]
#[kani::assigns((*self).values.buf.ptr.pointer.pointer[..], (*self).values.buf.cap, (*self).values.len)]
pub fn clear(&mut self) {
    self.keys.clear();
    self.values.clear();
}

Note this is very basic and leaks private detail, e.g. the lvalues assigns can refer to private fields