fix return types of various __builtin_is* functions

Author: Daniel Kroening

src/ansi-c/c_typecheck_expr.cpp

@@ -2210,7 +2210,10 @@ exprt c_typecheck_baset::do_special_functions(
     isnan_exprt isnan_expr(expr.arguments().front());
     isnan_expr.add_source_location()=source_location;
 
-    return isnan_expr;
+    if(expr.type()!=isnan_expr.type())
+      return typecast_exprt(isnan_expr, expr.type());
+    else
+      return isnan_expr;
   }
   else if(identifier==CPROVER_PREFIX "isfinitef" ||
           identifier==CPROVER_PREFIX "isfinited" ||
@@ -2226,7 +2229,10 @@ exprt c_typecheck_baset::do_special_functions(
     isfinite_exprt isfinite_expr(expr.arguments().front());
     isfinite_expr.add_source_location()=source_location;
 
-    return isfinite_expr;
+    if(expr.type()!=isfinite_expr.type())
+      return typecast_exprt(isfinite_expr, expr.type());
+    else
+      return isfinite_expr;
   }
   else if(identifier==CPROVER_PREFIX "inf" ||
           identifier=="__builtin_inf")
@@ -2298,14 +2304,17 @@ exprt c_typecheck_baset::do_special_functions(
     if(expr.arguments().size()!=1)
     {
       err_location(f_op);
-      error() << "isinf expects one operand" << eom;
+      error() << identifier << " expects one operand" << eom;
       throw 0;
     }
 
     isinf_exprt isinf_expr(expr.arguments().front());
     isinf_expr.add_source_location()=source_location;
 
-    return isinf_expr;
+    if(expr.type()!=isinf_expr.type())
+      return typecast_exprt(isinf_expr, expr.type()); // int
+    else
+      return isinf_expr; // bool
   }
   else if(identifier==CPROVER_PREFIX "isnormalf" ||
           identifier==CPROVER_PREFIX "isnormald" ||
@@ -2314,14 +2323,26 @@ exprt c_typecheck_baset::do_special_functions(
     if(expr.arguments().size()!=1)
     {
       err_location(f_op);
-      error() << "isnormal expects one operand" << eom;
+      error() << identifier << " expects one operand" << eom;
+      throw 0;
+    }
+
+    const exprt &fp_value = expr.arguments()[0];
+
+    if(fp_value.type().id() != ID_floatbv)
+    {
+      err_location(fp_value);
+      error() << "non-floating-point argument for " << identifier << eom;
       throw 0;
     }
 
     isnormal_exprt isnormal_expr(expr.arguments().front());
     isnormal_expr.add_source_location()=source_location;
 
-    return isnormal_expr;
+    if(expr.type()!=isnormal_expr.type())
+      return typecast_exprt(isnormal_expr, expr.type()); // int
+    else
+      return isnormal_expr; // bool
   }
   else if(identifier==CPROVER_PREFIX "signf" ||
           identifier==CPROVER_PREFIX "signd" ||
@@ -2333,14 +2354,17 @@ exprt c_typecheck_baset::do_special_functions(
     if(expr.arguments().size()!=1)
     {
       err_location(f_op);
-      error() << "sign expects one operand" << eom;
+      error() << identifier << " expects one operand" << eom;
       throw 0;
     }
 
     sign_exprt sign_expr(expr.arguments().front());
     sign_expr.add_source_location()=source_location;
 
-    return sign_expr;
+    if(expr.type()!=sign_expr.type())
+      return typecast_exprt(sign_expr, expr.type()); // int
+    else
+      return sign_expr; // bool
   }
   else if(identifier=="__builtin_popcount" ||
           identifier=="__builtin_popcountl" ||