Post and invariant contracts don't play nice with mutable borrows
Hello, Stumbled onto your crate while looking for ways to more explicitly work with contracts for my own crates, but I've been stopped in my tracks when doing my first mutable borrow method :
// #[post(self.contains_key(key) ==> ret.is_some())]
// #[post(!self.contains_key(key) ==> ret.is_none())]
// #[post(true)]
pub fn get_mut<'l, Q: PartialEq<K>>(&'l mut self, key: &Q) -> Option<&'l mut V> {
if let Some(position) = self.keys.iter().position(|k| key == k) {
Some(&mut self.values[position])
} else {
None
}
}
ANY post or invariant contract will result in rust finding conflicts in lifetimes for the mutable borrows.
I'll try working on a fix for that, I'm thinking of casting &mut references to & references through unsafe pointers, when passing the parameters to the contract clauses. This shouldn't cause memory sanity issues due to the lifetimes of the mutable references which are currently the root of this issue being greater than the lifetime of the contracts.