C library: do not flag division-by-zero when building NaN

We construct NaN (and Inf) by dividing by zero, which is a standards-compliant way in that Nan (Inf) is the correct result for these cases. Do not flag these operations as division-by-zero, which the user would not expect.
diffblue · Feb 7, 2024 · fd07bb3 · fd07bb3
1 parent 6153505
commit fd07bb3
Showing 1 changed file with 105 additions and 0 deletions.
diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c
@@ -220,21 +220,30 @@ int __isnormalf(float f)
 
 float __builtin_inff(void)
 {
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
   return 1.0f / 0.0f;
+#pragma CPROVER check pop
 }
 
 /* FUNCTION: __builtin_inf */
 
 double __builtin_inf(void)
 {
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
   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 "div-by-zero"
   return 1.0l / 0.0l;
+#pragma CPROVER check pop
 }
 
 /* FUNCTION: __builtin_isinf */
@@ -276,21 +285,30 @@ int __builtin_isnanf(float f)
 
 float __builtin_huge_valf(void)
 {
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
   return 1.0f / 0.0f;
+#pragma CPROVER check pop
 }
 
 /* FUNCTION: __builtin_huge_val */
 
 double __builtin_huge_val(void)
 {
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
   return 1.0 / 0.0;
+#pragma CPROVER check pop
 }
 
 /* FUNCTION: __builtin_huge_vall */
 
 long double __builtin_huge_vall(void)
 {
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
   return 1.0l / 0.0l;
+#pragma CPROVER check pop
 }
 
 /* FUNCTION: _dsign */
@@ -597,7 +615,10 @@ double __builtin_nan(const char *str)
   // the 'str' argument is not yet used
 __CPROVER_hide:;
   (void)*str;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
   return 0.0/0.0;
+#pragma CPROVER check pop
 }
 
 /* FUNCTION: __builtin_nanf */
@@ -607,7 +628,10 @@ float __builtin_nanf(const char *str)
   // the 'str' argument is not yet used
 __CPROVER_hide:;
   (void)*str;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
   return 0.0f/0.0f;
+#pragma CPROVER check pop
 }
 
 
@@ -630,7 +654,10 @@ double nan(const char *str) {
   // the 'str' argument is not yet used
  __CPROVER_hide:;
   (void)*str;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
   return 0.0/0.0;
+#pragma CPROVER check pop
 }
 
 /* FUNCTION: nanf */
@@ -639,7 +666,10 @@ float nanf(const char *str) {
   // the 'str' argument is not yet used
  __CPROVER_hide:;
   (void)*str;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
   return 0.0f/0.0f;
+#pragma CPROVER check pop
 }
 
 /* FUNCTION: nanl */
@@ -648,7 +678,10 @@ long double nanl(const char *str) {
   // the 'str' argument is not yet used
  __CPROVER_hide:;
   (void)*str;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
   return 0.0/0.0;
+#pragma CPROVER check pop
 }
 
 /* FUNCTION: nextUpf */
