Skip to main content

rebind_property_to_args

Function rebind_property_to_args 

Source
fn rebind_property_to_args<'tcx>(
    prop: &mut Property<'tcx>,
    args: &[Operand<'tcx>],
    callee_args: &GenericArgs<'tcx>,
    body: &Body<'tcx>,
) -> bool
Expand description

Rewrite a contract’s argument references (PlaceBase::Arg(i)) onto the enclosing callee’s parameters using the call-site argument list. This rebinds a leaf callee’s contract (e.g. ptr::write’s ValidPtr(self, T, 1)) to the wrapper callee’s arguments (e.g. maybe_init_slot’s ptr).

Returns false when a referenced argument cannot be traced to a parameter (a constant, a field projection, a temporary, or a call result). Such a contract expresses an internal invariant of the leaf callee and cannot be restated as a precondition on this callee’s parameters, so it is dropped.