__builtin_isinf{,_sign} require a floating-point argument

This isn't necessarily spelled out in the signature of the function, but
GCC's documentation states this requirement.

Author: tautschnig

regression/cbmc-library/Float_lib1/main.c

@@ -43,10 +43,10 @@ int main()
 
   _Static_assert(__builtin_isnormal(DBL_MIN), "__builtin_isnormal is constant");
 
-  _Static_assert(!__builtin_isinf(0), "__builtin_isinf is constant");
+  _Static_assert(!__builtin_isinf(0.0), "__builtin_isinf is constant");
 
   _Static_assert(
-    __builtin_isinf_sign(0) == 0, "__builtin_isinf_sign is constant");
+    __builtin_isinf_sign(0.0) == 0, "__builtin_isinf_sign is constant");
 
 #endif
 

src/ansi-c/c_typecheck_expr.cpp

@@ -2457,6 +2457,15 @@ exprt c_typecheck_baset::do_special_functions(
 
     typecheck_function_call_arguments(expr);
 
+    const exprt &fp_value = expr.arguments().front();
+
+    if(fp_value.type().id() != ID_floatbv)
+    {
+      error().source_location = fp_value.source_location();
+      error() << "non-floating-point argument for " << identifier << eom;
+      throw 0;
+    }
+
     isinf_exprt isinf_expr(expr.arguments().front());
     isinf_expr.add_source_location()=source_location;
 
@@ -2477,6 +2486,13 @@ exprt c_typecheck_baset::do_special_functions(
 
     const exprt &fp_value = expr.arguments().front();
 
+    if(fp_value.type().id() != ID_floatbv)
+    {
+      error().source_location = fp_value.source_location();
+      error() << "non-floating-point argument for " << identifier << eom;
+      throw 0;
+    }
+
     isinf_exprt isinf_expr(fp_value);
     isinf_expr.add_source_location() = source_location;
 

src/util/simplify_expr_floatbv.cpp

@@ -20,9 +20,6 @@ Author: Daniel Kroening, [email protected]
 simplify_exprt::resultt<>
 simplify_exprt::simplify_isinf(const unary_exprt &expr)
 {
-  if(expr.op().type().id() != ID_floatbv)
-    return unchanged(expr);
-
   if(expr.op().is_constant())
   {
     ieee_floatt value(to_constant_expr(expr.op()));