ansi-c: support qualified __auto_type

[tautschnig]

GCC allows __auto_type with type qualifiers, e.g.
const __auto_type x = init;
which is equivalent to
const typeof(init) x = init;
The parser only had a production for the unqualified '__auto_type var = init;' form, so a qualified __auto_type -- as used by the Linux 6.12 kernel in arch/x86/include/asm/string_64.h -- failed with a syntax error.

Add a declaring_list production for
type_qualifier_list TOK_GCC_AUTO_TYPE declarator
post_declarator_attributes_opt '=' initializer
whose semantic action builds the typeof-of-initializer node and merges the qualifier list into it, mirroring GCC's documented semantics.

• 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).
• 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.

[kroening]

All tests for __auto_type in one directory, please!

[Copilot]

Pull request overview

Note

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

This PR updates the ANSI-C parser to accept GCC’s qualified __auto_type declarations (e.g., const __auto_type x = init;) by treating them as qualified typeof(initializer) types, and adds a regression test to prevent future breakage.

Changes:

• Extend declaring_list to parse type_qualifier_list TOK_GCC_AUTO_TYPE ... = initializer and build a typeof(initializer) type merged with qualifiers.
• Add a regression test that exercises const __auto_type and expects successful verification without parsing errors.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 2 comments.

File	Description
src/ansi-c/parser.y	Adds a new grammar production + semantic action to support qualified __auto_type by rewriting to qualified typeof(initializer).
regression/ansi-c/auto_type_qualified/test.desc	Defines a regression test that must not emit parsing errors and must verify successfully.
regression/ansi-c/auto_type_qualified/main.c	Minimal C program using const __auto_type to validate parsing and type deduction.

---

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

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.68%. Comparing base (d452071) to head (929f463).

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #9053      +/-   ##
===========================================
- Coverage    80.68%   80.68%   -0.01%     
===========================================
  Files         1714     1714              
  Lines       189547   189556       +9     
  Branches        73       73              
===========================================
+ Hits        152939   152946       +7     
- Misses       36608    36610       +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]

All tests for __auto_type in one directory, please!

Done.