Struct InlineCtx 

pub(crate) struct InlineCtx<'z3, 'tcx> {
    pub inline_depth: usize,
    pub arg_referents: Vec<Option<Local>>,
    pub deferred_field_writes: Vec<(Local, Vec<usize>, VmValue<'z3, 'tcx>)>,
}

Scratch state for the recursive inlined-callee mechanism ([crate::verify::vm::call::exec_inline_call]), which unwinds via the Rust call stack, is bounded by inline_depth, and stashes its per-call bindings in arg_referents/deferred_field_writes.

(The path-replay mechanism — CalleeEntry/CalleeExit items — keeps its saved caller frames on VmState::caller_frames instead, which lives next to VmState::current_frame to form the frame stack.)

Deferring &mut writes across the inline frame

While the callee runs, the caller’s local_alloc (the name → allocation binding) is parked in the saved FrameState, so a write through a &mut argument cannot resolve the caller referent local by address and land in its field values immediately. arg_referents pre-resolves (before save_frame) which caller local each &mut argument points at, and deferred_field_writes collects the writes to replay once the caller is restored:

struct Foo { field: i32 }
fn bar(foo: &mut Foo) { foo.field = 1; }   // inlined callee
fn main() {
    let mut x = Foo { field: 0 };
    bar(&mut x);                            // inline `bar`
}

1. Enter bar: save_frame parks main’s local_alloc; arg_referents[0] = x.
2. Run bar: foo.field = 1 ((*foo).field) can no longer resolve x by address (the caller’s address map is gone), so it pushes (x, [0], 1).
3. Exit bar: restore_frame brings main’s local_alloc back, then the deferred write is replayed, giving x.field == 1.

Fields

inline_depth: usize

Current inlining depth (nested inlined callees), bounded by MAX_INLINE_DEPTH.

arg_referents: Vec<Option<Local>>

During exec_inline_call, maps each callee argument index to the caller local its value points at (resolved from the reference’s address term before the caller’s address map is saved away). Used by exec_assign to resolve (*self).field = val writes through a &mut self reborrow temp back to the caller’s referent.

deferred_field_writes: Vec<(Local, Vec<usize>, VmValue<'z3, 'tcx>)>

Field writes through a &mut argument collected during exec_inline_call, replayed against the caller’s field values after restore_frame (the caller’s address map is parked while the callee runs). Each entry is (caller_local, field_path, value), where caller_local comes from arg_referents — the caller local the &mut argument points at, not the argument itself.

Trait Implementations

impl<'z3, 'tcx> Default for InlineCtx<'z3, 'tcx>

fn default() -> Self

Returns the “default value” for a type.