Skip to content

Commit fd07bb3

Browse files
tautschnigtautschnig
committed
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.
1 parent 6153505 commit fd07bb3

File tree

1 file changed

+105
-0
lines changed

1 file changed

+105
-0
lines changed

‎src/ansi-c/library/math.c

Lines changed: 105 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -220,21 +220,30 @@ int __isnormalf(float f)
220220

221221
float __builtin_inff(void)
222222
{
223+
#pragma CPROVER check push
224+
#pragma CPROVER check disable "div-by-zero"
223225
return 1.0f / 0.0f;
226+
#pragma CPROVER check pop
224227
}
225228

226229
/* FUNCTION: __builtin_inf */
227230

228231
double __builtin_inf(void)
229232
{
233+
#pragma CPROVER check push
234+
#pragma CPROVER check disable "div-by-zero"
230235
return 1.0 / 0.0;
236+
#pragma CPROVER check pop
231237
}
232238

233239
/* FUNCTION: __builtin_infl */
234240

235241
long double __builtin_infl(void)
236242
{
243+
#pragma CPROVER check push
244+
#pragma CPROVER check disable "div-by-zero"
237245
return 1.0l / 0.0l;
246+
#pragma CPROVER check pop
238247
}
239248

240249
/* FUNCTION: __builtin_isinf */
@@ -276,21 +285,30 @@ int __builtin_isnanf(float f)
276285

277286
float __builtin_huge_valf(void)
278287
{
288+
#pragma CPROVER check push
289+
#pragma CPROVER check disable "div-by-zero"
279290
return 1.0f / 0.0f;
291+
#pragma CPROVER check pop
280292
}
281293

282294
/* FUNCTION: __builtin_huge_val */
283295

284296
double __builtin_huge_val(void)
285297
{
298+
#pragma CPROVER check push
299+
#pragma CPROVER check disable "div-by-zero"
286300
return 1.0 / 0.0;
301+
#pragma CPROVER check pop
287302
}
288303

289304
/* FUNCTION: __builtin_huge_vall */
290305

291306
long double __builtin_huge_vall(void)
292307
{
308+
#pragma CPROVER check push
309+
#pragma CPROVER check disable "div-by-zero"
293310
return 1.0l / 0.0l;
311+
#pragma CPROVER check pop
294312
}
295313

296314
/* FUNCTION: _dsign */
@@ -597,7 +615,10 @@ double __builtin_nan(const char *str)
597615
// the 'str' argument is not yet used
598616
__CPROVER_hide:;
599617
(void)*str;
618+
#pragma CPROVER check push
619+
#pragma CPROVER check disable "div-by-zero"
600620
return 0.0/0.0;
621+
#pragma CPROVER check pop
601622
}
602623

603624
/* FUNCTION: __builtin_nanf */
@@ -607,7 +628,10 @@ float __builtin_nanf(const char *str)
607628
// the 'str' argument is not yet used
608629
__CPROVER_hide:;
609630
(void)*str;
631+
#pragma CPROVER check push
632+
#pragma CPROVER check disable "div-by-zero"
610633
return 0.0f/0.0f;
634+
#pragma CPROVER check pop
611635
}
612636

613637

@@ -630,7 +654,10 @@ double nan(const char *str) {
630654
// the 'str' argument is not yet used
631655
__CPROVER_hide:;
632656
(void)*str;
657+
#pragma CPROVER check push
658+
#pragma CPROVER check disable "div-by-zero"
633659
return 0.0/0.0;
660+
#pragma CPROVER check pop
634661
}
635662

636663
/* FUNCTION: nanf */
@@ -639,7 +666,10 @@ float nanf(const char *str) {
639666
// the 'str' argument is not yet used
640667
__CPROVER_hide:;
641668
(void)*str;
669+
#pragma CPROVER check push
670+
#pragma CPROVER check disable "div-by-zero"
642671
return 0.0f/0.0f;
672+
#pragma CPROVER check pop
643673
}
644674

