Method run_terminator

src/checker/assertion_checker.rs:70–139

(
        &mut self,
        term: &Terminator<'tcx>,
        abstract_value: &AbstractDomain<DomainType>,
    )

    IntervalAbstractDomain<DomainType>: GetDomainType,
{
    fn run_terminator(
        &mut self,
        term: &Terminator<'tcx>,
        abstract_value: &AbstractDomain<DomainType>,
    ) {
        let Terminator { source_info, kind } = term;
        let span = source_info.span;
        if let TerminatorKind::Assert {
            cond,
            expected,
            msg,
            ..
        } = &kind
        {
            debug!(
                "Checking assertion: {:?} with message: {:?}, exptected: {}",
                term, msg, expected
            );
            debug!("Current state: {:?}", abstract_value);

            if let Some(place) = cond.place() {
                if let Some(cond_val) = self.body_visitor.place_to_abstract_value.get(&place) {
                    debug!("place: {:?}, cond_val: {:?}", place, cond_val);
                    let cond_val = cond_val.clone();
                    let check_result = match msg.deref() {
                        mir::AssertKind::Overflow(..) => {
                            self.check_overflow(cond_val.clone(), *expected, abstract_value)
                        }
                        mir::AssertKind::MisalignedPointerDereference { .. } => {
                            return;
                        }
                        _ => self.check_assert_condition(cond_val, *expected, abstract_value),
                    };

                    match check_result {
                        CheckerResult::Safe => (),
                        CheckerResult::Unsafe => {
                            let error = self.body_visitor.context.session.dcx().struct_span_warn(
                                span,
                                format!(
                                    "[Bypasser] Provably error: {:?}",
                                    self.body_visitor.recover_var_name(msg.deref())
                                ),
                            );
                            self.body_visitor.emit_diagnostic(
                                error,
                                false,
                                DiagnosticCause::from(msg.deref()),
                            );
                        }
                        CheckerResult::Warning => {
                            // let warning = self.body_visitor.context.session.dcx().struct_span_warn(
                            //     span,
                            //     format!(
                            //         "[Bypasser] Possible error: {:?}",
                            //         self.body_visitor.recover_var_name(msg.deref())
                            //     ),
                            // );