Uh oh!
There was an error while loading. Please reload this page.
division-by-zero on float - #8233
Conversation
b4f949a to
2f2e163CompareCodecov ReportAll modified and coverable lines are covered by tests ✅
Additional details and impacted files@@ Coverage Diff @@## develop #8233 +/- ##
===========================================
- Coverage 79.64% 79.64% -0.01%
===========================================
Files 1684 1684 Lines 195670 195684 +14 ===========================================
+ Hits 155841 155852 +11 - Misses 39829 39832 +3 ☔ View full report in Codecov by Sentry. |
e3f0ba9 to
16ea284Compare| #pragma CPROVER check push | ||
| #pragma CPROVER check disable "bounds" | ||
| #pragma CPROVER check disable "pointer" | ||
| #pragma CPROVER check disable "div-by-zero" |
There was a problem hiding this comment.
This regression test is called "...enable_all," so shouldn't the new check be enabled in addition rather than replace an existing one?
There was a problem hiding this comment.
There isn't any integer division, so that wouldn't have any effect.
There was a problem hiding this comment.
Ah, but then this test should be extended to have one (the test is "enable_all", so we should be testing all of them).
| #pragma CPROVER check push | ||
| #pragma CPROVER check disable "bounds" | ||
| #pragma CPROVER check disable "pointer" | ||
| #pragma CPROVER check disable "div-by-zero" |
There was a problem hiding this comment.
Ah, but then this test should be extended to have one (the test is "enable_all", so we should be testing all of them).
16ea284 to
ffaf0eeComparekroening
commented
Mar 22, 2024
Test extended by adding an integer division by zero. |
This separates the division-by-zero check for floating-point operations from the division-by-zero check for integers. The new division-by-zero check for floating-point operations is off by default, and is enabled by --float-div-by-zero-check. The case for doing so is weak. ISO/IEC 9899:2021 (C21) and predecessors clealy state (Sec 6.5.5 par 5) "In both operations, if the value of the second operand is zero, the behavior is undefined." However, Annex F (IEC 60559 floating-point arithmetic) states that implementations that define __STDC_IEC_559__ must implement IEC 60559 division, which clearly defines the behavior when dividing floating-point numbers by zero. This behavior can be observed on all architectures that we support.
ffaf0ee to
e00a1bdCompare
This separates the division-by-zero check for floating-point operations from the division-by-zero check for integers. The new division-by-zero check for floating-point operations is off by default, and is enabled by
--float-div-by-zero-check.The case for doing so is weak. ISO/IEC 9899:2021 (C21) and predecessors clealy state (Sec 6.5.5 par 5) "In both operations, if the value of the second operand is zero, the behavior is undefined."
However, Annex F (IEC 60559 floating-point arithmetic) states that implementations that define
__STDC_IEC_559__must implement IEC 60559 division, which clearly defines the behavior when dividing floating-point numbers by zero. This behavior can be observed on all architectures that we support.