fn visit_drop()

in checker/src/block_visitor.rs [429:524]


    fn visit_drop(
        &mut self,
        place: &mir::Place<'tcx>,
        target: mir::BasicBlock,
        unwind: Option<mir::BasicBlock>,
    ) {
        let place_path = self.get_path_for_place(place);
        let path = place_path.canonicalize(&self.bv.current_environment);
        let mut ty = self
            .type_visitor()
            .get_path_rustc_type(&path, self.bv.current_span);
        if ty.is_never() {
            ty = self
                .type_visitor()
                .get_rustc_place_type(place, self.bv.current_span);
            debug!("ty {:?}", ty);
        }
        self.type_visitor_mut()
            .set_path_rustc_type(path.clone(), ty);

        if let TyKind::Adt(def, substs) = ty.kind() {
            if let Some(destructor) = self.bv.tcx.adt_destructor(def.did()) {
                let actual_argument_types = vec![self
                    .bv
                    .cv
                    .tcx
                    .mk_mut_ref(self.bv.cv.tcx.lifetimes.re_static, ty)];
                let callee_generic_arguments = self
                    .type_visitor()
                    .specialize_substs(substs, &self.type_visitor().generic_argument_map);
                let callee_generic_argument_map = self.type_visitor().get_generic_arguments_map(
                    def.did(),
                    callee_generic_arguments,
                    &actual_argument_types,
                );
                let fun_ty = self.bv.tcx.type_of(destructor.did);
                let func_const = self
                    .visit_function_reference(destructor.did, fun_ty, Some(substs))
                    .clone();
                let func_to_call = Rc::new(func_const.clone().into());
                let ref_to_path_value = AbstractValue::make_reference(path.clone());
                let actual_args = vec![(
                    Path::new_computed(ref_to_path_value.clone()),
                    ref_to_path_value,
                )];
                let function_constant_args =
                    self.get_function_constant_args(&actual_args, &actual_argument_types);

                // Since drop calls are implicit in the source code, we treat them like foreign
                // code and suppress diagnostics. In most cases this should improve precision, but
                // it does sacrifice soundness, so we still give diagnostics when in Paranoid mode.
                let saved_assume_preconditions_of_next_call =
                    self.bv.assume_preconditions_of_next_call;
                self.bv.assume_preconditions_of_next_call = saved_assume_preconditions_of_next_call
                    || self.bv.cv.options.diag_level != DiagLevel::Paranoid;

                // We need a place, but the drop statement does not provide one, so we use the
                // local being dropped as the return result.
                let destination = Some((*place, target));
                let mut call_visitor = CallVisitor::new(
                    self,
                    destructor.did,
                    Some(callee_generic_arguments),
                    callee_generic_argument_map.clone(),
                    self.bv.current_environment.clone(),
                    func_const,
                );
                call_visitor.actual_args = actual_args;
                call_visitor.actual_argument_types = actual_argument_types;
                call_visitor.cleanup = unwind;
                call_visitor.destination = destination;
                call_visitor.callee_fun_val = func_to_call;
                call_visitor.function_constant_args = &function_constant_args;

                let function_summary = call_visitor.get_function_summary().unwrap_or_default();
                call_visitor.transfer_and_refine_into_current_environment(&function_summary);
                // Undo the return type update of the fake return value place.
                self.type_visitor_mut()
                    .set_path_rustc_type(path.clone(), ty);
                self.bv.assume_preconditions_of_next_call = saved_assume_preconditions_of_next_call;
                return;
            }
        }

        // Propagate the entry condition to the successor blocks.
        self.bv
            .current_environment
            .exit_conditions
            .insert_mut(target, self.bv.current_environment.entry_condition.clone());
        if let Some(unwind_target) = unwind {
            self.bv.current_environment.exit_conditions.insert_mut(
                unwind_target,
                self.bv.current_environment.entry_condition.clone(),
            );
        }
    }