Introduce round_to_integral_exprt

This adds a new expression, round_to_integral, which rounds an IEEE 754
floating-point number given as bit-vector to the nearest integer,
considering the explicitly given rounding mode.

Author: kroening

src/ansi-c/c_typecheck_expr.cpp

@@ -3237,6 +3237,21 @@ exprt c_typecheck_baset::do_special_functions(
 
     return std::move(infl_expr);
   }
+  else if(identifier == CPROVER_PREFIX "round_to_integral")
+  {
+    if(expr.arguments().size() != 2)
+    {
+      error().source_location = f_op.source_location();
+      error() << identifier << " expects two arguments" << eom;
+      throw 0;
+    }
+
+    auto round_to_integral_expr =
+      floatbv_round_to_integral_exprt{expr.arguments()[0], expr.arguments()[1]};
+    round_to_integral_expr.add_source_location() = source_location;
+
+    return std::move(round_to_integral_expr);
+  }
   else if(
     identifier == CPROVER_PREFIX "abs" || identifier == CPROVER_PREFIX "labs" ||
     identifier == CPROVER_PREFIX "llabs" ||