Merge pull request #8775 from tautschnig/fix-8710-builtin_inff

C front-end: recognize __builtin_inff() as constant expression

Author: kroening

regression/cbmc-library/__builtin_inf-01/main.c

@@ -0,0 +1,42 @@
+#include <assert.h>
+#include <math.h>
+
+float g = -INFINITY;
+
+void test_static_float_infinity()
+{
+  static float f = +INFINITY;
+  assert(isinf(f));
+}
+
+void test_static_double_infinity()
+{
+  static double d = INFINITY;
+  assert(isinf(d));
+}
+
+void test_static_long_double_infinity()
+{
+  static long double ld = INFINITY;
+  assert(isinf(ld));
+}
+
+void test_static_huge_val()
+{
+  static float f = HUGE_VALF;
+  static double d = HUGE_VAL;
+  static long double ld = HUGE_VALL;
+
+  assert(isinf(f));
+  assert(isinf(d));
+  assert(isinf(ld));
+}
+
+int main()
+{
+  test_static_float_infinity();
+  test_static_double_infinity();
+  test_static_long_double_infinity();
+  test_static_huge_val();
+  return 0;
+}

regression/cbmc-library/__builtin_inff-01/main.c

@@ -1,6 +1,6 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
+CORE
+static_init.c
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-library/__builtin_inff-01/test.desc

@@ -3265,8 +3265,9 @@ exprt c_typecheck_baset::do_special_functions(
 
     return typecast_exprt::conditional_cast(isfinite_expr, expr.type());
   }
-  else if(identifier==CPROVER_PREFIX "inf" ||
-          identifier=="__builtin_inf")
+  else if(
+    identifier == CPROVER_PREFIX "inf" || identifier == "__builtin_inf" ||
+    identifier == "__builtin_huge_val")
   {
     constant_exprt inf_expr=
       ieee_floatt::plus_infinity(
@@ -3275,7 +3276,9 @@ exprt c_typecheck_baset::do_special_functions(
 
     return std::move(inf_expr);
   }
-  else if(identifier==CPROVER_PREFIX "inff")
+  else if(
+    identifier == CPROVER_PREFIX "inff" || identifier == "__builtin_inff" ||
+    identifier == "__builtin_huge_valf")
   {
     constant_exprt inff_expr=
       ieee_floatt::plus_infinity(
@@ -3284,7 +3287,9 @@ exprt c_typecheck_baset::do_special_functions(
 
     return std::move(inff_expr);
   }
-  else if(identifier==CPROVER_PREFIX "infl")
+  else if(
+    identifier == CPROVER_PREFIX "infl" || identifier == "__builtin_infl" ||
+    identifier == "__builtin_huge_vall")
   {
     floatbv_typet type=to_floatbv_type(long_double_type());
     constant_exprt infl_expr=

regression/cbmc-library/__builtin_infl-01/main.c

@@ -216,39 +216,6 @@ int __isnormalf(float f)
   return __CPROVER_isnormalf(f);
 }
 
-/* FUNCTION: __builtin_inff */
-
-float __builtin_inff(void)
-{
-#pragma CPROVER check push
-#pragma CPROVER check disable "float-div-by-zero"
-#pragma CPROVER check disable "float-overflow"
-  return 1.0f / 0.0f;
-#pragma CPROVER check pop
-}
-
-/* FUNCTION: __builtin_inf */
-
-double __builtin_inf(void)
-{
-#pragma CPROVER check push
-#pragma CPROVER check disable "float-div-by-zero"
-#pragma CPROVER check disable "float-overflow"
-  return 1.0 / 0.0;
-#pragma CPROVER check pop
-}
-
-/* FUNCTION: __builtin_infl */
-
-long double __builtin_infl(void)
-{
-#pragma CPROVER check push
-#pragma CPROVER check disable "float-div-by-zero"
-#pragma CPROVER check disable "float-overflow"
-  return 1.0l / 0.0l;
-#pragma CPROVER check pop
-}
-
 /* FUNCTION: __builtin_isinf */
 
 int __builtin_isinf(double d)