Strange error jumping to join point in code involving mutable references

[nilehmann]

This is related to #671, but I feel we will need a couple of extra things to make this code work.

#[flux::refined_by(ring_len: int, head: int, tail: int)]
#[flux::invariant(0 < ring_len)]
pub struct RingBuffer<'a, T: 'a> {
    #[flux::field({&mut [T][ring_len] | ring_len > 0})]
    ring: &'a mut [T],
    #[flux::field({usize[head] | head < ring_len})]
    head: usize,
    #[flux::field({usize[tail] | tail < ring_len})]
    tail: usize,
    #[flux::field({usize[ring_len] | ring_len > 0})]
    length: usize,
}

impl<'a, T: Copy + 'a> RingBuffer<'a, T> {
    fn is_full(&self) -> bool {
        todo!()
    }

    fn ring_len(&self) -> usize {
        todo!()
    }

    fn push(&mut self, val: T) -> Option<T> {
        let result = if self.is_full() {
            let val = self.ring[self.head];
            self.head = (self.head + 1) % self.ring_len();
            Some(val) // error[E0999]: error jumping to join point
        } else {
            None
        };

        self.ring[self.tail] = val;
        self.tail = (self.tail + 1) % self.ring_len();
        result
    }
}

error[E0999]: error jumping to join point
  --> attic/playground.rs:27:13
   |
27 |             Some(val) // error[E0999]: error jumping to join point
   |             ^^^^^^^^^
-Ztrack-diagnostics: created at crates/flux-refineck/src/lib.rs:145:50

[enjhnsn2]

Recent developments in mut ref unfolding around calls seems to have fixed this (at least in tock). Close?

[nilehmann]

Wait, I'll add a test for this before closing.