fixup #8538 -- correct rounding modes for floor, trunc

kroening · kroening · commit 177f33b408fa · 2025-02-20T10:28:38.000Z
This fixes the rounding modes used for the floor and trunc C library functions.
diff --git a/regression/cbmc-library/floor-01/main.c b/regression/cbmc-library/floor-01/main.c
@@ -3,7 +3,10 @@
 
 int main()
 {
-  floor();
-  assert(0);
+  assert(floor(1.1)==1.0);
+  assert(floor(1.9)==1.0);
+  assert(floor(-1.1)==-2.0);
+  assert(floor(-1.9)==-2.0);
+  assert(signbit(floor(-0.0)));
   return 0;
 }
diff --git a/regression/cbmc-library/floor-01/test.desc b/regression/cbmc-library/floor-01/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/floorf-01/main.c b/regression/cbmc-library/floorf-01/main.c
@@ -3,7 +3,10 @@
 
 int main()
 {
-  floorf();
-  assert(0);
+  assert(floorf(1.1f)==1.0f);
+  assert(floorf(1.9f)==1.0f);
+  assert(floorf(-1.1f)==-2.0f);
+  assert(floorf(-1.9f)==-2.0f);
+  assert(signbit(floorf(-0.0f)));
   return 0;
 }
diff --git a/regression/cbmc-library/floorf-01/test.desc b/regression/cbmc-library/floorf-01/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/floorl-01/main.c b/regression/cbmc-library/floorl-01/main.c
@@ -3,7 +3,10 @@
 
 int main()
 {
-  floorl();
-  assert(0);
+  assert(floorl(1.1l)==1.0l);
+  assert(floorl(1.9l)==1.0l);
+  assert(floorl(-1.1l)==-2.0l);
+  assert(floorl(-1.9l)==-2.0l);
+  assert(signbit(floorl(-0.0l)));
   return 0;
 }
diff --git a/regression/cbmc-library/floorl-01/test.desc b/regression/cbmc-library/floorl-01/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/round-01/main.c b/regression/cbmc-library/round-01/main.c
@@ -3,7 +3,12 @@
 
 int main()
 {
-  round();
-  assert(0);
+  assert(round(1.1)==1.0);
+  assert(round(1.5)==2.0);
+  assert(round(1.9)==2.0);
+  assert(round(-1.1)==-1.0);
+  assert(round(-1.5)==-2.0);
+  assert(round(-1.9)==-2.0);
+  assert(signbit(round(-0.0)));
   return 0;
 }
diff --git a/regression/cbmc-library/round-01/test.desc b/regression/cbmc-library/round-01/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/roundf-01/main.c b/regression/cbmc-library/roundf-01/main.c
@@ -3,7 +3,12 @@
 
 int main()
 {
-  roundf();
-  assert(0);
+  assert(roundf(1.1f)==1.0f);
+  assert(roundf(1.5f)==2.0f);
+  assert(roundf(1.9f)==2.0f);
+  assert(roundf(-1.1f)==-1.0f);
+  assert(roundf(-1.5f)==-2.0f);
+  assert(roundf(-1.9f)==-2.0f);
+  assert(signbit(roundf(-0.0f)));
   return 0;
 }
diff --git a/regression/cbmc-library/roundf-01/test.desc b/regression/cbmc-library/roundf-01/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/roundl-01/main.c b/regression/cbmc-library/roundl-01/main.c
@@ -3,7 +3,12 @@
 
 int main()
 {
-  roundl();
-  assert(0);
+  assert(roundl(1.1l)==1.0l);
+  assert(roundl(1.5l)==2.0l);
+  assert(roundl(1.9l)==2.0l);
+  assert(roundl(-1.1l)==-1.0l);
+  assert(roundl(-1.5l)==-2.0l);
+  assert(roundl(-1.9l)==-2.0l);
+  assert(signbit(roundl(-0.0l)));
   return 0;
 }
