C front-end: initializer lists do not initialise anonymous members #5688

tautschnig · 2020-12-23T22:47:56Z

We already took care of this in another place in
c_typecheck_initializer, but did not handle initializer lists correctly.

The test is based on a case found by C-Reduce when starting from an
SV-COMP task.

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.

codecov · 2020-12-23T23:25:32Z

Codecov Report

Base: 78.34% // Head: 78.34% // Increases project coverage by +0.00% 🎉

Coverage data is based on head (5d3e9a8) compared to base (a53fa0f).
Patch coverage: 91.30% of modified lines in pull request are covered.

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #5688   +/-   ##
========================================
  Coverage    78.34%   78.34%           
========================================
  Files         1644     1645    +1     
  Lines       190313   190381   +68     
========================================
+ Hits        149097   149156   +59     
- Misses       41216    41225    +9

Impacted Files	Coverage Δ
jbmc/src/janalyzer/janalyzer_parse_options.cpp	`48.58% <ø> (ø)`
.../src/java_bytecode/character_refine_preprocess.cpp	`54.27% <ø> (ø)`
...mc/src/java_bytecode/character_refine_preprocess.h	`100.00% <ø> (ø)`
jbmc/src/java_bytecode/ci_lazy_methods.h	`100.00% <ø> (ø)`
jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp	`98.41% <ø> (ø)`
jbmc/src/java_bytecode/ci_lazy_methods_needed.h	`100.00% <ø> (ø)`
jbmc/src/java_bytecode/code_with_references.cpp	`84.61% <ø> (ø)`
jbmc/src/java_bytecode/java_bmc_util.cpp	`100.00% <ø> (ø)`
...mc/src/java_bytecode/java_bytecode_convert_class.h	`0.00% <ø> (ø)`
...src/java_bytecode/java_bytecode_convert_method.cpp	`97.69% <ø> (ø)`
... and 405 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

martin-cs

The small part that touches area I maintain looks OK. I'm not sure the tests have enough context for me to really check what is going on with them.

regression/cbmc-library/memcpy-06/test.desc

kroening · 2021-01-13T12:40:18Z

regression/ansi-c/struct5/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--i386-win32
 ^EXIT=0$


Seems unrelated?

No, this is a relevant change. We previously wrongly supported the code in this test on all platforms: it uses anonymous (but tagged) union members.

kroening · 2022-09-23T09:26:52Z

Are zero-width bit-fields considered when processing initialiser lists?

tautschnig · 2022-10-09T13:18:56Z

@kroening:

Are zero-width bit-fields considered when processing initialiser lists?

The C standard requires "The expression that specifies the width of a bit-field [...]. If the value is zero, the declaration shall have no declarator." GCC and Clang enforce this, we did not. I'll put together a PR to ensure our C front-end becomes equally strict.

kroening · 2022-10-09T13:53:59Z

src/ansi-c/c_typecheck_type.cpp

+            if(
+              (new_component.type().id() != ID_struct_tag &&
+               new_component.type().id() != ID_union_tag) ||
+              follow(new_component.type()).find(ID_tag).is_not_nil())


What does the follow do here?

This is to distinguish untagged (anonymous) structs/unions from ones that are named.

I have extended the comment above this code now.

May I suggest using to_tag_type to make this clear.

I've rewritten it to use to_struct_tag_type and to_union_tag_type.

Compilers differ in their handling of anonymous members, also depending on the type of the anonymous member. Make sure we accurately model this while type checking. Consequently, regression tests need to be amened to either be compiler-specific or not rely on anonymous or empty compound types, which dump-c also must not spuriously generate (from incomplete structs or unions). New tests are based on a case found by C-Reduce when starting from an SV-COMP task. Behaviour across different compilers confirmed with Compiler Explorer (https://godbolt.org/).

tautschnig added bugfix C Front End labels Dec 23, 2020

tautschnig assigned kroening Dec 23, 2020

tautschnig requested review from chrisr-diffblue and kroening as code owners December 23, 2020 22:47

tautschnig assigned tautschnig and unassigned kroening Dec 24, 2020

tautschnig force-pushed the anonymous-members branch 4 times, most recently from f57b412 to 55c955a Compare December 27, 2020 06:02

tautschnig requested review from hannes-steffenhagen-diffblue, martin-cs, peterschrammel and smowton as code owners December 27, 2020 06:02

tautschnig force-pushed the anonymous-members branch 3 times, most recently from a1076c7 to ac8dd60 Compare December 27, 2020 12:05

tautschnig assigned kroening and unassigned tautschnig Dec 27, 2020

martin-cs approved these changes Jan 11, 2021

View reviewed changes

kroening reviewed Jan 13, 2021

View reviewed changes

regression/cbmc-library/memcpy-06/test.desc Outdated Show resolved Hide resolved

kroening reviewed Jan 13, 2021

View reviewed changes

tautschnig force-pushed the anonymous-members branch from ac8dd60 to 8df2a13 Compare January 13, 2021 21:35

tautschnig force-pushed the anonymous-members branch from 8df2a13 to b21e6b5 Compare March 3, 2021 07:54

tautschnig force-pushed the anonymous-members branch 2 times, most recently from 91e47de to 1ab17a4 Compare May 7, 2021 13:03

tautschnig force-pushed the anonymous-members branch from 1ab17a4 to e908072 Compare November 5, 2021 09:35

tautschnig assigned nwetzler Sep 22, 2022

tautschnig assigned tautschnig and unassigned kroening Sep 23, 2022

tautschnig force-pushed the anonymous-members branch from e908072 to ee50473 Compare October 9, 2022 13:25

tautschnig requested a review from chris-ryder as a code owner October 9, 2022 13:25

tautschnig assigned kroening Oct 9, 2022

kroening reviewed Oct 9, 2022

View reviewed changes

tautschnig force-pushed the anonymous-members branch 2 times, most recently from 8e16ac6 to 1f2aea9 Compare October 9, 2022 15:39

tautschnig removed their assignment Oct 9, 2022

tautschnig force-pushed the anonymous-members branch 2 times, most recently from e650662 to af9a202 Compare October 10, 2022 09:07

tautschnig force-pushed the anonymous-members branch from af9a202 to 6b0241c Compare October 27, 2022 09:30

tautschnig force-pushed the anonymous-members branch from 6b0241c to a9b5182 Compare November 18, 2022 22:56

tautschnig self-assigned this Nov 19, 2022

tautschnig force-pushed the anonymous-members branch from a9b5182 to e80a063 Compare November 21, 2022 13:27

tautschnig removed their assignment Nov 21, 2022

tautschnig force-pushed the anonymous-members branch from e80a063 to 5d3e9a8 Compare November 22, 2022 09:43

tautschnig assigned remi-delmas-3000 and peterschrammel Dec 1, 2022

peterschrammel approved these changes Dec 5, 2022

View reviewed changes

peterschrammel removed their assignment Dec 5, 2022

tautschnig merged commit 6672791 into diffblue:develop Dec 5, 2022

tautschnig deleted the anonymous-members branch December 5, 2022 12:47

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

C front-end: initializer lists do not initialise anonymous members #5688

C front-end: initializer lists do not initialise anonymous members #5688

Uh oh!

tautschnig commented Dec 23, 2020

Uh oh!

codecov bot commented Dec 23, 2020 •

edited

Loading

Uh oh!

martin-cs left a comment

Uh oh!

Uh oh!

kroening Jan 13, 2021

Uh oh!

tautschnig Jan 13, 2021

Uh oh!

kroening commented Sep 23, 2022

Uh oh!

tautschnig commented Oct 9, 2022

Uh oh!

kroening Oct 9, 2022

Uh oh!

tautschnig Oct 9, 2022

Uh oh!

tautschnig Oct 9, 2022

Uh oh!

kroening Oct 9, 2022

Uh oh!

tautschnig Oct 9, 2022

Uh oh!

Uh oh!

C front-end: initializer lists do not initialise anonymous members #5688

C front-end: initializer lists do not initialise anonymous members #5688

Uh oh!

Conversation

tautschnig commented Dec 23, 2020

Uh oh!

codecov bot commented Dec 23, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

kroening Jan 13, 2021

Choose a reason for hiding this comment

Uh oh!

tautschnig Jan 13, 2021

Choose a reason for hiding this comment

Uh oh!

kroening commented Sep 23, 2022

Uh oh!

tautschnig commented Oct 9, 2022

Uh oh!

kroening Oct 9, 2022

Choose a reason for hiding this comment

Uh oh!

tautschnig Oct 9, 2022

Choose a reason for hiding this comment

Uh oh!

tautschnig Oct 9, 2022

Choose a reason for hiding this comment

Uh oh!

kroening Oct 9, 2022

Choose a reason for hiding this comment

Uh oh!

tautschnig Oct 9, 2022

Choose a reason for hiding this comment

Uh oh!

Uh oh!

codecov bot commented Dec 23, 2020 •

edited

Loading