Rust FFI and Aliasing: C -> Rust -> C -> Rust call stacks with C values being aliased: Undefined Behaviour?

Question

I'm trying to wrap my head around Rust's aliasing rules in the following situation:

Let's assume we have a memory allocation in C. We pass a pointer to this allocation to Rust. The Rust function does something with the allocation, and then calls back to C code (without any parameters), where another rust function is called with the same allocation as parameter. For now, let's assume that only the first Rust function gets a mutable reference.

The call stack would look like:

Some C Code (owns data)
  Rust(pointer as &mut)
    Some C code (does not get parameters from Rust)
      Rust(pointer as &)

As a short example, let's assume the following two files: test.c

#include <stdio.h>
#include <stdlib.h>

void first_rust_function(int * ints);
void another_rust_function(const int * ints);
int * arr;
void called_from_rust() {
        another_rust_function(arr);
}
int main(int argc, char ** argv) {
        arr = malloc(3*sizeof(int));
        arr[0]=3;
        arr[1]=4;
        arr[2]=53;
        first_rust_function(arr);
        free(arr);
}

test.rs

use std::os::raw::c_int;
extern "C" { fn called_from_rust(); }
#[no_mangle]
pub extern "C" fn first_rust_function(ints : &mut [c_int;3]) {
    ints[1] = 7;
    unsafe { called_from_rust() };
}
#[no_mangle]
pub extern "C" fn another_rust_function(ints : &[c_int;3]) {
    println!("Second value: {}", ints[1])
}

(For the sake of completeness: running this code prints "Second value: 7")

Please note that the call back to C from Rust (called_from_rust()) does not have any parameters. The Rust compiler therefore does not have the information that anyone might read from the pointed-to value.

My gut feeling tells me that this is undefined behaviour, but I'm not certain.

I've had a quick look at Stacked Borrows, and that model is violated. In the above example only the Rule (protector) gets broken, but if first_rust_function(ints : &mut [c_int;3]) would still use ints after calling called_from_rust() also additional rules would be violated.

However, I haven't found any official documentation stating that Stacked Borrows are the aliasing model used by the Rust compiler, and that everything considered undefined under Stacked Borrows is actually undefined in Rust. Naively this looks similar enough to coercion of &mut to &, so it might actually be sane, but given that called_from_rust() does not take the reference as parameter, I don't think this reasoning applies.

This brings me to the actual questions:

• Is the above code invoking undefined behaviour (and why/why not?)
• If it is undefined: Would the behaviour be well-defined if called_from_rust() would have the pointer as parameter and pass it forward: void called_from_rust(const int * i) { another_rust_function(i); }?
• What if both Rust functions were using &mut [c_int;3]?