Skip to content

ansi-c: support -fms-extensions anonymous tagged struct/union members#9050

Open
tautschnig wants to merge 1 commit into
diffblue:developfrom
tautschnig:extract/ansi-c-fms-anon-members
Open

ansi-c: support -fms-extensions anonymous tagged struct/union members#9050
tautschnig wants to merge 1 commit into
diffblue:developfrom
tautschnig:extract/ansi-c-fms-anon-members

Conversation

@tautschnig

Copy link
Copy Markdown
Collaborator

A 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). This is the second blocker (after __builtin_has_attribute) to compiling real kernel objects with goto-cc.

GCC/Clang accept this only with -fms-extensions (without it they ignore the member, matching the existing regression/ansi-c/anonymous_member* tests). So:

  • config: add ansi_c.ms_extensions (default false);
  • 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; otherwise (and for non-aggregate unnamed members) keep the previous "ignore" behaviour.

With the flag the member now contributes its size and its fields are injected (reachable by name). Regression test
goto-gcc/ms_extensions_anonymous_member checks exact layout via _Static_assert and member access; the existing anonymous_member1/3 (no flag, sizeof==0) confirm the default behaviour is preserved.

  • 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.
  • 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.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@tautschnig tautschnig self-assigned this Jun 18, 2026
Copilot AI review requested due to automatic review settings June 18, 2026 15:48

Copilot AI left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

Pull request overview

Note

Copilot was unable to run its full agentic suite in this review.

Adds support for MS-style extensions needed to correctly typecheck and lay out tagged anonymous struct/union members (e.g., Linux kernel patterns) when compiling in GCC/Clang mode with -fms-extensions.

Changes:

  • Introduce a new ansi_c.ms_extensions config flag (default false) and reset it in configt::set.
  • Enable the flag when -fms-extensions is passed through goto-gcc.
  • Extend compound member typechecking to accept tagged anonymous struct/union members only when ms_extensions is enabled, and add a regression test validating layout + member injection.

Reviewed changes

Copilot reviewed 6 out of 6 changed files in this pull request and generated 4 comments.

Show a summary per file
File Description
src/util/config.h Adds ansi_c.ms_extensions configuration flag.
src/util/config.cpp Initializes/resets ansi_c.ms_extensions during configt::set.
src/goto-cc/gcc_mode.cpp Parses -fms-extensions and maps it to config.ansi_c.ms_extensions.
src/ansi-c/c_typecheck_type.cpp Implements conditional acceptance of tagged anonymous struct/union members.
regression/goto-gcc/ms_extensions_anonymous_member/test.desc Adds a regression test driver for the new behavior.
regression/goto-gcc/ms_extensions_anonymous_member/main.c Adds a regression C file asserting layout and injected member access.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Comment thread src/goto-cc/gcc_mode.cpp
Comment on lines +587 to +593
// -fms-extensions enables MS/GCC extensions such as anonymous members
// that are a *tagged* struct/union type (used throughout the Linux
// kernel, e.g. struct __filename_head embedded in struct filename).
// Note: goto_cc_cmdlinet stores long options without the leading '-',
// so we query "fms-extensions" (cf. the "fshort-double" check below).
if(cmdline.isset("fms-extensions"))
config.ansi_c.ms_extensions = true;
Comment on lines +21 to +25
_Static_assert(sizeof(struct head) == 24, "head size");
_Static_assert(sizeof(struct filename) == 192, "filename size");
_Static_assert(
__builtin_offsetof(struct filename, iname) == 24,
"iname offset");
};
long tail;
};
_Static_assert(sizeof(struct u_outer) == 16, "union-anon size");
Comment thread src/goto-cc/gcc_mode.cpp
Comment on lines +592 to +593
if(cmdline.isset("fms-extensions"))
config.ansi_c.ms_extensions = true;
@codecov

codecov Bot commented Jun 18, 2026

Copy link
Copy Markdown

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.68%. Comparing base (321ba11) to head (8a14ea8).

Additional details and impacted files
@@           Coverage Diff            @@
##           develop    #9050   +/-   ##
========================================
  Coverage    80.68%   80.68%           
========================================
  Files         1714     1714           
  Lines       189501   189509    +8     
  Branches        73       73           
========================================
+ Hits        152902   152912   +10     
+ Misses       36599    36597    -2     

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

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
  • 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

@tautschnig

Copy link
Copy Markdown
Collaborator Author

We'll have to consider whether to take this one or #9022.

A *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). This is the second blocker (after
__builtin_has_attribute) to compiling real kernel objects with goto-cc.

GCC/Clang accept this only with -fms-extensions (without it they ignore
the member, matching the existing regression/ansi-c/anonymous_member*
tests). So:
- config: add ansi_c.ms_extensions (default false);
- 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; otherwise (and for non-aggregate unnamed members)
  keep the previous "ignore" behaviour.

With the flag the member now contributes its size and its fields are
injected (reachable by name). Regression test
goto-gcc/ms_extensions_anonymous_member checks exact layout via
_Static_assert and member access; the existing anonymous_member1/3 (no
flag, sizeof==0) confirm the default behaviour is preserved.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
@tautschnig tautschnig force-pushed the extract/ansi-c-fms-anon-members branch from ae1b3ef to 8a14ea8 Compare June 18, 2026 18:42
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.

2 participants