fn numeric_cast()

in checker/src/z3_solver.rs [1380:1487]
99 lines of code
12 McCabe index (conditional complexity)

    fn numeric_cast(
        &self,
        expression: &Expression,
        target_type: ExpressionType,
    ) -> (bool, z3_sys::Z3_ast) {
        unsafe {
            let path_symbol = self.get_symbol_for(expression);
            match target_type {
                ExpressionType::F32 => (
                    true,
                    z3_sys::Z3_mk_const(self.z3_context, path_symbol, self.f32_sort),
                ),
                ExpressionType::F64 => (
                    true,
                    z3_sys::Z3_mk_const(self.z3_context, path_symbol, self.f64_sort),
                ),
                _ => {
                    if target_type.is_integer() || target_type == ExpressionType::Char {
                        let exp_type = expression.infer_type();
                        if exp_type == target_type {
                            self.get_as_numeric_z3_ast(expression)
                        } else if exp_type.is_signed_integer() {
                            // In order to (re-interpret) cast the expr value to unsigned, or
                            // just to safely truncate it, we need to compute the 2's complement.
                            let expr_ast = self.get_as_numeric_z3_ast(expression).1;
                            let modulo_constant = target_type.as_unsigned().modulo_constant();
                            let modulo_ast = if modulo_constant.is_bottom() {
                                let num_str = "340282366920938463463374607431768211456";
                                let c_string = CString::new(num_str).unwrap();
                                z3_sys::Z3_mk_numeral(
                                    self.z3_context,
                                    c_string.into_raw(),
                                    self.int_sort,
                                )
                            } else {
                                self.get_constant_as_ast(&modulo_constant)
                            };
                            let args = vec![expr_ast, modulo_ast];
                            let complement = z3_sys::Z3_mk_add(self.z3_context, 2, args.as_ptr());
                            let is_negative =
                                z3_sys::Z3_mk_lt(self.z3_context, expr_ast, self.zero);
                            let mut unsigned_ast = z3_sys::Z3_mk_ite(
                                self.z3_context,
                                is_negative,
                                complement,
                                expr_ast,
                            );

                            // Truncate the complement by taking its unsigned remainder, if need be
                            if target_type.bit_length() < exp_type.bit_length() {
                                unsigned_ast =
                                    z3_sys::Z3_mk_rem(self.z3_context, unsigned_ast, modulo_ast);
                            }

                            self.transmute_to_signed_if_necessary(
                                target_type,
                                modulo_ast,
                                unsigned_ast,
                            )
                        } else if exp_type.is_unsigned_integer() || exp_type == ExpressionType::Char
                        {
                            let mut unsigned_ast = self.get_as_numeric_z3_ast(expression).1;
                            let modulo_constant = target_type.as_unsigned().modulo_constant();
                            let modulo_ast = if modulo_constant.is_bottom() {
                                let num_str = "340282366920938463463374607431768211456";
                                let c_string = CString::new(num_str).unwrap();
                                z3_sys::Z3_mk_numeral(
                                    self.z3_context,
                                    c_string.into_raw(),
                                    self.int_sort,
                                )
                            } else {
                                self.get_constant_as_ast(&modulo_constant)
                            };

                            // Truncate the expression value if need be
                            if target_type.bit_length() < exp_type.bit_length() {
                                unsigned_ast =
                                    z3_sys::Z3_mk_rem(self.z3_context, unsigned_ast, modulo_ast);
                            }

                            self.transmute_to_signed_if_necessary(
                                target_type,
                                modulo_ast,
                                unsigned_ast,
                            )
                        } else {
                            // Could be a thin pointer or an enum
                            (
                                false,
                                z3_sys::Z3_mk_const(self.z3_context, path_symbol, self.int_sort),
                            )
                        }
                    } else {
                        if target_type != ExpressionType::ThinPointer {
                            // target type is not numeric and not a pointer, but the result of the
                            // cast is expected to be numeric. This probably a mistake.
                            info!(
                                "non numeric cast to {:?} found in numeric context {:?}",
                                target_type, expression
                            );
                        }
                        self.get_as_numeric_z3_ast(expression)
                    }
                }
            }
        }
    }