@@ -676,7 +709,10 @@ float nextUpf(float f)
 {
 __CPROVER_hide:;
   if (__CPROVER_isnanf(f))
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0f/0.0f;  // NaN
+#pragma CPROVER check pop
   else if (f == 0.0f)
     return 0x1p-149f;
   else if (f > 0.0f)
@@ -725,7 +761,10 @@ double nextUp(double d)
 {
 __CPROVER_hide:;
   if (__CPROVER_isnand(d))
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0/0.0;  // NaN
+#pragma CPROVER check pop
   else if (d == 0.0)
     return 0x1.0p-1074;
   else if (d > 0.0)
@@ -773,7 +812,10 @@ long double nextUpl(long double d)
 {
 __CPROVER_hide:;
   if(__CPROVER_isnanld(d))
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0/0.0;  // NaN
+#pragma CPROVER check pop
   else if (d == 0.0)
   {
     union mixl m;
@@ -840,7 +882,10 @@ float sqrtf(float f)
  __CPROVER_hide:;
 
   if ( f < 0.0f )
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0f/0.0f; // NaN
+#pragma CPROVER check pop
   else if (__CPROVER_isinff(f) ||   // +Inf only
            f == 0.0f          ||   // Includes -0
            __CPROVER_isnanf(f))
@@ -927,7 +972,10 @@ double sqrt(double d)
  __CPROVER_hide:;
 
   if ( d < 0.0 )
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0/0.0; // NaN
+#pragma CPROVER check pop
   else if (__CPROVER_isinfd(d) ||   // +Inf only
            d == 0.0            ||   // Includes -0
            __CPROVER_isnand(d))
@@ -998,7 +1046,10 @@ long double sqrtl(long double d)
  __CPROVER_hide:;
 
   if(d < 0.0l)
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0l/0.0l; // NaN
+#pragma CPROVER check pop
   else if (__CPROVER_isinfld(d) ||   // +Inf only
            d == 0.0l            ||   // Includes -0
            __CPROVER_isnanld(d))
@@ -2700,7 +2751,10 @@ double log(double x)
   else if(__CPROVER_signd(x))
   {
     errno = EDOM;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0 / 0.0;
+#pragma CPROVER check pop
   }
 
   _Static_assert(
@@ -2758,7 +2812,10 @@ float logf(float x)
   else if(__CPROVER_signf(x))
   {
     errno = EDOM;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0f / 0.0f;
+#pragma CPROVER check pop
   }
 
   _Static_assert(
@@ -2817,7 +2874,10 @@ long double logl(long double x)
   else if(__CPROVER_signld(x))
   {
     errno = EDOM;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0l / 0.0l;
+#pragma CPROVER check pop
   }
 
 #if LDBL_MAX_EXP == DBL_MAX_EXP
@@ -2881,7 +2941,10 @@ double log2(double x)
   else if(__CPROVER_signd(x))
   {
     errno = EDOM;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0 / 0.0;
+#pragma CPROVER check pop
   }
 
   _Static_assert(
@@ -2938,7 +3001,10 @@ float log2f(float x)
   else if(__CPROVER_signf(x))
   {
     errno = EDOM;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0f / 0.0f;
+#pragma CPROVER check pop
   }
 
   _Static_assert(
@@ -2996,7 +3062,10 @@ long double log2l(long double x)
   else if(__CPROVER_signld(x))
   {
     errno = EDOM;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0l / 0.0l;
+#pragma CPROVER check pop
   }
 
 #if LDBL_MAX_EXP == DBL_MAX_EXP
@@ -3060,7 +3129,10 @@ double log10(double x)
   else if(__CPROVER_signd(x))
   {
     errno = EDOM;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0 / 0.0;
+#pragma CPROVER check pop
   }
 
   _Static_assert(
@@ -3120,7 +3192,10 @@ float log10f(float x)
   else if(__CPROVER_signf(x))
   {
     errno = EDOM;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0f / 0.0f;
+#pragma CPROVER check pop
   }
 
   _Static_assert(
@@ -3180,7 +3255,10 @@ long double log10l(long double x)
   else if(__CPROVER_signld(x))
   {
     errno = EDOM;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0l / 0.0l;
+#pragma CPROVER check pop
   }
 
 #if LDBL_MAX_EXP == DBL_MAX_EXP
@@ -3237,7 +3315,10 @@ double pow(double x, double y)
     nearbyint(y) != y)
   {
     errno = EDOM;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0 / 0.0;
+#pragma CPROVER check pop
   }
   else if(x == 1.0)
     return 1.0;
@@ -3303,7 +3384,10 @@ double pow(double x, double y)
       return HUGE_VAL;
   }
   else if(isnan(x) || isnan(y))
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0 / 0.0;
+#pragma CPROVER check pop
 
   _Static_assert(
     sizeof(double) == 2 * sizeof(int32_t),
@@ -3366,7 +3450,10 @@ float powf(float x, float y)
     nearbyintf(y) != y)
   {
     errno = EDOM;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0f / 0.0f;
+#pragma CPROVER check pop
   }
   else if(x == 1.0f)
     return 1.0f;
@@ -3435,7 +3522,10 @@ float powf(float x, float y)
       return HUGE_VALF;
   }
   else if(isnanf(x) || isnanf(y))
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0f / 0.0f;
+#pragma CPROVER check pop
 
   _Static_assert(
     sizeof(float) == sizeof(int32_t),
@@ -3492,7 +3582,10 @@ long double powl(long double x, long double y)
     nearbyintl(y) != y)
   {
     errno = EDOM;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0l / 0.0l;
+#pragma CPROVER check pop
   }
   else if(x == 1.0l)
     return 1.0l;
@@ -3562,7 +3655,10 @@ long double powl(long double x, long double y)
       return HUGE_VALL;
   }
   else if(isnanl(x) || isnanl(y))
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0l / 0.0l;
+#pragma CPROVER check pop
 
 #if LDBL_MAX_EXP == DBL_MAX_EXP
   return pow(x, y);
@@ -3617,6 +3713,8 @@ double __builtin_inf(void);
 double fma(double x, double y, double z)
 {
   // see man fma (https://linux.die.net/man/3/fma)
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
   if(isnan(x) || isnan(y))
     return 0.0 / 0.0;
   else if(
@@ -3637,6 +3735,7 @@ double fma(double x, double y, double z)
     feraiseexcept(FE_INVALID);
     return 0.0 / 0.0;
   }
+#pragma CPROVER check pop
 
   // TODO: detect overflow (FE_OVERFLOW), return +/- __builtin_inf()
   // TODO: detect underflow (FE_UNDERFLOW), return +/- 0
@@ -3660,6 +3759,8 @@ float __builtin_inff(void);
 float fmaf(float x, float y, float z)
 {
   // see man fma (https://linux.die.net/man/3/fma)
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
   if(isnanf(x) || isnanf(y))
     return 0.0f / 0.0f;
   else if(
@@ -3680,6 +3781,7 @@ float fmaf(float x, float y, float z)
     feraiseexcept(FE_INVALID);
     return 0.0f / 0.0f;
   }
+#pragma CPROVER check pop
 
   // TODO: detect overflow (FE_OVERFLOW), return +/- __builtin_inff()
   // TODO: detect underflow (FE_UNDERFLOW), return +/- 0
@@ -3708,6 +3810,8 @@ long double __builtin_infl(void);
 long double fmal(long double x, long double y, long double z)
 {
   // see man fma (https://linux.die.net/man/3/fma)
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
   if(isnanl(x) || isnanl(y))
     return 0.0l / 0.0l;
   else if(
@@ -3728,6 +3832,7 @@ long double fmal(long double x, long double y, long double z)
     feraiseexcept(FE_INVALID);
     return 0.0l / 0.0l;
   }
+#pragma CPROVER check pop
 
 #if LDBL_MAX_EXP == DBL_MAX_EXP
   return fma(x, y, z);