Uh oh!
There was an error while loading. Please reload this page.
Support anonymous struct embedding via -fms-extensions - #9022
Merged
Conversation
chaosape
requested review from
kroening, peterschrammel, remi-delmas-3000 and tautschnig
as code ownersMay 28, 2026 19:47
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@## develop #9022 +/- ##
========================================
Coverage 80.68% 80.69% ========================================
Files 1714 1714 Lines 189593 189596 +3 Branches 73 73 ========================================
+ Hits 152979 152987 +8 + Misses 36614 36609 -5 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
tautschnig
commented
May 31, 2026
Collaborator
Could you please add test(s) and address the clang-format error for a start? |
3 tasks
tautschnigforce-pushed
the
plan9-extensions
branch
2 times, most recently
from
June 24, 2026 11:17
1382f80 to
167c93bCompareA *tagged* struct/union used as an unnamed (anonymous) member -- e.g. the Linux kernel's `struct __filename_head;` embedded in struct filename -- was silently dropped by the C front-end in GCC/Clang mode: it contributed no bytes (so sizeof was wrong, breaking the kernel's static_assert(sizeof(struct filename) % 64 == 0)) and its members were not injected (inaccessible by name). GCC/Clang accept this only with -fms-extensions (the Plan 9 C extension); without it they ignore the member, matching the existing regression/ansi-c/anonymous_member* tests. So: - config: add ansi_c.allow_anonymous_struct_embedding (default false), named to be explicit that only this one MS/Plan 9 extension is implemented, not all of -fms-extensions; - gcc_mode: set it when -fms-extensions is passed (queried as "fms-extensions" -- goto_cc_cmdlinet stores long options without the leading '-'); - c_typecheck_type: in GCC/Clang mode accept an *untagged* struct/union anonymous member always (C11) and a *tagged* one only under -fms-extensions; a non-struct/union unnamed member, or a tagged one without the flag, keeps the previous "ignore" behaviour. With the flag the member now contributes its size and its fields are injected (reachable by name). The new behaviour is documented in the goto-cc section of the CPROVER manual, and exercised from both sides: goto-gcc/ms_extensions_anonymous_member checks exact layout and member access with the flag, and goto-gcc/ms_extensions_anonymous_member_ignored checks the member is ignored without it. The existing anonymous_member* tests confirm the default cbmc behaviour is preserved. Co-authored-by: Michael Tautschnig <tautschn@amazon.com> Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnigforce-pushed
the
plan9-extensions
branch
from
June 24, 2026 15:17
167c93b to
8206334Comparetautschnig
approved these changes
Jun 24, 2026
Uh oh!
There was an error while loading. Please reload this page.
tautschnig added a commit
that referenced
this pull request
Aug 21, 2026
This release adds support for anonymous struct embedding via -fms-extensions (via #9022), extends the in-tree SMT2 solver with mathematical and string/regex types and operations (via #9074), and fixes various front-end and encoding bugs. Docker images are now published to GitHub Container Registry instead of Docker Hub (via #9143). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
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 freeto join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
When -fms-extensions is passed, tagged struct/union members without a declarator name are treated as anonymous embedding (Plan 9 C extension). This allows code using the GCC extension where 'struct tag;' inside another struct inlines the tagged struct's fields.
The implementation lets the tagged anonymous member fall through to the existing anonymous member handling (the $anon naming + set_anonymous pass), rather than skipping it with 'continue'.
Only this one behavior is implemented — no other MSVC or Plan 9 extensions. The internal config field is named
allow_anonymous_struct_embedding to be explicit about scope.