diff --git a/regression/cbmc-library/roundl-01/test.desc b/regression/cbmc-library/roundl-01/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/trunc-01/main.c b/regression/cbmc-library/trunc-01/main.c
@@ -3,7 +3,10 @@
 
 int main()
 {
-  trunc();
-  assert(0);
+  assert(trunc(1.1)==1.0);
+  assert(trunc(1.9)==1.0);
+  assert(trunc(-1.1)==-1.0);
+  assert(trunc(-1.9)==-1.0);
+  assert(signbit(trunc(-0.0)));
   return 0;
 }
diff --git a/regression/cbmc-library/trunc-01/test.desc b/regression/cbmc-library/trunc-01/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/truncf-01/main.c b/regression/cbmc-library/truncf-01/main.c
@@ -3,7 +3,10 @@
 
 int main()
 {
-  truncf();
-  assert(0);
+  assert(truncf(1.1f)==1.0f);
+  assert(truncf(1.9f)==1.0f);
+  assert(truncf(-1.1f)==-1.0f);
+  assert(truncf(-1.9f)==-1.0f);
+  assert(signbit(trunc(-0.0f)));
   return 0;
 }
diff --git a/regression/cbmc-library/truncf-01/test.desc b/regression/cbmc-library/truncf-01/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/truncl-01/main.c b/regression/cbmc-library/truncl-01/main.c
@@ -3,7 +3,10 @@
 
 int main()
 {
-  truncl();
-  assert(0);
+  assert(truncl(1.1l)==1.0l);
+  assert(truncl(1.9l)==1.0l);
+  assert(truncl(-1.1l)==-1.0l);
+  assert(truncl(-1.9l)==-1.0l);
+  assert(signbit(truncl(-0.0l)));
   return 0;
 }
diff --git a/regression/cbmc-library/truncl-01/test.desc b/regression/cbmc-library/truncl-01/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c
@@ -1322,7 +1322,7 @@ long double ceill(long double x)
 
 double floor(double x)
 {
-  return __CPROVER_round_to_integrald(x, 3); // FE_DOWNWARD
+  return __CPROVER_round_to_integrald(x, 1); // FE_DOWNWARD
 }
 
 /* FUNCTION: floorf */
@@ -1339,7 +1339,7 @@ double floor(double x)
 
 float floorf(float x)
 {
-  return __CPROVER_round_to_integralf(x, 3); // FE_DOWNWARD
+  return __CPROVER_round_to_integralf(x, 1); // FE_DOWNWARD
 }
 
 
@@ -1357,7 +1357,7 @@ float floorf(float x)
 
 long double floorl(long double x)
 {
-  return __CPROVER_round_to_integralld(x, 3); // FE_DOWNWARD
+  return __CPROVER_round_to_integralld(x, 1); // FE_DOWNWARD
 }
 
 
@@ -1381,7 +1381,7 @@ long double floorl(long double x)
 
 double trunc(double x)
 {
-  return __CPROVER_round_to_integrald(x, 0); // FE_TOWARDZERO
+  return __CPROVER_round_to_integrald(x, 3); // FE_TOWARDZERO
 }
 
 /* FUNCTION: truncf */
@@ -1398,7 +1398,7 @@ double trunc(double x)
 
 float truncf(float x)
 {
-  return __CPROVER_round_to_integralf(x, 0); // FE_TOWARDZERO
+  return __CPROVER_round_to_integralf(x, 3); // FE_TOWARDZERO
 }
 
 
@@ -1416,7 +1416,7 @@ float truncf(float x)
 
 long double truncl(long double x)
 {
-  return __CPROVER_round_to_integralld(x, 0); // FE_TOWARDZERO
+  return __CPROVER_round_to_integralld(x, 3); // FE_TOWARDZERO
 }
 
 
@@ -1889,7 +1889,7 @@ long long int llroundl(long double x)
 
 double modf(double x, double *iptr)
 {
-  *iptr = __CPROVER_round_to_integrald(x, 0); // FE_TOWARDZERO
+  *iptr = __CPROVER_round_to_integrald(x, 3); // FE_TOWARDZERO
   return (x - *iptr);
 }
 
