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

Assignments to bit-fields yield results of bit-field type #8082

Merged
merged 2 commits into from
Dec 14, 2023

Conversation

tautschnig
Copy link
Collaborator

Do not pre-emptively cast side effects over bit-fields to the underlying type. sizeof just has a very peculiar semantics, which is discussed in https://www.open-std.org/jtc1/sc22/wg14/www/docs/n2958.htm.

Issue was found by CSmith (test generated with random seed 1700653858).

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a 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).
  • n/a 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.

@tautschnig tautschnig added C Front End soundness Soundness bug? Review and add "aws" if it is, or remove "soundness" if it isn't. labels Nov 24, 2023
@tautschnig tautschnig self-assigned this Nov 24, 2023
@tautschnig tautschnig marked this pull request as ready for review December 14, 2023 18:05
// the result is the declared width (rounded to bytes), all others use the
// size of the underlying type.
// https://www.open-std.org/jtc1/sc22/wg14/www/docs/n2958.htm
// for a discussion that this isn't actually specified (while being a
Copy link
Member

Choose a reason for hiding this comment

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

(Still GCC's interpretation makes considerably more sense than the others'.)

Copy link

codecov bot commented Dec 14, 2023

Codecov Report

Attention: 10 lines in your changes are missing coverage. Please review.

Comparison is base (2e0fcc8) 79.08% compared to head (16c0cbe) 79.08%.

Files Patch % Lines
src/ansi-c/c_typecheck_expr.cpp 56.52% 10 Missing ⚠️
Additional details and impacted files
@@           Coverage Diff            @@
##           develop    #8082   +/-   ##
========================================
  Coverage    79.08%   79.08%           
========================================
  Files         1698     1698           
  Lines       196465   196491   +26     
========================================
+ Hits        155380   155401   +21     
- Misses       41085    41090    +5     

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

goto-program conversion may introduce temporaries of c_bit_field type.
These, however, are not permitted outside structs in C. Instead, change
their types to their underlying types and use a bit mask to fix up
initial values.
Do not pre-emptively cast side effects over bit-fields to the underlying type.
sizeof just has a very peculiar semantics, which is discussed in
https://www.open-std.org/jtc1/sc22/wg14/www/docs/n2958.htm.

Issue was found by CSmith (test generated with random seed 1700653858).
@tautschnig tautschnig merged commit 3777fa9 into diffblue:develop Dec 14, 2023
35 of 36 checks passed
@tautschnig tautschnig deleted the bugfixes/bit-fields branch December 14, 2023 20:06
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
C Front End soundness Soundness bug? Review and add "aws" if it is, or remove "soundness" if it isn't.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants