Add support for transitive modifies clause

[celinval]

Requested feature: Enable contracts for functions that modify memory via encapsulated pointer.
Use case: Kani contracts require that all writeable memory to be specified. However, they may not be visible in the current context
Link to relevant documentation (Rust reference, Nomicon, RFC):

Test case:

mod heap {
#[derive(Default)]
pub struct HeapArray<T, const N: usize> {
  inner: Box<[T; N]>,
}

impl<T, const N: usize> HeapArray<T, N> {
  pub fn set(&mut self, val: T, idx: usize) {
  }
}
}

mod other {
  struct Stack<T> {
     buf: HeapArray,
     next: usize,
  }

  impl<T> Stack<T> {
    #[modifies(buf)] // This is not enough today
    #[kani::ensures(|_| self.contains(val))]
    fn enqueue(&mut self, val: T) {
      assert!(!self.is_full());
      self.buf.set(val, next);
    }
  }
}

[celinval]

A good example here is Arc, which contains a pointer to an ArcInner which includes the object itself, but also an atomic counter which is changed in get_mut.