//@compile-flags: -Zmiri-tree-borrows
// This test tests that TB's protector end semantics correctly ensure
// that protected activated writes can be reordered.
fn the_other_function(ref_to_fst_elem: &mut i32, ptr_to_vec: *mut i32) -> *mut i32 {
    // Activate the reference. Afterwards, we should be able to reorder arbitrary writes.
    *ref_to_fst_elem = 0;
    // Here is such an arbitrary write.
    // It could be moved down after the retag, in which case the `funky_ref` would be invalidated.
    // We need to ensure that the `funky_ptr` is unusable even if the write to `ref_to_fst_elem`
    // happens before the retag.
    *ref_to_fst_elem = 42;
    // this creates a reference that is Reserved Lazy on the first element (offset 0).
    // It does so by doing a proper retag on the second element (offset 1), which is fine
    // since nothing else happens at that offset, but the lazy init mechanism means it's
    // also reserved at offset 0, but not initialized.
    let funky_ptr_lazy_on_fst_elem =
        unsafe { (&mut *(ptr_to_vec.wrapping_add(1))) as *mut i32 }.wrapping_sub(1);
    // If we write to `ref_to_fst_elem` here, then any further access to `funky_ptr_lazy_on_fst_elem` would
    // definitely be UB. Since the compiler ought to be able to reorder the write of `42` above down to
    // here, that means we want this program to also be UB.
    return funky_ptr_lazy_on_fst_elem;
}

fn main() {
    let mut v = vec![0, 1];
    // get a pointer to the root of the allocation
    // note that it's not important it's the actual root, what matters is that it's a parent
    // of both references that will be created
    let ptr_to_vec = v.as_mut_ptr();
    let ref_to_fst_elem = unsafe { &mut *ptr_to_vec };
    let funky_ptr_lazy_on_fst_elem = the_other_function(ref_to_fst_elem, ptr_to_vec);
    // now we try to use the funky lazy pointer.
    // It should be UB, since the write-on-protector-end should disable it.
    unsafe { println!("Value of funky: {}", *funky_ptr_lazy_on_fst_elem) } //~ ERROR: /reborrow through .* is forbidden/
}