Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Split ieee_floatt into ieee_float_valuet and ieee_floatt #8550

Open
wants to merge 1 commit into
base: develop
Choose a base branch
from

Conversation

kroening
Copy link
Member

@kroening kroening commented Dec 31, 2024

This splits ieee_floatt into two parts:

  1. ieee_float_valuet stores an IEEE 754 floating-point value. It offers no operations that require rounding, and hence, does not require a rounding mode.

  2. ieee_floatt extends ieee_float_valuet with a rounding mode, and hence, offers operators that require rounding.

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@kroening kroening force-pushed the ieee_float_valuet branch 4 times, most recently from 2e21587 to 4e6923f Compare January 2, 2025 13:53
@kroening kroening changed the title Split ieee_floatt into ieee_float_valuet and ieee_floatt Split ieee_floatt into ieee_float_valuet and ieee_floatt Jan 2, 2025
@kroening kroening marked this pull request as ready for review January 2, 2025 13:55
Copy link

codecov bot commented Jan 2, 2025

Codecov Report

Attention: Patch coverage is 81.60920% with 48 lines in your changes missing coverage. Please review.

Project coverage is 78.95%. Comparing base (36b2335) to head (be78e50).

Files with missing lines Patch % Lines
src/util/ieee_float.cpp 76.76% 33 Missing ⚠️
src/ansi-c/goto-conversion/goto_check_c.cpp 40.00% 6 Missing ⚠️
src/goto-programs/interpreter_evaluate.cpp 0.00% 4 Missing ⚠️
src/analyses/interval_domain.cpp 0.00% 2 Missing ⚠️
...src/java_bytecode/java_bytecode_convert_method.cpp 75.00% 1 Missing ⚠️
src/goto-programs/interpreter.cpp 0.00% 1 Missing ⚠️
src/util/ieee_float.h 96.96% 1 Missing ⚠️
Additional details and impacted files
@@             Coverage Diff             @@
##           develop    #8550      +/-   ##
===========================================
+ Coverage    78.79%   78.95%   +0.15%     
===========================================
  Files         1730     1730              
  Lines       199160   198774     -386     
  Branches     18320    18376      +56     
===========================================
+ Hits        156938   156950      +12     
+ Misses       42222    41824     -398     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I very much like the idea, but I'm a bit confused: several places (some of which I've commented on below) appear to newly be drawing a rounding mode out of thin air when I'd naively have expected for those to be ieee_float_valuet. Can you please clarify?

@tautschnig tautschnig removed their assignment Jan 8, 2025
@kroening kroening assigned martin-cs and unassigned peterschrammel Jan 9, 2025
@kroening kroening force-pushed the ieee_float_valuet branch 4 times, most recently from 4112d43 to ac51457 Compare January 9, 2025 23:36
This splits ieee_floatt into two parts:

1) ieee_float_valuet stores an IEEE 754 floating-point value.  It offers no
operations that require rounding, and hence, does not require a rounding
mode.

2) ieee_floatt extends ieee_float_valuet with a rounding mode, and hence,
offers operators that require rounding.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants