fx

Author: Daniel Kroening

src/ansi-c/c_typecheck_expr.cpp

@@ -2195,10 +2195,11 @@ exprt c_typecheck_baset::do_special_functions(
 
     return bswap_expr;
   }
-  else if(identifier=="__builtin_fpclassify" ||
-          identifier==CPROVER_PREFIX "fpclassify")
+  else if(
+    identifier == "__builtin_fpclassify" ||
+    identifier == CPROVER_PREFIX "fpclassify")
   {
-    if(expr.arguments().size()!=6)
+    if(expr.arguments().size() != 6)
     {
       err_location(f_op);
       error() << identifier << " expects six arguments" << eom;
@@ -2210,28 +2211,33 @@ exprt c_typecheck_baset::do_special_functions(
     // FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL and FP_ZERO.
     // gcc expects this to be able to produce compile-time constants.
 
-    if(expr.arguments()[5].type().id()!=ID_floatbv)
+    const auto &arguments = expr.arguments();
+    const exprt &fp_value=arguments[5];
+
+    if(fp_value.type().id() != ID_floatbv)
     {
-      err_location(expr.arguments()[5]);
+      err_location(fp_value);
       error() << "non-floating-point argument for " << identifier << eom;
       throw 0;
     }
 
-    const auto &floatbv_type=to_floatbv_type(expr.arguments()[5].type());
+    const auto &floatbv_type = to_floatbv_type(fp_value.type());
 
-    const exprt zero=
-      ieee_floatt::zero(floatbv_type).to_expr();
+    const exprt zero = ieee_floatt::zero(floatbv_type).to_expr();
 
-    return
-      if_exprt(unary_predicate_exprt(ID_isnan, expr.arguments()[5]),
-               expr.arguments()[0],
-      if_exprt(unary_predicate_exprt(ID_isinf, expr.arguments()[5]),
-               expr.arguments()[1],
-      if_exprt(unary_predicate_exprt(ID_isnormal, expr.arguments()[5]),
-               expr.arguments()[2],
-      if_exprt(ieee_float_equal_exprt(expr.arguments()[5], zero),
-               expr.arguments()[4],
-      expr.arguments()[3])))); // subnormal
+    return if_exprt(
+      isnan_exprt(fp_value),
+      arguments[0],
+      if_exprt(
+        isinf_exprt(fp_value),
+        arguments[1],
+        if_exprt(
+          isnormal_exprt(fp_value),
+          arguments[2],
+          if_exprt(
+            ieee_float_equal_exprt(fp_value, zero),
+            arguments[4],
+            arguments[3])))); // subnormal
   }
   else if(identifier==CPROVER_PREFIX "isnanf" ||
           identifier==CPROVER_PREFIX "isnand" ||

src/ansi-c/library/math.c

@@ -287,8 +287,8 @@ inline short _fdclass(float f) {
 
 inline int __fpclassifyd(double d) {
   __CPROVER_HIDE:
-  return __CPROVER_fpclassify(
-    FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, d);
+    return __CPROVER_fpclassify(
+      FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, d);
 }
 
 /* FUNCTION: __fpclassifyf */
@@ -300,8 +300,8 @@ inline int __fpclassifyd(double d) {
 
 inline int __fpclassifyf(float f) {
   __CPROVER_HIDE:
-  return __CPROVER_fpclassify(
-    FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, f);
+    return __CPROVER_fpclassify(
+      FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, f);
 }
 
 /* FUNCTION: __fpclassifyl */
@@ -313,8 +313,8 @@ inline int __fpclassifyf(float f) {
 
 inline int __fpclassifyl(long double f) {
   __CPROVER_HIDE:
-  return __CPROVER_fpclassify(
-    FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, f);
+    return __CPROVER_fpclassify(
+      FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, f);
 }
 
 /* FUNCTION: __fpclassify */
@@ -330,14 +330,14 @@ inline int __fpclassifyl(long double f) {
 #ifdef __APPLE__
 inline int __fpclassify(long double d) {
   __CPROVER_HIDE:
-  return __CPROVER_fpclassify(
-    FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, d);
+    return __CPROVER_fpclassify(
+      FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, d);
 }
 #else
 inline int __fpclassify(double d) {
   __CPROVER_HIDE:
-  return __CPROVER_fpclassify(
-    FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, d);
+    return __CPROVER_fpclassify(
+      FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, d);
 }
 #endif