Remove RoundTiesEven intrinsics

Author: zhassan-aws

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

@@ -431,9 +431,6 @@ impl GotocCtx<'_> {
             Intrinsic::RotateRight => codegen_intrinsic_binop!(ror),
             Intrinsic::RoundF32 => codegen_simple_intrinsic!(Roundf),
             Intrinsic::RoundF64 => codegen_simple_intrinsic!(Round),
-            Intrinsic::RoundTiesEvenF32 | Intrinsic::RoundTiesEvenF64 => {
-                self.codegen_round_to_integral(cbmc::RoundingMode::ToNearest, fargs, place, loc)
-            }
             Intrinsic::SaturatingAdd => codegen_intrinsic_binop_with_mm!(saturating_add),
             Intrinsic::SaturatingSub => codegen_intrinsic_binop_with_mm!(saturating_sub),
             Intrinsic::SinF32 => codegen_simple_intrinsic!(Sinf),
@@ -641,23 +638,6 @@ impl GotocCtx<'_> {
         dividend_is_int_min.and(divisor_is_minus_one).not()
     }
 
-    // Builds a floatbv_round_to_integral expression with specified cbmc::RoundingMode.
-    fn codegen_round_to_integral(
-        &mut self,
-        rounding_mode: cbmc::RoundingMode,
-        mut fargs: Vec<Expr>,
-        place: &Place,
-        loc: Location,
-    ) -> Stmt {
-        let place_ty = self.place_ty_stable(place);
-        let result_type = self.codegen_ty_stable(place_ty);
-        let f = fargs.remove(0);
-        assert!(fargs.is_empty());
-        let rm = Expr::int_constant(rounding_mode, Type::c_int());
-        let expr = Expr::floatbv_round_to_integral(f, rm, result_type);
-        self.codegen_expr_to_place_stable(place, expr, loc)
-    }
-
     /// Intrinsics of the form *_with_overflow
     fn codegen_op_with_overflow(
         &mut self,