Repository navigation
Regression test for double rounding carrying out of the significand - #9223
Merged
tautschnig merged 1 commit intoNov 6, 2026
Merged
Conversation
tautschnig
requested review from
kroening,
martin-cs and
peterschrammel
as code owners
October 20, 2026 19:38
There was a problem hiding this comment.
Copilot was unable to review this pull request because the user who requested the review has reached their quota limit.
An organization owner can choose the repository organization as the billing source for reviews requested by members with a paid Copilot license. Learn about Copilot code review billing. Review the Copilot code review billing settings.
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #9223 +/- ##
========================================
Coverage 80.93% 80.93%
========================================
Files 1719 1719
Lines 190345 190345
Branches 73 73
========================================
Hits 154052 154052
Misses 36293 36293 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
kroening
approved these changes
Oct 21, 2026
diffblue#9395 fixed float_bvt::round_fraction, which set bit 20 instead of bit 52 when rounding overflowed the significand of a double, as it computed 1 << 52 in int. Its test only covers converting a binary128 long double to double on ppc64le. The bug, however, equally affects conversions and arithmetic on the default target with the non-FPA SMT encoding (e.g., --z3), as reported in diffblue#9200: converting a long long just below 2^63 to double, or a double addition that rounds up to 2.0, yielded a tiny subnormal. Add these reproducers as a regression test, which fails with --z3 without the fix. Fixes: diffblue#9200 Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
changed the title
tautschnig
force-pushed
the
kiro/9200-float-bv-shift-overflow
branch
from
November 5, 2026 16:54
9656f0d to
189ed16
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The fix for #9200 (
float_bvt::round_fractioncomputing1 << 52inint, which set bit 20 instead of bit 52 when rounding carried out of a double's significand) was merged as part of #9395. That PR's test only covers converting a ppc64le binary128long doubletodouble. This PR adds the reproducers from #9200 as a regression test: converting along longjust below 2^63 todouble, and adoubleaddition rounding up to 2.0, on the default target. With--z3(run bymake -C regression/cbmc test-z3in CI), both assertions fail without the fix and pass on develop.Fixes: #9200