Function bamts_array_push 

#[unsafe(no_mangle)]
pub unsafe extern "C" fn bamts_array_push(
    frame: *mut ShadowFrame,
    array: u64,
    value: u64,
    out: *mut Completion,
) -> u32

Safety

The caller must provide a live, uniquely owned frame whose nonempty handle range is disjoint from its header, and a live, aligned, writable out when this helper has one. Both remain valid and unaliased for the full call.

bamts_array_push(frame, array, value, out).