645675
/* FUNCTION: nanl */
@@ -648,7 +678,10 @@ long double nanl(const char *str) {
648678
// the 'str' argument is not yet used
649679
__CPROVER_hide:;
650680
(void)*str;
681+
#pragma CPROVER check push
682+
#pragma CPROVER check disable "div-by-zero"
651683
return 0.0/0.0;
684+
#pragma CPROVER check pop
652685
}
653686

654687
/* FUNCTION: nextUpf */
@@ -676,7 +709,10 @@ float nextUpf(float f)
676709
{
677710
__CPROVER_hide:;
678711
if (__CPROVER_isnanf(f))
712+
#pragma CPROVER check push
713+
#pragma CPROVER check disable "div-by-zero"
679714
return 0.0f/0.0f; // NaN
715+
#pragma CPROVER check pop
680716
else if (f == 0.0f)
681717
return 0x1p-149f;
682718
else if (f > 0.0f)
@@ -725,7 +761,10 @@ double nextUp(double d)
725761
{
726762
__CPROVER_hide:;
727763
if (__CPROVER_isnand(d))
764+
#pragma CPROVER check push
765+
#pragma CPROVER check disable "div-by-zero"
728766
return 0.0/0.0; // NaN
767+
#pragma CPROVER check pop
729768
else if (d == 0.0)
730769
return 0x1.0p-1074;
731770
else if (d > 0.0)
@@ -773,7 +812,10 @@ long double nextUpl(long double d)
773812
{
774813
__CPROVER_hide:;
775814
if(__CPROVER_isnanld(d))
815+
#pragma CPROVER check push
816+
#pragma CPROVER check disable "div-by-zero"
776817
return 0.0/0.0; // NaN
818+
#pragma CPROVER check pop
777819
else if (d == 0.0)
778820
{
779821
union mixl m;
@@ -840,7 +882,10 @@ float sqrtf(float f)
840882
__CPROVER_hide:;
841883

842884
if ( f < 0.0f )
885+
#pragma CPROVER check push
886+
#pragma CPROVER check disable "div-by-zero"
843887
return 0.0f/0.0f; // NaN
888+
#pragma CPROVER check pop
844889
else if (__CPROVER_isinff(f) || // +Inf only
845890
f == 0.0f || // Includes -0
846891
__CPROVER_isnanf(f))
@@ -927,7 +972,10 @@ double sqrt(double d)
927972
__CPROVER_hide:;
928973

929974
if ( d < 0.0 )
975+
#pragma CPROVER check push
976+
#pragma CPROVER check disable "div-by-zero"
930977
return 0.0/0.0; // NaN
978+
#pragma CPROVER check pop
931979
else if (__CPROVER_isinfd(d) || // +Inf only
932980
d == 0.0 || // Includes -0
933981
__CPROVER_isnand(d))
@@ -998,7 +1046,10 @@ long double sqrtl(long double d)
9981046
__CPROVER_hide:;
9991047

10001048
if(d < 0.0l)
1049+
#pragma CPROVER check push
1050+
#pragma CPROVER check disable "div-by-zero"
10011051
return 0.0l/0.0l; // NaN
1052+
#pragma CPROVER check pop
10021053
else if (__CPROVER_isinfld(d) || // +Inf only
10031054
d == 0.0l || // Includes -0
10041055
__CPROVER_isnanld(d))
@@ -2700,7 +2751,10 @@ double log(double x)
27002751
else if(__CPROVER_signd(x))
27012752
{
27022753
errno = EDOM;
2754+
#pragma CPROVER check push
2755+
#pragma CPROVER check disable "div-by-zero"
27032756
return 0.0 / 0.0;
2757+
#pragma CPROVER check pop
27042758
}
27052759

27062760
_Static_assert(
@@ -2758,7 +2812,10 @@ float logf(float x)
27582812
else if(__CPROVER_signf(x))
27592813
{
27602814
errno = EDOM;
2815+
#pragma CPROVER check push
2816+
#pragma CPROVER check disable "div-by-zero"
27612817
return 0.0f / 0.0f;
2818+
#pragma CPROVER check pop
27622819
}
27632820

27642821
_Static_assert(
@@ -2817,7 +2874,10 @@ long double logl(long double x)
28172874
else if(__CPROVER_signld(x))
28182875
{
28192876
errno = EDOM;
2877+
#pragma CPROVER check push
2878+
#pragma CPROVER check disable "div-by-zero"
28202879
return 0.0l / 0.0l;
2880+
#pragma CPROVER check pop
28212881
}
28222882

28232883
#if LDBL_MAX_EXP == DBL_MAX_EXP
@@ -2881,7 +2941,10 @@ double log2(double x)
28812941
else if(__CPROVER_signd(x))
28822942
{
28832943
errno = EDOM;
2944+
#pragma CPROVER check push
2945+
#pragma CPROVER check disable "div-by-zero"
28842946
return 0.0 / 0.0;
2947+
#pragma CPROVER check pop
28852948
}
28862949

28872950
_Static_assert(
@@ -2938,7 +3001,10 @@ float log2f(float x)
29383001
else if(__CPROVER_signf(x))
29393002
{
29403003
errno = EDOM;
3004+
#pragma CPROVER check push
3005+
#pragma CPROVER check disable "div-by-zero"
29413006
return 0.0f / 0.0f;
3007+
#pragma CPROVER check pop
29423008
}
29433009

29443010
_Static_assert(
@@ -2996,7 +3062,10 @@ long double log2l(long double x)
29963062
else if(__CPROVER_signld(x))
29973063
{
29983064
errno = EDOM;
3065+
#pragma CPROVER check push
3066+
#pragma CPROVER check disable "div-by-zero"
29993067
return 0.0l / 0.0l;
3068+
#pragma CPROVER check pop
30003069
}
30013070

30023071
#if LDBL_MAX_EXP == DBL_MAX_EXP
@@ -3060,7 +3129,10 @@ double log10(double x)
30603129
else if(__CPROVER_signd(x))
30613130
{
30623131
errno = EDOM;
3132+
#pragma CPROVER check push
3133+
#pragma CPROVER check disable "div-by-zero"
30633134
return 0.0 / 0.0;
3135+
#pragma CPROVER check pop
30643136
}
30653137

30663138
_Static_assert(
@@ -3120,7 +3192,10 @@ float log10f(float x)
31203192
else if(__CPROVER_signf(x))
31213193
{
31223194
errno = EDOM;
3195+
#pragma CPROVER check push
3196+
#pragma CPROVER check disable "div-by-zero"
31233197
return 0.0f / 0.0f;
3198+
#pragma CPROVER check pop
31243199
}
31253200

31263201
_Static_assert(
@@ -3180,7 +3255,10 @@ long double log10l(long double x)
31803255
else if(__CPROVER_signld(x))
31813256
{
31823257
errno = EDOM;
3258+
#pragma CPROVER check push
3259+
#pragma CPROVER check disable "div-by-zero"
31833260
return 0.0l / 0.0l;
3261+
#pragma CPROVER check pop
31843262
}
31853263

31863264
#if LDBL_MAX_EXP == DBL_MAX_EXP
@@ -3237,7 +3315,10 @@ double pow(double x, double y)
32373315
nearbyint(y) != y)
32383316
{
32393317
errno = EDOM;
3318+
#pragma CPROVER check push
3319+
#pragma CPROVER check disable "div-by-zero"
32403320
return 0.0 / 0.0;
3321+
#pragma CPROVER check pop
32413322
}
32423323
else if(x == 1.0)
32433324
return 1.0;
@@ -3303,7 +3384,10 @@ double pow(double x, double y)
33033384
return HUGE_VAL;
33043385
}
33053386
else if(isnan(x) || isnan(y))
3387+
#pragma CPROVER check push
3388+
#pragma CPROVER check disable "div-by-zero"
33063389
return 0.0 / 0.0;
3390+
#pragma CPROVER check pop
33073391

33083392
_Static_assert(
33093393
sizeof(double) == 2 * sizeof(int32_t),
@@ -3366,7 +3450,10 @@ float powf(float x, float y)
33663450
nearbyintf(y) != y)
33673451
{
33683452
errno = EDOM;
3453+
#pragma CPROVER check push
3454+
#pragma CPROVER check disable "div-by-zero"
33693455
return 0.0f / 0.0f;
3456+
#pragma CPROVER check pop
33703457
}
33713458
else if(x == 1.0f)
33723459
return 1.0f;
@@ -3435,7 +3522,10 @@ float powf(float x, float y)
34353522
return HUGE_VALF;
34363523
}
34373524
else if(isnanf(x) || isnanf(y))
3525+
#pragma CPROVER check push
3526+
#pragma CPROVER check disable "div-by-zero"
34383527
return 0.0f / 0.0f;
3528+
#pragma CPROVER check pop
34393529

34403530
_Static_assert(
34413531
sizeof(float) == sizeof(int32_t),
@@ -3492,7 +3582,10 @@ long double powl(long double x, long double y)
34923582
nearbyintl(y) != y)
34933583
{
34943584
errno = EDOM;
3585+
#pragma CPROVER check push
3586+
#pragma CPROVER check disable "div-by-zero"
34953587
return 0.0l / 0.0l;
3588+
#pragma CPROVER check pop
34963589
}
34973590
else if(x == 1.0l)
34983591
return 1.0l;
@@ -3562,7 +3655,10 @@ long double powl(long double x, long double y)
35623655
return HUGE_VALL;
35633656
}
35643657
else if(isnanl(x) || isnanl(y))
3658+
#pragma CPROVER check push
3659+
#pragma CPROVER check disable "div-by-zero"
35653660
return 0.0l / 0.0l;
3661+
#pragma CPROVER check pop
35663662

35673663
#if LDBL_MAX_EXP == DBL_MAX_EXP
35683664
return pow(x, y);
@@ -3617,6 +3713,8 @@ double __builtin_inf(void);
36173713
double fma(double x, double y, double z)
36183714
{
36193715
// see man fma (https://linux.die.net/man/3/fma)
3716+
#pragma CPROVER check push
3717+
#pragma CPROVER check disable "div-by-zero"
36203718
if(isnan(x) || isnan(y))
36213719
return 0.0 / 0.0;
36223720
else if(
@@ -3637,6 +3735,7 @@ double fma(double x, double y, double z)
36373735
feraiseexcept(FE_INVALID);
36383736
return 0.0 / 0.0;
36393737
}
3738+
#pragma CPROVER check pop
36403739

36413740
// TODO: detect overflow (FE_OVERFLOW), return +/- __builtin_inf()
36423741
// TODO: detect underflow (FE_UNDERFLOW), return +/- 0
@@ -3660,6 +3759,8 @@ float __builtin_inff(void);
36603759
float fmaf(float x, float y, float z)
36613760
{
36623761
// see man fma (https://linux.die.net/man/3/fma)
3762+
#pragma CPROVER check push
3763+
#pragma CPROVER check disable "div-by-zero"
36633764
if(isnanf(x) || isnanf(y))
36643765
return 0.0f / 0.0f;
36653766
else if(
@@ -3680,6 +3781,7 @@ float fmaf(float x, float y, float z)
36803781
feraiseexcept(FE_INVALID);
36813782
return 0.0f / 0.0f;
36823783
}
3784+
#pragma CPROVER check pop
36833785

36843786
// TODO: detect overflow (FE_OVERFLOW), return +/- __builtin_inff()
36853787
// TODO: detect underflow (FE_UNDERFLOW), return +/- 0
@@ -3708,6 +3810,8 @@ long double __builtin_infl(void);
37083810
long double fmal(long double x, long double y, long double z)
37093811
{
37103812
// see man fma (https://linux.die.net/man/3/fma)
3813+
#pragma CPROVER check push
3814+
#pragma CPROVER check disable "div-by-zero"
37113815
if(isnanl(x) || isnanl(y))
37123816
return 0.0l / 0.0l;
37133817
else if(
@@ -3728,6 +3832,7 @@ long double fmal(long double x, long double y, long double z)
37283832
feraiseexcept(FE_INVALID);
37293833
return 0.0l / 0.0l;
37303834
}
3835+
#pragma CPROVER check pop
37313836

37323837
#if LDBL_MAX_EXP == DBL_MAX_EXP
37333838
return fma(x, y, z);

0 commit comments

Comments
 (0)