ansi-c: fix self-referential enum from __attribute__((mode)) fallback

[tautschnig]

For an enum with attribute((mode(M))), when M is not one of the special-cased mode names (e.g. plain "byte" rather than "byte"), the handler fell back to result = subtype, where the subtype is the c_enum_tag. It then wrote that back as the enum symbol's underlying type, making the enum's underlying type its own tag -- a cyclic, malformed type. This later caused infinite recursion in alignment() (a stack-overflow segfault) and a to_bitvector_type precondition abort in pointer_offset_bits(), crashing goto-cc on real kernel objects (net/rxrpc/rxgk, rxkad, af_rxrpc via crypto/krb5 headers).

Fall back to the already-resolved underlying bitvector type instead of the c_enum_tag subtype. For a non-enum bitvector subtype this is unchanged (underlying_type == subtype); for an enum subtype it uses the enum's underlying integer type, so no cycle is created.

Regression test gcc_enum_mode_attribute covers a special-cased mode (QI) and a fall-back mode name (byte).

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

[Copilot]

Pull request overview

Note

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

Fixes a crash in the ANSI-C typechecker when handling enums with __attribute__((mode(...))) for non-special-cased mode names by preventing creation of a cyclic/self-referential underlying enum type.

Changes:

• Adjust enum mode(...) fallback handling to use the already-resolved underlying bitvector type instead of the enum tag subtype.
• Add a regression test covering both a special-cased mode (__QI__) and a fallback mode name (byte).

Reviewed changes

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

File	Description
src/ansi-c/c_typecheck_type.cpp	Prevents cyclic enum underlying types by falling back to the resolved underlying bitvector type.
regression/ansi-c/gcc_enum_mode_attribute/test.desc	Adds a new regression test descriptor to ensure successful verification and no conversion errors/warnings for this case.
regression/ansi-c/gcc_enum_mode_attribute/main.c	Adds a C testcase reproducing the enum mode(...) scenario that previously triggered crashes during layout/alignment computation.

---

💡 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 (321ba11) to head (a631ed4).

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #9051   +/-   ##
========================================
  Coverage    80.68%   80.68%           
========================================
  Files         1714     1714           
  Lines       189501   189501           
  Branches        73       73           
========================================
+ Hits        152902   152908    +6     
+ Misses       36599    36593    -6     

☔ 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.