@@ -1907,7 +1907,7 @@ double modf(double x, double *iptr)
 
 float modff(float x, float *iptr)
 {
-  *iptr = __CPROVER_round_to_integralf(x, 0); // FE_TOWARDZERO
+  *iptr = __CPROVER_round_to_integralf(x, 3); // FE_TOWARDZERO
   return (x - *iptr);
 }
 
@@ -1926,7 +1926,7 @@ float modff(float x, float *iptr)
 
 long double modfl(long double x, long double *iptr)
 {
-  *iptr = __CPROVER_round_to_integralld(x, 0); // FE_TOWARDZERO
+  *iptr = __CPROVER_round_to_integralld(x, 3); // FE_TOWARDZERO
   return (x - *iptr);
 }
 

Original file line number	Diff line number	Diff line change
`@@ -3,7 +3,10 @@`
`3`	`3`
`4`	`4`	`int main()`
`5`	`5`	`{`
`6`		`- floor();`
`7`		`- assert(0);`
	`6`	`+ assert(floor(1.1)==1.0);`
	`7`	`+ assert(floor(1.9)==1.0);`
	`8`	`+ assert(floor(-1.1)==-2.0);`
	`9`	`+ assert(floor(-1.9)==-2.0);`
	`10`	`+ assert(signbit(floor(-0.0)));`
`8`	`11`	`return 0;`
`9`	`12`	`}`
Original file line number	Diff line number	Diff line change
`@@ -3,7 +3,10 @@`
`3`	`3`
`4`	`4`	`int main()`
`5`	`5`	`{`
`6`		`- floorf();`
`7`		`- assert(0);`
	`6`	`+ assert(floorf(1.1f)==1.0f);`
	`7`	`+ assert(floorf(1.9f)==1.0f);`
	`8`	`+ assert(floorf(-1.1f)==-2.0f);`
	`9`	`+ assert(floorf(-1.9f)==-2.0f);`
	`10`	`+ assert(signbit(floorf(-0.0f)));`
`8`	`11`	`return 0;`
`9`	`12`	`}`
Original file line number	Diff line number	Diff line change
`@@ -3,7 +3,10 @@`
`3`	`3`
`4`	`4`	`int main()`
`5`	`5`	`{`
`6`		`- floorl();`
`7`		`- assert(0);`
	`6`	`+ assert(floorl(1.1l)==1.0l);`
	`7`	`+ assert(floorl(1.9l)==1.0l);`
	`8`	`+ assert(floorl(-1.1l)==-2.0l);`
	`9`	`+ assert(floorl(-1.9l)==-2.0l);`
	`10`	`+ assert(signbit(floorl(-0.0l)));`
`8`	`11`	`return 0;`
`9`	`12`	`}`
Original file line number	Diff line number	Diff line change
`@@ -3,7 +3,12 @@`
`3`	`3`
`4`	`4`	`int main()`
`5`	`5`	`{`
`6`		`- round();`
`7`		`- assert(0);`
	`6`	`+ assert(round(1.1)==1.0);`
	`7`	`+ assert(round(1.5)==2.0);`
	`8`	`+ assert(round(1.9)==2.0);`
	`9`	`+ assert(round(-1.1)==-1.0);`
	`10`	`+ assert(round(-1.5)==-2.0);`
	`11`	`+ assert(round(-1.9)==-2.0);`
	`12`	`+ assert(signbit(round(-0.0)));`
`8`	`13`	`return 0;`
`9`	`14`	`}`
Original file line number	Diff line number	Diff line change
`@@ -3,7 +3,12 @@`
`3`	`3`
`4`	`4`	`int main()`
`5`	`5`	`{`
`6`		`- roundf();`
`7`		`- assert(0);`
	`6`	`+ assert(roundf(1.1f)==1.0f);`
	`7`	`+ assert(roundf(1.5f)==2.0f);`
	`8`	`+ assert(roundf(1.9f)==2.0f);`
	`9`	`+ assert(roundf(-1.1f)==-1.0f);`
	`10`	`+ assert(roundf(-1.5f)==-2.0f);`
	`11`	`+ assert(roundf(-1.9f)==-2.0f);`
	`12`	`+ assert(signbit(roundf(-0.0f)));`
`8`	`13`	`return 0;`
`9`	`14`	`}`